Unification via the se-style of explicit substitutions
Maurício Ayala-Rincón · Logic Journal of IGPL · 2001
A unification method based on the λse-style of explicit substitution is proposed. This method together with appropriate translations, provide a Higher Order Unification (HOU) procedure for the pure λ-calculus. Our method is influenced by the treatment introduced by Dowek, Hardin and Kirchner using the λσ-style of explicit substitution. Correctness and completeness properties of the proposed λse-unification method are shown and its advantages, inherited from the qualities of the λse-calculus, are pointed out. Our method needs only one sort of objects: terms. And in contrast to the HOU approach based on the λσ-calculus, it avoids the use of substitution objects. This makes our method closer to the syntax of the λ-calculus. Furthermore, detection of redices depends on the search for solutions of simple arithmetic constraints which makes our method more operational than the one based on the λσ-style of explicit substitution.