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
Abstract
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.