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

摘要：

主要解决了如下形式的程序的终止性判定的问题:while(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).

关键词：程序验证、计算机代数、非线性程序、不动点

所属期刊栏目：43

分类号：TP181;TP301(自动化基础理论)

资助基金：国家重点基础研究发展计划资助项目2004CB318003

在线出版日期：2017-01-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：76-80