Unification via λse-style of explicit substitution

Mauricio Ayala-Rincón, Fairouz Kamareddine

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 ?s-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 ?s-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 ?s-style of explicit substitution.

Original languageEnglish
Title of host publicationProceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages163-174
Number of pages12
Publication statusPublished - 2000
EventProceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) - Montreal, Que., Canada
Duration: 20 Sep 200023 Sep 2000

Conference

ConferenceProceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)
CountryCanada
CityMontreal, Que.
Period20/09/0023/09/00

Keywords

  • Explicit substitution
  • Higher order unification
  • Lambda-calculus

Fingerprint Dive into the research topics of 'Unification via λs<sub>e</sub>-style of explicit substitution'. Together they form a unique fingerprint.

  • Cite this

    Ayala-Rincón, M., & Kamareddine, F. (2000). Unification via λse-style of explicit substitution. In Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (pp. 163-174)