可积整环中终止性的单调性约束
Monotonicity Constraints for Termination in the Integer Domain
摘要：
大小变化终止（SCT）是一种基于无限下降不可能性的程序终止性证明方法。为此，我们使用一个程序抽象，其中过渡描述的单调性约束（抽象）变量。当只允许形式为x>y'和x \geq y'的约束时，我们有大小变化图。在过去的十年中，理论和实践都在这个有限的框架内发生了重大变化。过去大多数工作的关键基本假设是变量的域是有根据的。在最近的一篇论文中，我展示了如何将一些理论从大小变化图的域扩展到一般的单调性约束，从而补充了以前的工作，但仍然停留在良基域的领域。然而，单调性约束，有趣的是，能够证明终止也在整数域中，这是没有根据的。本文的目的是探讨单调性约束在这一领域中的应用。我们奠定了必要的理论基础，并提出了精确的决策程序终止;最后，我们提供了一个程序来构建明确的全球排名功能的单调性约束在单指数时间，最佳的最坏情况下的大小和尺寸（序数）。
英文摘要：
Size-Change Termination (SCT) is a method of proving program termination based on the impossibility of infinite descent. To this end we use a program abstraction in which transitions are described by Monotonicity Constraints over (abstract) variables. When only constraints of the form x>y' and x\geq y' are allowed, we have size-change graphs. In the last decade, both theory and practice have evolved significantly in this restricted framework. The crucial underlying assumption of most of the past work is that the domain of the variables is well-founded. In a recent paper I showed how to extend and adapt some theory from the domain of size-change graphs to general monotonicity constraints, thus complementing previous work, but remaining in the realm of well-founded domains. However, monotonicity constraints are, interestingly, capable of proving termination also in the integer domain, which is not well-founded. The purpose of this paper is to explore the application of monotonicity constraints in this domain. We lay the necessary theoretical foundation, and present precise decision procedures for termination; finally, we provide a procedure to construct explicit global ranking functions from monotonicity constraints in singly-exponential time, and of optimal worst-case size and dimension (ordinal).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
