1  Introduction au λ-calcul

Le λ-calcul a été inventé par le logicien américain Alonzo Church dans les années 1930, dans l’espoir de fournir un fondement au mathématiques plus simple que la théorie des ensembles, et fondé sur la notion de fonction. Ce programme a échoué, car le λ-calcul a un pouvoir d’expression beaucoup plus faible; en revanche, le λ-calcul a exactement le même pouvoir d’expression que les machines de Turing par exemple, ce qui en fait un bon choix pour fonder la notion de fonction calculable. La bible du λ-calcul est le livre de Barendregt [Bar84].

1.1  Syntaxe

Les trois constructions principales du λ-calcul sont:

• la variable (il faut bien commencer quelque part): nous les noterons x, y, z, etc.
• l’application: si u et v sont deux programmes, on peut considérer u comme une fonction et v comme un argument possible, et former l’application uv. Ceci correspond à la notation mathématique usuelle u(v) tout en nous économisant quelques parenthèses. On remarquera qu’il n’y a pas de contraintes de typage ici, et qu’il est donc tout à fait légal de former des auto-applications xx, par exemple.
• l’abstraction: si u est un programme dépendant (ou non) de la variable x, alors on peut former un nouveau programme λ x · u, qui représente la fonction qui à x associe u.

Par exemple, λ x · x+1 est intuitivement la fonction qui à x associe x+1 — sauf que + et 1 ne font pas partie du vocabulaire décrit ci-dessus, un point sur lequel nous reviendrons.

Formellement, fixons-nous un ensemble V infini dénombrable dit de variables. On définit l’ensemble Λ des λ-termes s, t, u, v, …, comme étant le plus petit tel que V ⊆ Λ, si u et v sont dans Λ alors uv est dans Λ, et si x∈ V et u est dans Λ alors λ x · u est dans Λ. Ou, sous forme de déclaration de grammaire:

On autorisera l’usage de parenthèses pour désambigüer les expressions. D’autre part, les abstractions s’étendent aussi loin qu’il leur est permis, ce qui signifie en particulier que λ x · u v dénote λ x · (u v) et non (λ x · u) v. La notation u u₁ … u_n dénotera u si n=0, et sinon ( … ((u u₁) u₂) … u_n), quant à la notation λ x₁, …, x_n · u, elle abrégera λ x₁ · … · λ x_n · u.

L’intérêt de ces deux dernières notations est que, bien que toutes les fonctions du λ-calcul soient unaires (ne prennent qu’un argument), on peut simuler les fonctions d’arité quelconque par currification: la fonction λ x · λ y · x+y, par exemple, est la fonction qui prend un x en argument, et retourne une fonction qui prend un y en argument et retourne x+y; autrement dit, c’est la fonction qui prend x, y et retourne leur somme.

1.2  Calculs et réduction

Il s’agit maintenant de donner un sens à ces λ-termes. Une première observation simple est que nous voudrions que λ x · x+1 et λ y · y+1 dénotent la même fonction: que l’argument s’appelle x ou y, c’est toujours la fonction qui ajoute 1 à son argument. On va donc vouloir confondre les deux termes. Supposons pour cela que nous sachions ce que veut dire remplacer une variable x par un terme v dans un terme u, et notons u [x:=v] le résultat. L’égalité entre deux termes dont seuls les noms des variables d’entrée diffèrent s’exprime alors par la règle suivante, dite d’α-renommage:

ce qui définit une relation binaire α. Notons =_α la plus petite congruence contenant α, autrement dit la plus petite relation telle que u α v implique u =_αv, =_α est réflexive, symétrique, transitive et passe au contexte: u₁ =_αu₂ et v₁ =_αv₂ impliquent u₁ v₁ =_αu₂ v₂, et u =_αv implique λ x · u =_αλ x · v.

Pour plus de simplicité, nous quotientons implicitement Λ par =_α, de sorte que λ x · x+1 et λ y · y+1 seront en fait vus comme deux termes identiques.

Sémantiquement, la règle importante est la β-réduction:

qui exprime que si on applique la fonction qui à x associe u à l’argument v, on obtient la même chose que si on calcule directement u avec x remplacé par v. Par exemple, (λ x · x+1) 4  β  4+1.

Nous noterons →_β, ou plus souvent →, la plus petite relation contenant β qui passe au contexte. Nous noterons →^* sa clôture réflexive transitive: u →^* v si et seulement s’il existe n ≥ 0, et n+1 termes u₀, u₁, …, u_n tels que u = u₀ → u₁ → … → u_n = v. Nous noterons →⁺ la clôture transitive de →: la définition est similaire, mais avec n > 0. Finalement, deux termes u et v sont β-équivalents si et seulement si u =_βv, où =_β est la plus petite congruence contenant β.

Mais avant d’aller plus avant, il faut d’abord réaliser que la notion de remplacement, ou substitution u [x:=v] n’est pas aussi simple qu’elle y paraît. Par exemple, si vous utilisez la notion de remplacement textuel, fourni par la commande de recherche et de remplacement de n’importe quel éditeur de texte, vous allez obtenir une absurdité:

mais λ uv · y n’est pas un terme légal, uv n’étant pas une variable. Le remède est simple: ne remplaçons pas les variables qui suivent un λ, que l’on considère comme des variables liées. Mais ça ne résout pas tout:

Dans le premier exemple ci-dessus, le fait de remplacer x par y dans la fonction identité λ x · x a produit la fonction constante qui retourne toujours y. Dans le deuxième exemple, c’est le contraire qui se produit.

Le problème dans le premier exemple, c’est que nous avons remplacé une occurrence de la variable x qui était liée par l’en-tête λ x: nous devons donc exclure ce cas. Dans le second, c’est plus subtil: nous avons remplacé une variable non liée y par un terme qui contient une variable libre x (autrement dit, pas dans la portée d’un en-tête d’abstraction), qui si l’on remplace y par x, va se retrouver subrepticement liée par le λ x au-dessus.

Pour éviter ces problèmes, nous conviendrons que les termes sont toujours préalablement α-renommés de sorte à éviter ces problèmes. Formellement (et nous revenons pour cela à la notion de termes hors α-renommage):

Formellement, on définit en fait →_β comme la plus petite relation contenant β et =_α qui passe au contexte, et de même pour →_β^*, →_β⁺, =_β.

L’exercice suivant montre que l’on peut essentiellement faire comme s’il n’y avait aucun problème dans la définition de la substitution, pourvu que l’on s’arrange toujours pour remplacer u par un α-équivalent avant substitution, et que l’on raisonne toujours modulo α-équivalence. C’est ce que nous supposerons toujours dans la suite.

Nous considérerons aussi de temps en temps la règle d’η-contraction:

qui exprime que, lorsque u ne dépend pas de x, la fonction qui à x associe u de x est exactement u elle-même. Par exemple, la fonction λ x · len x, où len est la fonction longueur sur les listes, est len elle-même. Curieusement, (η) est indépendante des relations précédentes, et notamment λ x · ux ≠_βu lorsque x∉fv(u) en général. On note →_βη, →_βη^*, =_βη la plus petite relation contenant β, η et =_α, sa clôture réflexive transitive, sa clôture transitive et la plus petite congruence la contenant respectivement.

Une occurrence d’un sous-terme de la forme (λ x · u) v dans un terme t est appelé un β-rédex dans t. (Ce mot vient de l’anglais “redex”, abréviation de “reduction expression”.) Dire que t → s signifie que s est obtenu à partir de t (modulo α-renommage) en remplaçant un rédex (λ x · u) v par son contractum u [x:=v].

Le but de l’exercice suivant est de montrer qu’un terme peut contenir zéro, un ou plusieurs rédex.