论CHR中多重头的表达能力
计算机科学中的逻辑
2011-01-19 v6 分布式、并行与集群计算
摘要
约束处理规则（Constraint Handling Rules, CHR）是一种提交选择式声明式语言，最初设计用于编写约束求解器，如今已成为一种通用目的语言。CHR程序由多头守护规则组成，这些规则允许将约束重写为更简单的约束，直到达到已解形式。许多经验证据表明，多重头增强了语言的表达能力，但迄今为止尚未在该方向上得到形式化证明。在本文的第一部分，我们分析了CHR相对于底层约束理论的图灵完备性。我们证明，如果约束理论足够强大，那么限制为单头规则不会影响语言的图灵完备性。另一方面，与多头语言的情况不同，当底层签名（用于约束理论）不包含函数符号时，单头CHR语言不具备图灵强大性。在第二部分，我们证明，无论考虑哪种约束理论，在合理的假设下，都不可能在保持程序语义的同时将（具有多头规则的）CHR语言编码为单头语言。我们还表明，在更强的假设下，考虑规则头中原子数量的增加会增强语言的表达能力。这些结果为多重头增强CHR语言表达能力的论断提供了形式化证明。
引用
@article{arxiv.0804.3351,
title = {On the Expressive Power of Multiple Heads in CHR},
author = {Cinzia Di Giusto and Maurizio Gabbrielli and Maria Chiara Meo},
journal= {arXiv preprint arXiv:0804.3351},
year = {2011}
}
备注
v.6 Minor changes, new formulation of definitions, changed some details in the proofs