多区间上非线性程序的终止性判定

作者：牟琳; 李轶; 李玲娜; 刘栋

来源：四川大学学报(工程科学版), 2011, (03): 76-80.

DOI：10.15961/j.jsuese.2011.03.019

• 程序验证
• 计算机代数
• 非线性程序
• 不动点 program verification
• computer algebra
• nonlinear program
• fixed point

主要解决了如下形式的程序的终止性判定的问题:wh ile(x∈Ω)do{x:=f(x)}end,其中,x为程序变元,Ω(Ω=(a1,b1‖∪‖a2,b2‖∪…∪‖an,bn),其中,‖∈{(,),[,]},n∈N*)是间段并集,f是一个多项式函数。证明了:当φ(b1)φ(a2)>0,…,φ(bn-1)φ(an)>0(其中,φ(x)=f(x)-x)时,这类区间上的非线性程序不终止的必要条件是:在Ω内部或者边界上存在不动点。如果不动点仅仅在Ω内部,则上述结果是充要条件。通过添加一定的约束条件,对于仅区间边界有不动点的情况,也给出了判定的方法。对一类多项式函数的终止性给出了完备性的算法(TNPSI)...

• 出版日期2011
• 单位电子科技大学; 中国科学院成都计算机应用研究所