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
SN - 1570-8683
VL - 6
SP - 72
EP - 108
JO - Journal of Applied Logic
JF - Journal of Applied Logic
IS - 1
ER -