Substitutions explicites et unification d'ordre supérieur
Résumé
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.
Les lambda-calculs à substitutions explicites fournissent un cadre formel pour l'étude de la théorie des substitutions. Ils constituent ainsi un pont entre le lambda-calcul et les programmes. Notre contribution, composée de deux volets, porte sur l'étude en soi des lambda-calculs à substitutions explicites et sur l'emploi d'un tel calcul comme pont entre théorie et pratique. Le premier volet a pour but l'explicitation de la eta-réduction, le second a trait à l'unification d'ordre supérieur. Notre travail sur la eta-réduction se résume ainsi. La beta-réduction du lambda-calcul distingue certaines fonctions extensionnellement égales. En ajoutant la règle de eta-réduction, on obtient \ une égalité extensionnelle. Nous définissons et étudions une règle eta opératoire et indépendante d'un calcul à substitutions explicites donné. Ceci nous conduit à une variante non-conditionnelle de eta, nommée eta". Nous montrons que la réduction générée est une extension conservative de la beta-eta-réduction, cela sur l'ensemble des lambda-termes typables avec l'intersection. Le second problème qui nous intéresse, l'unification d'ordre supérieur, consiste à résoudre des équations entre lambda-termes simplement typés. Sa programmation demeure difficile à vérifier car l'algorithme classique est formellement défini au moyen de la substitution du lambda-calcul. Décrire une procédure d'unification d'ordre supérieur à l'aide de substitutions explicites établit une passerelle entre l'unification d'ordre supérieur et son implantation. Une approche précédente se fonde sur le système lambda-sigma' et s'appuie sur la composition et la confluente ouverte. Notre approche, basée sur le système lambda-upsilon, montre que ni l'une ni l'autre ne sont nécessaires pour exprimer l'unification d'ordre supérieur au moyen d'un lambda-calcul à substitutions explicites. Notre travail à ce sujet simplifie, sur plusieurs plans, les travaux précédents sur ce thème.