Substitutions explicites et unification d'ordre supérieur

Abstract : Lambda-calculi with explicit substitutions allow to handle formally substitutions. They constitute a bridge between lambda-calculus and programs. Our contribution is two-folded. The first part study an explicit eta-reduction rule, the second part concerns higher order unification. The beta-reduction of lambda-calculus distinguishes sorne functions which are extensionally equal. Adding an eta-réduction rule gives an extensional equality. We define and study an effective eta rule, independent of a specifie explicit substitutions system. This leads us to an unconditional eta-rule. We prove that the generated reduction is a conservative extension of beta-eta-réduction on the set of lambda-te'rms typable with intersection. Higher order unification consists in solving equations between sim ply typed lambda-terms. The classical procedure is expressed in ordinary lambda-calculus. Hence checking its implementation is difficult. Explicit substitutions allows to describe formally the procedure at a lower level. A previous approach is based on lambda-sigma' and relies on composition and open confluence. Our approach, based on lambda-upsilon, proves that neither composition nor open confluence is needed.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_1997_0251_BRIAUD.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01747461
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:00:36 AM
Last modification on : Monday, April 16, 2018 - 10:40:39 AM

Identifiers

  • HAL Id : tel-01747461, version 1

Collections

Citation

Daniel Briaud. Substitutions explicites et unification d'ordre supérieur. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10251⟩. ⟨tel-01747461⟩

Share

Metrics

Record views

1