传统的数学证明是用纸和笔来完成的,而随着计算机技术的发展,一些问题的数学证明已经可以利用计算机来完成.可信验证正是利用计算机来数学证明某个问题在某区间内存在解的一种方法.另外,可信验证方法还可以解决数值方法几乎不能完成的工作.代数方程组的可信验证问题,即是建立有效的可信验证方法给出包含方程组解的区间量,又称为方程组的解存在性检验,是可信验证研究课题中的最基本问题之一.本文主要研究代数方程组解的可信验证方法及其INTLAB实现.代数方程组的可信验证问题来源于科学及工程计算的许多领域,比如火箭喷口受力分析,核磁共振机设计,数码机床控制等高风险应用领域中的很多问题最终都要归结为非线性方程组解的可信验证问题;再比如Stokes方程的求解,约束与加权最小二乘估计,约束优化,电磁方程的计算,电力系统与网络构造,计算机图形学的网格生成等具体问题,最终则要转化成线性方程组解的计算与验证问题.因此,研究、发展和完善代数方程组解的可信验证方法及其具体的算法实现程序具有重要的理论意义和很高的实用价值.考虑一般的n个未知量n个方程的非线性方程组f(x)=0,(1)其中f:Rn→Rn,f=(f1,f2…,fn)T,f1,f2…,fn为n2元非线性函数.直到目前为止,Rump在1983年所做的工作仍然是检验其解存在的最为基本最为实用的可信验证方法.Rump可信验证方法(即解存在性定理3.1.2和验证算法3.1.1)是利用Brouwer不动点定理和改进的Krawczyk区间算子S(x,x)=-Rf(x)+(In-RJf(x+x))x(2)建立的,其中x∈ Rn,x∈IRn且 0∈x,Jf(x+x)=∩{M∈IRn×n|(?)x ∈ x+x,Jf(x)∈ M},R∈Rn×n为任意非奇异矩阵.在Rump可信验证方法中,矩阵R取为Jf(x)-1,即有S(x,x)=-Jf(x)-1f(x)+(In-Jf(x)-1 Jf(x+x)x=:SR(x,x),(3)+其中Jf(x)-1为映射f在x处的雅可比(Jacobian)矩阵Jf(x)的逆矩阵.从实际计算的角度看,区间算子S(x,x)(2)的SR(x,x)(3)形式需要额外耗费一定的计算量和时间去计算矩阵Jf(x)和进行区间运算.而如果把区间算子S(x,x)(2)中的矩阵R取为(mid Jf(x+x)-1,则所有不足都将迎刃而解.在第三章,我们首先利用R=(mid Jf(x+x))-1和区间量x,Jf(x+x)的中点半径表示形式x=mid x+rad x[-1,1]=mid x+1/2wid x[-1,1]和Jf(x+x)=mid Jf(x+x)+1/2wid Jf(x+x)[-1,1]给出了区间算子S(x,x)(2)的另一种具体形式,即SH(x,x):=-(mid Jf(x+x)-1 f(x)+1/4|(mid Jf(x+xc))-1|wid Jf(x+x)wid x[-1,1]+1/2|(mid Jf(x+x))-1|wid Jf(x+x)|mid x|[-1,1].(4)对比区间算子S(x,x)(2)的SR(x,x)(3)形式和SH(x,x)(4)形式,我们不难发现形式SH(x,x)(4)不再涉及矩阵Jf(x)的计算,而替代它的矩阵mid Jf(x+x)可以从这两种形式都要使用的区间矩阵Jf(x+x)中直接获取,即我们无需再花费额外的计算量和时间去计算矩阵mid Jf(x+x);还能发现形式SH(x,x)(4)不会直接涉及区间量之间的运算,这是因为(mid Jf(x+x))-1,wid Jf(x+x)∈ Rn×n和mid x,wid x∈Rn,即这些矩阵和向量都不是区间量,而在形式SR(x,x)(3)中,区间量之间的运算是不可避免的,这又是因为In-Jf(x)-1 Jf(x+x)∈ IRn×n和x∈IRn,即这些量都是区间量.所以,基于形式SH(x,x)(4)建立的验证算法的计算量要比基于形式SR(x,x)(3)建立的验证算法低很多.另外,在一些附加条件下,我们还证明了包含关系SH(x,x)SR(x,x)成立,其中x∈ Rn为非线性方程组(1)的非奇异解或单根,即雅可比矩阵Jf(x)非奇异.然后在验证算法3.1.1的基础上,我们利用区间算子S(x,x)(2)的SH(x,x)(4)形式和解存在性定理3.1.2给出了改进验证算法3.3.1.和原验证算法3.1.1相比,理论分析和数值结果都表明,改进验证算法3.3.1不仅节约了验证时间,而且还可以给出宽度更窄(或至少相同)的包含非线性方程组(1)解的区间向量.由于基于Brouwer不动点定理建立的解存在性定理(比如定理3.1.1和3.1.2)的假设条件都是用一个区间上所有点的信息刻画的,这使得该类定理的假设条件不太容易满足,所以由其建立的可信验证方法(即Rump型可信验证方法)只有借助高精度的初值才能验证成功,这对Rump型可信验证方法的广泛应用是极为不利的.而对应的,由于Kantorovich存在定理的假设条件是基于一点的信息进行刻画的,这使得它的假设条件更容易得到满足,所以用其建立的可信验证方法对于精度较低的初值也能验证成功.由此可以想象的到,这类可信验证方法必定有着广泛的应用前景.在解存在性检验研究史上,曾经也有学者就应用Kantorovich存在定理检验非线性方程组(1)解存在问题进行过深入的研究,但遗憾的是所做的工作均处于理论阶段,没有给出具体的算法实现程序.在第四章,我们给出了应用Kantorovich存在定理验证非线性方程组(1)解存在的具体算法实现程序.Kantorovich存在定理是前苏联著名数学家Kantorovich在20世纪50年代研究非线性方程组(1)的Newton迭代解法的收敛性、误差估计等问题时提出、并利用优界方程思想证明的.其具体内容如下:定理1设非线性映射f:DRn→Rn及x∈ Rn满足下列条件:1.f(x)-1 存在,且 ‖f’(x)-1‖≤β,‖f’(x)-1(x)-1f(x)‖≤η;2.x∈U(x,2η)D,f’(x)存在且满足Lipschitz条件‖f’(x)-f’(y)‖ ≤ K‖x-y‖,x,y ∈ U(x,2η).(5)若ρ:=kβη≤0.5,则非线性方程组f(x)=0于x的δ-领域U(x,δ)有唯一解x存在,其中δ=η.从定理1不难发现,应用Kantorovich存在定理验证非线性方程组(1)解存在的难点是严格计算Lipschitz条件(5)中的常系数k.为了解决这一难题,我们首先根据多元分析理论和矩阵理论,并借助张量表示法给出了一个可用于计算Lipschitz常系数K的具体表达式其中表示多元函数fi在x∈U(x,2η)处的二阶偏导数,i,j,k=1,2,…,n2.因为根据区间分析理论可知,对任意的x∈U(x,2η)有其中(?)(x)表示二阶偏导函数(?)在区间向量x=[x-2η,x+2η]上的具包含单调性的区间扩展,0≤yi∈IR,i,j,k=1,2,…,n,而区间yi可由INTLAB/Matlab命令语句Yi=fi(hessianinit(x))和yi=norm(Yi.hx,Inf)直接获得,所以在实际计算时,量Ki:=(?)的大小是通过区间量yi计算的,即ki=yi,其中yi为区间yi的上端点.于是K=n max{K1,K2,…,Kn}.然后在理论研究的基础上,我们利用INTLAB/Matlab软件给出了应用Kan-torovich 存在定理验证非线性方程组(1)解存在的具体算法实现程序,即算法 4.3.1和 4.3.2.相对于流行的Rump型验证算法(即算法3.1.1和3.3.1),理论分析和数值实验均表明,我们的Kantorovich型验证算法(即算法4.3.1和4.3.2)具有以下两方面的优势:一是该验证算法对初值的精度要求不高,即该验证算法使用精度较低的初值就能验证成功;二是该验证算法具有承袭性,即在验证过程中,如果因为初值精度低导致验证失败,需要通过提高初值精度再次进行验证时,该验证算法在新的验证步中可以利用上个验证步中的部分运算结果以降低运算量.第五章研究了鞍点线性方程组(?)(7)的可信验证问题,其中矩阵A ∈ Rn×n对称正定,B∈ Rm×n行满秩;右端项c∈ Rn,d ∈Rm;向量x∈Rn,y ∈ Rm 为未知量;n≥m.该类问题的应用背景十分广泛,诸如计算流体力学,约束与加权最小二乘估计,约束优化,电磁方程的计算,电力系统与网络构造,计算机图形学的网格生成等具有不同应用背景的数学模型问题,最终都要转化为大规模的鞍点线性方程组(7)解的计算与验证问题.由于传统的线性方程组解的可信验证方法均需要使用系数矩阵的数值近似逆,而对于鞍点线性方程组(7)的系数矩阵H∈R(m-n)×(m-n),一是其条件数会随着问题规模的扩大而变大;二是其逆矩阵一般情况下不再具有稀疏性,所以这些传统的可信验证方法对于维数l:=m+n很大的鞍点线性方程组(7)就不再有效.为了避免使用系数矩阵H的数值近似逆,2009年,Kimura和Chen首先利用块对角预处理子及其代数分析理论解决了量‖H-1‖2的实际计算问题,即(?)(8)然后他们利用界估计式(8)给出了线性方程组(7)如下的误差界:(9)其中u,u∈R1分别表示鞍点线性方程组(7)的准确解和满足一定精度的数值解.再由矩阵A和BBT的对称性,可得其中Q(A)表示矩阵A的谱半径.于是根据误差界(9)又可得(10)一般来说,误差界(10)比误差界(9)更容易实现.另外在条件下,还有(11)其中A-1和BBT-1分别表示矩阵A和BBT的满足一定精度的数值近似逆.由矩阵A和BBT的对称正定性和当今求逆方法的数值稳定性可知,数值矩阵A1和BBT-1是十分接近矩阵A1和(BBT)1的,所以条件‖A-1A-In‖∞<1和‖BBT-1(BBT)-Im‖∞<1是容易成立的.综上所述,Kimura和Chen的可信验证方法可归纳为如下形式:(12)可信验证方法(12)的优点是避免使用系数矩阵H的数值近似逆,采用了更易实现的误差界(10),并应用界估计式(11)来达到快速计算量‖A-1‖∞和‖(BBT)-1‖∞的目的.该验证方法的不足是量‖(BBT)-1‖∞有时候会很大,这会导致可信验证方法(12)给出的结果没有实用价值.此外,尽管矩阵A是稀疏的,但是其数值近似逆A-1不再具有稀疏性.这将导致我们无法利用计算机有效解决更大规模的鞍点线性方程组(7)的可信验证问题.为了弥补可信验证方法(12)的不足,我们给出了如下的改进可信验证方法.首先,由矩阵A-1和(BBT)-1的实对称正定性可得其中λmin(·)表示实对称正定矩阵A和BBT的最小特征值.其次,如果还存在正实数α,β分别使得矩阵A-αIn和BBT-βIm亦为实对称正定矩阵,则λmin(A)>α>0 和λmin(BBT)>β>0.所以,我们有(13)最后,利用矩阵A的对称性和误差界(9)又可得(14)综上所述,我们的可信验证方法如下:(15)在实际应用时,为了确保可信验证的顺利实现和效果,可信验证方法(15)中的正实数α和β一般要分别选取为α=0.9λmin(A)或0.95λmin(A),β=0.9λmin(BBT)或0.95λmin(BBT),其中λmin(·)表示实对称正定矩阵A或BBT的最小特征值的数值近似,可采用反幂法求之.由于矩阵A和BBT的对称正定性和当今计算矩阵极大极小特征值技术的先进性,所以上述的解决方案是可行的.实对称矩阵A-αIn和BBT-βIm的正定性判断则由INTLAB函数isspd来完成.理论结果和数值结果均表明,改进后的可信验证方法(15)不仅耗费的计算时间比原可信验证方法(12)的少,而且给出的解的误差界也比可信验证方法(12)的小.另外,有关理论分析和数值结果还表明,可信验证方法(15)对于更大维数的鞍点线性方程组(7)仍然有效,所以可信验证方法(15)的适用范围要比可信验证方法(12)的广泛.除上述研究工作外,我们还利用鞍点矩阵H的特有结构和特殊性质以及矩阵基本理论,给出了界估计式(8)的另一种证明方法.与原证明法相比,新证明方法更简单明了.