Skip to Main content Skip to Navigation

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 :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:00:36 AM
Last modification on : Tuesday, February 16, 2021 - 2:11:29 PM

Links full text


  • HAL Id : tel-01747461, version 1



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⟩



Record views