等式约束列表的幂等MGU公理的机器学习模型
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
摘要：
我们提出了形式化的证明，验证了一阶统一算法定义的可满足的约束列表生成一个最一般的统一（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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
