4 - Higher-Order Equational Unification
Published online by Cambridge University Press: 12 January 2010
Summary
We define and discuss higher-order unification with a built-in higher-order equational theory. It subsumes unification and matching of simply typed λ-terms at all orders, and we present the major forms and their complexities down to the first-order cases.
Other forms of unification, their properties or applications are discussed in surveys by Gallier [64], and Siekmann [175, 176], and in collections of papers [110, 111].
Higher-order equational unifiability uses a definition of higher-order rewriting which can also be used for proofs in higher-order equational logic. We give soundness and completeness results for higher-order equational unification procedures which enable us to define higher-order resolution for CTT formulas of all orders. These results link unification and general model semantics.
We show that pure third-order equational matching is undecidable by a reduction from Hilbert's Tenth Problem. We discuss the open problem of the decidability of higher-order matching. Several approaches for its solution are presented. We give a higher-order matching algorithm which is sound and terminating. We also present a class of decidable pure third-order matching problems based on the Schwichtenberg-Statman characterization of the λ-definable functions on the simply typed Church numerals, a class of decidable matching problems of arbitrary order, show that pure third-order matchability is NP-hard by a reduction from propositional satisfiability, discuss resolving the Plotkin-Statman Conjecture, and consider Zaionc's treatment of regular unification problems. All of these approaches suggest that the problem is decidable.
- Type
- Chapter
- Information
- The Clausal Theory of Types , pp. 45 - 88Publisher: Cambridge University PressPrint publication year: 1993