带约束Prolog的更好终止性
Better Termination for Prolog with Constraints
摘要：
实际的Prolog系统的终止性是脆弱的，难以分析。缺乏发生检查，moded和过载的算术评价通过是/2和偶尔nontermination的有限域约束是无效的终止分析器，依赖于理想化的假设所获得的终止结果的所有来源。在本文中，我们提出的解决方案，以解决这些问题的底层Prolog系统的水平。改进的统一模式通过提供动态发生检查检测来满足基于范数的分析器的要求。广义有限域求解器克服了传统算法的缺点，没有显着的运行时开销。解算器提供无界域，但传播始终终止。我们的工作改进了Prolog的终止性，使Prolog成为一个更可靠的终止性和类型分析的目标。它是SWI-Prolog 5.6.50版本的一部分。
英文摘要：
Termination properties of actual Prolog systems with constraints are fragile and difficult to analyse. The lack of the occurs-check, moded and overloaded arithmetical evaluation via is/2 and the occasional nontermination of finite domain constraints are all sources for invalidating termination results obtained by current termination analysers that rely on idealized assumptions. In this paper, we present solutions to address these problems on the level of the underlying Prolog system. Improved unification modes meet the requirements of norm based analysers by offering dynamic occurs-check detection. A generalized finite domain solver overcomes the shortcomings of conventional arithmetic without significant runtime overhead. The solver offers unbounded domains, yet propagation always terminates. Our work improves Prolog's termination and makes Prolog a more reliable target for termination and type analysis. It is part of SWI-Prolog since version 5.6.50.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
