A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
复制标题
方程约束列表的幂等 MGU 公理的机器检查模型
DOI：
10.4204/eptcs.42.3
复制
发表时间：
2010
影响因子：
7.4
通讯作者：
J. Caldwell
中科院分区：
文献类型：
--
作者：
Sunil Kothari;J. Caldwell
我们提出了形式化的证明，验证了一阶统一算法定义的可满足的约束列表生成一个最一般的统一（MGU），这也恰好是幂等的。我们所有的证明都在Coq定理证明器中得到了形式化。我们的证明表明，由统一算法产生的有限映射提供了一个模型的公理表征幂等MGU的约束列表。作为我们验证的基础的公理是从一个标准集通过将它们扩展到约束列表而得出的。对我们来说，约束是简单类型语言中术语之间的等式。使用Coq库Coq.FSets.FMapInterface将替换正式建模为有限映射。Coq的函数归纳法是证明许多公理的主要证明技术。
We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. All of our proofs have been formalized in the Coq theorem prover. Our proofs show that finite maps produced by the unification algorithm provide a model of the axioms characterizing idempotent MGUs of lists of constraints. The axioms that serve as the basis for our verification are derived from a standard set by extending them to lists of constraints. For us, constraints are equalities between terms in the language of simple types. Substitutions are formally modeled as finite maps using the Coq library Coq.FSets.FMapInterface. Coq's method of functional induction is the main proof technique used in proving many of the axioms.