基于Dixon结式和逐次差分代换的多项式秩函数探测方法

秩函数探测是循环程序终止性分析的重要方法,目前,已有很多研究者致力于为线性循环程序探测对应的线性秩函数,然而,针对具有多项式循环条件和多项式赋值的多项式型的循环,现有的秩函数探测方法还有所不足,解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题,基于扩展Dixon结式(KSY方法)和逐次差分代换(SDS)方法,提出一种为多项式循环程序探测多项式型秩函数的方法。首先,将待探测的秩函数模板看作带参数系数的多项式,将秩函数的探测转换为寻找满足条件的参数系数的问题;然后,进一步将问题转换为判定相应的方程组是否有解的问题,至此,利用KSY方法中的扩展的Dixon结式,将问题更进一步简化为带参系数多项式(即结式)严格为正的判定问题;最后,利用SDS方法,找到一个充分条件,使得得到的结式严格为正,此时,可以获取满足条件的参数系数的取值,从而找到一个满足条件的秩函数,通过实验验证该秩函数探测方法的有效性。实验结果表明,利用该方法,可以有效地为多项式循环程序找到多项式秩函数,包括深度为d的多阶段多项式秩函数,与已有方法相比,该方法能够更高效地找到多项式秩函数,对于基于柱形代数分解(CAD)方法的探测方法因时间复杂度问题无法而应对的一些循环,利用所提方法能够在几秒内为这些循环找到秩函数。

Polynomial ranking function detection method based on Dixon resultant and successive difference substitution

Ranking function detection is one of the most important methods to analyze the termination of loop program. Some tools have been developed to detect linear ranking functions corresponding to linear loop programs. However, for polynomial loops with polynomial loop conditions and polynomial assignments, existing methods for detecting their ranking functions are mostly incomplete or with high time complexity. To deal with these weaknesses of existing work, a method was proposed for detecting polynomial ranking functions for polynomial loop programs, which was based on extended Dixon resultants (the KSY (Kapur-Saxena-Yang) method) and Successive Difference Substitution (SDS) method. Firstly, the ranking functions to be detected were seen as polynomials with parametric coefficients. Then the detection of ranking functions was transformed to the problem of finding parametric coefficients satisfying the conditions. Secondly, this problem was further transformed to the problem of determining whether the corresponding equations have solutions or not. Based on extended Dixon resultants in KSY method, the problem was reduced to the decision problem whether the polynomials with symbolic coefficients (resultants) were strictly positive or not. Thirdly, a sufficient condition making the resultants obtained strictly positive were found by SDS method. In this way, the coefficients satisfying the conditions were able to be obtained and thus a ranking function satisfying the conditions was found. The effectiveness of the method was proved by experiments. The experimental results show that polynomial ranking functions including d-depth multi-stage polynomial ranking functions are able to be detected for polynomial loop programs. This method is more efficient to find polynomial ranking functions compared with the existing methods. For loops whose ranking functions cannot be detected by the method based on Cylindrical Algebraic Decomposition (CAD) due to high time complexity, their ranking functions are able be found within a few seconds with the proposed method.