A Machine-Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction
Sunil Kothari · 2009
Abstract. The most general unifier (MGU) of a pair of terms can be specified by four axioms. In this paper we generalize the standard presentation of the axioms to specify the MGU of a list of equational constraints and we formally verify that the unification algorithm satisfies the axioms. Our constraints are equalities between terms in a language of simple types. We model substitutions as finite maps from the Coq library Coq.FSets.FMapInterface. Since the unification algorithm is general recursive, we show termination using a lexicographic ordering on lists of constraints. Coq’s method of functional induction is the main proof technique used in proving the axioms. 1