一种证明实际CHR程序不变量与等价性汇流的约束求解器
Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs
摘要：
一个不确定性程序的汇流确保了功能性的输入输出关系，使程序员不必考虑实际的调度策略，并允许优化和并行实现。汇流模等价的更一般的性质确保等价的输入与等价的输出相关，而不需要是相同的。不变量下的合流也被认为是。约束处理规则是基于重写的逻辑程序设计语言的一个重要例子，本文旨在给出一种可机械化的方法来证明终止程序的汇流模等价性。虽然早期的方法，融合的可编程逻辑程序关注一个理想化的逻辑子集，我们指的是一个语义与标准的基于Prolog的实现兼容。我们指定了一个元级约束语言，在其中不变量和等价可以表示和操纵，扩展我们以前的理论结果走向实际的实施。
英文摘要：
Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated, extending our previous theoretical results towards a practical implementation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
