ACL2 中的代数基本定理

我们报告了在 ACL2(r) 中对代数基本定理的验证。该证明由四部分组成。首先，定义了复值和实值复变函数的连续性，并证明从复数到实数的连续函数在闭正方形区域上能取到最小值。取连续复函数的传统复范数可得到连续实值复函数这一重要情形。我们将这些连续函数视为只有一个（复）自变量，但在 ACL2(r) 中它们表现为带两个自变量的函数。额外的自变量是一个“上下文（context）”，它未被解释。例如，它可以是被固定的其他自变量，如指数函数中的底数和指数，二者均可被固定。其次，证明复多项式是连续的，因此复多项式的范数是连续实值函数，并在以原点为中心的任意正方形区域上取到最小值。证明的这一部分得益于“上下文”自变量的引入，并展示了一种简化带无界参数的经典性质证明的创新。第三，我们推导了非常数多项式在离原点足够远的输入下范数的下界和上界。这意味着可以找到一个足够大的正方形，保证其包含多项式范数的全局最小值。第四，证明若给定数不是非常数多项式的根，则它不能是全局最小值。最后，综合这些结果证明全局最小值必为该多项式的根。该结果是 ACL2(r) 中复多项式形式化这一更宏大工作的一部分。