Substitution explicite

Pour que le système formel puisse parler à la fois d'abstraction et d'application aussi bien que de substitution, il faut enrichir la syntaxe du lambda-calcul avec un opérateur de substitution explicite. Il y a deux façons de le faire, suivant que l'on travaille avec des variables explicites ou avec des indices de de Bruijn.

• Si les variables sont explicites, on ajoute un opérateur 〈x:=N〉. Dans ce cas, la notation P〈x:=N〉 dénote l'opérateur de substitution explicite appliqué à P et signifie que l'on veut remplacer x par N dans P. On notera que dans l'expression P〈x:=N〉, 〈x:=N〉 est un lieur pour x dans P au même titre que λ est un lieur pour x dans λx.P. Cela a bien sûr une répercussion sur la notion de variable libre qui doit être libre pour λ mais aussi pour 〈x:=N〉.
• Si des indices de Bruijn sont utilisés pour coder les variables, on ajoute un opérateur [s] où s est une substitution. La notation M[s] signifie que M est modifié par la substitution s. Dans ce cas, les substitutions forment une autre sorte d'objets. Elles sont engendrées par des opérateurs spécifiques /, ⇑, ↑, décrits plus loin dans cet article.

Voici quelques propriétés que l'on souhaite voir satisfaites par un système de substitutions explicites[1]. Tout d'abord il y a des propriétés requises.

• Le système doit être confluent sur les termes clos, c'est-à-dire sur les termes qui ne contiennent pas de variables libres.
• Le système doit simuler chaque étape de β-réduction.
• Le système restreint aux substitutions seules doit être fortement normalisable, c'est-à-dire que toutes les réductions qui ne contiennent pas d'élimination de β-rédex doivent se terminer.

Il y a aussi des propriétés optionnelles que l'on peut souhaiter.

• Pour définir les règles on introduit des variables ad hoc (différentes des variables internes du système et du lambda-calcul), qui peuvent être remplacées par n'importe quel terme et que l'on appelle méta-variables, formant ainsi des méta-termes. Le système devrait être confluent sur les méta-termes.
• Le système de substitutions explicites devrait permettre de composer les substitutions.
• Le système de substitutions explicites devrait préserver la forte normalisation. Cela signifie que tout terme fortement normalisable du lambda-calcul devrait rester fortement normalisable quand on l'immerge dans la calcul de substitutions explicites.
• Le système de type du lambda-calcul s'étend et conserve ses caractéristiques comme la forte normalisation des termes typables.
• Le système devrait être simple, aussi bien du point de vue du nombre d'opérateurs, que du nombre de règles, de leur complexité et de leurs conditions annexes.

Il y a plusieurs calculs de substitutions explicites. Cela peut s'expliquer de deux façons :

• il y a différentes sortes de syntaxe: avec des variables explicites ou des variables implicites, avec des opérateurs différents,
• certaines propriétés citées plus haut sont satisfaites par un système et pas par un autre. Un système de substitutions explicites fait un compromis entre ces propriétés.

En général, les systèmes qui sont confluents sur les méta-termes ne préservent pas la forte normalisation et vice-versa. Ceux qui satisfont ces deux propriétés ne sont pas simples.

• La règle (b) élimine un β-rédex et introduit une substitution explicite.
• Dans la règle (xvI), le membre gauche est formé d'une substitution affectée à une variable. Comme la variable en question est la même que la variable de la substitution, on élimine la substitution en retournant le corps de celle-ci.
• La règle (xvK) a aussi un membre gauche formé d'une substitution affectée à une variable, mais comme les variables sont différentes, on retourne la variable.
• La règle (xap) distribue une substitution dans une application. Une bonne implantation devrait faire un partage.
• La règle (xab) fait entrer une substitution dans une abstraction.
• La règle (xvgc) évoque le glanage de cellules, d'où les deux lettres g et c. Là aussi le membre gauche est formé d'une substitution affectée à un terme qui ne contient pas la variable. On élimine la substitution en la supprimant, ce qui fait disparaître le corps de la substitution et équivaut à une récupération de mémoire c'est-à-dire un glanage de cellules.

Les trois premières règles correspondent aux règles équivalentes de lambda-x, par exemple, la règle (B) élimine un bêta-rédex et introduit une substitution explicite.

• La règle (FVar) a pour terme l'indice 0 et pour partie substitution M/, elle retourne M.
• La règle (RVar) a pour terme l'indice n+1 et pour partie substitution M/, elle décrémente l'indice et oublie M. Pour justifier cette règle, il faut se souvenir que n+1 vient de dessous un lambda qui a disparu.
• La règle (FVarLift) met en face à face un indice 0 et une opération de hissage. 0 est inchangé par le hissage.
• La règle (RVarLift) prend en compte le fait suivant : si on applique le hissage d'une substitution à un indice strictement positif on obtient un terme résultant de l'application de la substitution à l'indice précédent dans lequel tous les indices internes sont décalés, c'est-à-dire incrémentés. On notera que dans le membre droit de ce terme il y a deux applications successives de substitutions : à savoir la substitution hissée et le décalage.
• La règle (VarShift) réalise le décalage ou incrémentation.