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

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 λσ-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 λσ-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 λσ-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 λσ-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 λσ-HOU is a generalization of Huet's algorithm and that solutions computed by the latter are always computed by the former method.     

The Weak Normalization of the Simply Typed {lambda}se-calculus

In this paper, we show the weak normalization (WN) of the simply-typeds_e-calculus with open terms where abstractions are decoratedwith types, and metavariables, de Bruijn indices and updatingoperators are decorated with environments. We show a proof ofWN using the _e-calculus, a calculus isomorphic to . This proof is strongly influenced by Goubault-Larrecq'sproof of WN for the -calculus but with subtle differences whichshow that the two styles require different attention. Furthermore,we give a new calculus '_e which works like s_e but which iscloser to than _e. For both _e and '_e we prove WN for typedsemi-open terms (i.e. those which allow term variables but nosubstitution variables), unlike the result of Goubault-Larrecqwhich covered all open terms.