Higher Order Unification via Lambda-s-e-Style of Explicit Substitution

Mauricio Ayala-Rincon and Fairouz Kamareddine

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


A higher order unification (HOU) method based on the lambda-s-e-style of explicit substitution is proposed. The method is influenced by the treatment introduced by Dowek, Hardin and Kirchner using the lambda-sigma-style of explicit substitution. Correctness and completeness properties of the proposed approach are shown and advantages of the method, inherited from the qualities of the lambda-s-e-calculus, are pointed out. Our method needs only one sort of objects: terms. And in contrast to the HOU approach based on the lambda-sigma-calculus, it avoids the use of substitution objects. This makes our method closer to the syntax of the lambda-calculus. Furthermore, detection of redices depends on the search for solutions of simple arithmetic constraints which makes our method more elegant than the one based on the lambda-sigma-style of explicit substitution.