TY - JOUR

T1 - Higher-Order Unification

T2 - A structural relation between Huet's method and the one based on explicit substitutions

AU - de Moura, F. L C

AU - Ayala-Rincón, Mauricio

AU - Kamareddine, Fairouz

PY - 2008/3

Y1 - 2008/3

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

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

KW - Calculi of explicit substitutions

KW - Higher-Order Unification

UR - http://www.scopus.com/inward/record.url?scp=38749146471&partnerID=8YFLogxK

U2 - 10.1016/j.jal.2006.10.001

DO - 10.1016/j.jal.2006.10.001

M3 - Article

VL - 6

SP - 72

EP - 108

JO - Journal of Applied Logic

JF - Journal of Applied Logic

SN - 1570-8683

IS - 1

ER -