Proving Termination of Constraint Solver Programs
Proving Termination of Constraint Solver Programs
复制标题
证明约束求解器程序的终止
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Thom W. Frühwirth
中科院分区：
文献类型：
--
作者：
Thom W. Frühwirth
我们适应和扩展现有的方法，终止在基于规则的语言（逻辑编程和重写系统），以证明终止实际实现的约束求解器。约束处理规则（Constraint Handling Rules）是一种声明性语言，专门用于编写约束求解器。约束逻辑是一种并发约束逻辑编程语言，由多头保护规则组成，这些规则将约束重写为更简单的约束，直到它们被解决。该方法允许证明终止许多约束求解器，从布尔和算术术语和路径一致的约束。由于多头，我们的终止顺序必须考虑合取，而原子公式在通常的方法中就足够了。我们的研究结果表明，在实践中，证明并发约束逻辑程序的终止可能不会比其他类别的逻辑编程语言，相反，在文献中担心。
We adapt and extend existing approaches to termination in rule-based languages (logic programming and rewriting systems) to prove termination of actually implemented CHR constraint solvers. CHR (Constraint Handling Rules) are a declarative language especially designed for writing constraint solvers. CHR are a concurrent constraint logic programming language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. The approach allows to prove termination of many constraint solvers, from Boolean and arithmetic to terminological and path-consistent constraints. Because of multi-heads, our termination orders must consider conjunctions, while atomic formulas suffice in usual approaches. Our results indicate that in practice, proving termination for concurrent constraint logic programs may not be harder than for other classes of logic programming languages, contrary to what has been feared in the literature.