本科毕业设计（论文）

外文翻译

代数基本定理的一个不依赖于有理数的构造性证明

作者：Herman Geuvers, Freek Wiedijk, and Jan Zwanenburg

国籍：Netherlands

出处：Types for Proofs and Programs

中文译文：

摘要：在Nijmegen的FTA项目中，我们已经形成了代数基本定理的构造性证明。在形式化过程中，我们首先定义了群，环，域等(构造性的)代数体系。对于实数，我们定义了实数结构的概念，它基本上是一个Cauchy完备阿基米德有序域。这归结为构造性实数的公理化。然后从这些公理(与实数的构造无关)中给出FTA的证明，其中复数定义为实数对。

我们选择形式化的FTA的证明是Troelstra和van Dalen[17]的具有重大意义的著作中的一个，最初是由Manfred Kneser[12]提出的。Troelstra和van Dalen的证明充分使用有理数（作为实数的合适近似值），这在构造分析中非常普遍，因为有理数的相等是可判定的，而实数上的等式则不是。在我们的例子中，因为实数的公理化并不包含有理数。此外，我们发现如果关于实数的证明涉及到有理数问题是困难的。因此，我们的FTA证明版本没有提到有理数。这里描述的证明是在Coq系统中完全形式化证明的体现。

简介

代数的基本定理指出复数域是封闭的。更明确地说，对于每一个非常数多项式:

系数在中，方程有一个解。

这个定理有着悠久而辉煌的历史(见[6][11]概述)。年。高斯博士在他发表的论文中首次给出了证明。代数基本定理的许多证明是已知的，其中大多数都具有构造性。

在这里我们展示的证明是由Manfred Kneser给出的(灵感来自他父亲Hellmuth Kneser在[11]中的证明)，通过来确定非常数多项式在处最小值，且的假设，导致矛盾而得出一个简单的构造性证明。我们在这里简短地重复经典的证明。

设是一个非常数多项式。首先，注意必须有一个最小值，因为如果.则，我们可以假设时达到的最小值(如果在达到最小值，考虑多项式。现在，假设的最小值不是(即)，函数具有以下形式

且.因此，我们可以令:

并且有，并且如果足够小，则部分与其余部分相比可忽略不计，并且我们得到

所以不是最小值，我们得出了一个矛盾。

通过迭代的想法，我们可以尝试构造一个Cauchy序列到多项式的零点。这种方法的主要困难在于我们对选择有两个相互矛盾的要求：

1.每次选择的太小，我们可能无法在可数多个步骤中达到零(我们将会下降，但可能不会一直下降到零)。

2.如果不够小，我们不允许忽略部分。

对此的解决方案是：在构造性证明中，不是使用上述表示(其中是具有非零系数的最小幂)，只需要一些合适的(不一定最小的)，并将写为:

这样不仅可以确保，而且对于某些固定的，也可以保证。

Manfred Kneser在[12]中提出的FTA证明是经典的，可以在没有任何严重问题的情况下变得具有构造性。在[17]中，给出了这个证明的一个构造性版本，使用有理逼近来克服实数上的等式的不可判定性。Swichtenberg在[15]中提出了Kneser证明的另一个构造性版本，也使用了有理逼近，但沿着不同的方向。FTA的构造性版本如下。

对于每个多项式:

的系数在中，对于某个，若，则等式有一个解。

因为上的等式(因此也在C上)是不可判定的，(不一定，我们不能将写为，其中。因此，在构造性分析中，我们使用间隔的概念，通常用表示。这是一个正定的不等式：如果我们肯定它们是不同的，即我们知道它们之间的距离。现在，如果我们肯定地知道某个系数与不同，那么可以构造性地找到的根。构造性FTA的证明首先证明一元多项式(即其中)是成立的。

一元多项式FTA的Kneser证明是利用系数为的多项式逼近，因为它需要比较各种表达式的大小(在中不可判定)。我们发现结果并不令人满意：有理数似乎与代数基本定理没有任何关系！另外，在Kneser证明Coq这个过程中，我们公理化地引入了实数(因此根据先验，我们在形式化过程中不涉及，为了能够形式化，重构实数内的有理数似乎是行不通的。因此，与其构造Q，我们选择修改了证明，使其不再涉及有理数。结果如下。

修改证明背后的主要思想是我们在比较中引入“模糊性”。证明包含一个“模糊参数”，而不必要求是否

我们需要确定的是

（我们可以通过的关系写成：

从构造性来看，他们的阶的关系具有传递性

由此可见，即使与的脱离也是可判定的。

除了不需要之外，这里给出的证明与文献[17]中的证明之间的另一个区别是，避免使用了Vandermonde。在原证明中，这用于证明一元多项式的FTA。我们通过多项式算法直接证明了这一含义。因此，在证明中不再使用线性代数。

我们已经使用Coq系统形式化了此处提供的证明：这就是所谓的FTA项目[7]，在形式化中，我们公理化地对待实数。更准确地说，实数构成了构造性代数体系的一部分，其中包括环，域和有序域的抽象概念，详见[8]。这个体系的基本级别包含构造性的setoid的概念，它基本上是一对类型和类型之间的间隔关系。(对于构造性的实数，“分开”比“等式”更加基础，所以我们从“分开”开始)。在这个体系中，实数结构被定义为Cauchy完整的阿基米德有序域。在FTA项目中，代数的基本定理证明适用于任何实数结构，因此事实上该定理是从构造实数的公理中证明的。此外，它表明通过构造证明了实数结构的存在性。有关此构造的详细信息，请参阅[9]，其中还讨论了其他公理化，并且表明任何两个实数结构都是同构的。

整个形式化为930K的Coq源代码，其中包括由Milad Niqui构建的实数，与文数学直接对应的部分约为65K的Coq源。在形式化中证明的最终引理是，在Coq语法中：

本文的计划如下：首先，我们介绍了Kneser证明中隐含的寻找根的算法(为简单起见，我们给出了该算法的经典版本)。之后，我们给出完整的构造性Kneser证明，其中包含算法的正确性证明。

Kneser经典算法

设

是次的复数域上的一元多项式。对于任意的复数我们构造一种计算Cauchy序列的算法

是收敛到该多项式的零点。

假设已经建立。由此我们必须确定序列中的下一项。故有两种可能性：

1.在的情况下，我们已经有零点，所以我们令即可；

2.在的情况下我们考虑多项式，通过定义，找到适当的，然后取

所以在第二种情况下我们有多项式

(事实上，系数取决于，但为了保证公式的简洁性，我们不考虑这种依赖性)，且有和，我们必须确定。

首先，我们将确定。定义

并由此定义一系列半径

通过

(可知每个半径都是前一个半径的)。

现在对于每个，让是的元素，这样

是最大的(如果有多个元素属于并取得最大值，则取最小一个)。这样构造出来一个递减序列

.

取最小的

并且令，我们定义为，并使与复平面中的相等。这意味取

和 以上是对Kneser算法的经典版本的简介。

注意：因为这里有个不同的复数根，故最后一步有很多方法。所以序列

实际上是这个算法计算的无限树中的一条路径。当然，沿着树中的不同路径可能会找到不同的零点。(和)选择的具有以下性质(这些性质和正确性将在下一节中详细说明。)

第一个不等式表示，因此序列的f值收敛于。第二个不等式表示，所以序列收敛。

Kneser构造性证明

现在我们介绍Kneser证明代数基本定理。与[17]中的证明不同，这个版本的证明中不使用。在证明中，我们不涉及关于实数的部分并且只涉及复数的部分。

复数域的一个基本性质是-次根存在，所以可以独立于FTA证明。这一事实最著名的证明是移至的极坐标表示法，因为我们选择了作为的表示法，所以这不是一个易于形式化的证明(首先必须定义函数，并在两个表示之间建立同构关系)。因此我们选择了一个基于构造性的证明。详见[5]和[13]。这里，中-次根的存在性直接来源于中平方根的存在性以及上的所有奇数次的多项式都有根的事实。这些性质的证明已在Coq中完全形式化。需注意的是，中值定理(它表示上的所有奇数次的多项式都有根)在构造性上是无效的。但是，可以证明多项式的中值定理。(在我们的形式化中，我们遵循了[17]的证明，使用引理作为了一个重要的捷径)。

FTA的证明使用了三个引理，在Coq形式化中被称为“关键引理”，“主要引理”和“Kneser引理”。我们在这里给出表示对应于它在Coq中形式化的方式。

首先，我们给出一个辅助引理，即可以通过构造找到“到达”的序列的最大值

引理：对于，，，存在一个，对所有有：

证明方法是简单的归纳法，通过关系的传递性来确定的最大值，首先确定(归纳假设)，比如，先选择若和。由于lt;的传递性性，可以做出后一种选择。

我们现在陈述关键引理：

引理2(关键引理)：对于每个和

且，那么有：

并且对于任意，如果我们定义，则对于有：

这个引理对应于上一节中建立和序列算法部分(在上一节被称为，在这里被称为，因为关键引理中不需要引用复数)。在经典情况下的令为：

在这里通过来表示

与经典情况的真正区别在于，在期间“取最大值”只是“达到：不同于，并且可能是最大的，但它不会超过之前选定的。

我们现在证明关键引理：

证明：首先，我们选择和，先取和的初始值，然后依次考虑的值从降至，并保证以下等式不变：

从初始值和开始。然后在每个处(从到)，我们更新和的值如下

1.如果，则不执行任何操作，并且不变量保持不变

2.如果，则将令为，为(这种情况下，的值在减少)。不变量的第一部分仍然不变，对于第二部分，它大于每一个(基于先前选择的的不变量和的值减少的事实)。此后，和具有合适的值。

因为我们从，，我们应用引理1，并将带入序列

得到，若

以及

我们现在将陈述并证明主要引理，该引理将关于实数的证明部分与涉及复数的部分分离开。

引理3(主要引理)：满足不等式

并有

主要引理对应于经典算法描述中和的选择。第一个条件表明与前一个值相比不能太大，这对应于在经典算法的讨论中提到的性质。第二个条件是确保如果我们让指向的相反方向，那么变得足够小(主要引理是关于实数的，但它会通过取来应用，其中是多项式的系数)。而且，第二和第三条件一起确保总和其余部分可忽略不计。

我们现在将证明主要引理。

应用关键引理得到序列和，因为序列是在有限集非递增的，所以存在最小的

取和。

因为，对于任意有

在这种情况中，和是特殊情况。

之后都有

从我们得到所有

从那以后就有

因此

同理就有

所以

结合上式得

我们现在陈述并证明Kneser引理。这个引理表明我们可以在前一节中找到所谓的：一个合适的向量，使足够接近零。在Kneser证明的经典版本中，根据或来区分情况。在第一种情况下，我们已经完成了证明，而在第二种情况下，我们发现存在一个使得<!--

剩余内容已隐藏，支付完成后下载完整资料

---

英语原文共 16 页，剩余内容已隐藏，支付完成后下载完整资料

---

资料编号：[272301]，资料为PDF文档或Word文档，PDF文档可免费转换为Word