Substitution explicite

vignette|M[s] est la notation d'une substitution explicite Un calcul de substitutions explicites est une extension du lambda-calcul dans lequel la substitution est intégrée au calcul au même titre que le sont l'abstraction ou l'application, alors que dans le lambda-calcul, la substitution fait partie de la métathéorie, c'est-à-dire qu'elle est définie en dehors de la théorie du lambda-calcul. L'idée qui conduit à expliciter les substitutions vient du souhait de traiter la substitution comme une opération à part entière du calcul en l'intégrant dans la syntaxe et en y adjoignant un certain nombre de règles qui distribuent et appliquent la substitution et qui font partie du calcul au même titre que la β-réduction fait partie du lambda-calcul. L'intérêt d'intégrer la substitution dans le calcul est de pouvoir parler de la substitution aussi bien en termes d'implantation, de complexité, d'efficacité ou de stratégie d'évaluation que dans ses rapports avec la β-réduction. On peut ainsi expliquer le partage, l'évaluation retardée ou paresseuse ou l'évaluation immédiate. Une substitution qui apparaît dans un terme peut-être évaluée immédiatement ou son évaluation peut être remise à plus tard, à un moment où on aura besoin d'elle. De plus, l'évaluation d'une substitution peut servir à plusieurs endroits et ne nécessiter qu'un seul calcul (partage). 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.