Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions

F. L C de Moura, Mauricio Ayala-Rincón, Fairouz Kamareddine

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

We compare two different styles of Higher-Order Unification (HOU): the classical HOU algorithm of Huet for the simply typed ?-calculus and HOU based on the ?s-calculus of explicit substitutions. For doing so, first, the original Huet algorithm for the simply typed ?-calculus with names is adapted to the language of the ?-calculus in de Bruijn's notation, since this is the notation used by the ?s-calculus. Afterwards, we introduce a new structural notation called unification tree, which eases the presentation of the subgoals generated by Huet's algorithm and its behaviour. The unification tree notation will be important for the comparison between Huet's algorithm and unification in the ?s-calculus whose derivations are presented into a structure called derivation tree. We prove that there exists an important structural correspondence between Huet's HOU and the ?s-HOU method: for each (sub-)problem in the unification tree there exists a counterpart in the derivation tree. This allows us to conclude that the ?s-HOU is a generalization of Huet's algorithm and that solutions computed by the latter are always computed by the former method. © 2006 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)72-108
Number of pages37
JournalJournal of Applied Logic
Volume6
Issue number1
DOIs
Publication statusPublished - Mar 2008

Keywords

  • Calculi of explicit substitutions
  • Higher-Order Unification

Fingerprint Dive into the research topics of 'Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions'. Together they form a unique fingerprint.

  • Cite this