La relation →β (en abrégé, →) est une règle de calcul, elle permet de simplifier des termes jusqu’à obtenir un terme qu’on ne peut plus simplifier. Un tel terme, sur lequel on ne peut pas appliquer la règle (β), est appelé une forme normale. Deux questions se posent immédiatement: 1. ce processus termine-t-il toujours, autrement dit aboutit-on toujours à une forme normale ? 2. la forme normale est-elle unique ? En général, combien a-t-on de formes normales d’un même terme ?
La première question a en fait une réponse négative:
Preuve : Considérons Ω =def (λ x · xx) (λ x · xx) (on a le droit d’écrire une chose pareille, oui). Il ne contient qu’un rédex, lui-même. Le contracter redonne Ω, ce qui signifie que la seule réduction (maximale) à partir de Ω est la boucle:
| Ω → Ω → … → Ω → … |
qui ne termine pas. ♦
Non seulement elle ne termine pas, mais en fait Ω n’a même pas de forme normale.
Si cette dernière phrase a l’air curieuse, c’est qu’il faut formaliser nos concepts:
Un terme u est faiblement normalisant si et seulement si au moins une réduction partant de u est finie.
Donc Ω n’est non seulement pas fortement normalisant, il n’est même pas faiblement normalisant.
Tous les termes fortement normalisants sont faiblement normalisants, mais le contraire n’est pas vrai:
Tant pis pour la terminaison, et en fait c’est normal: n’importe quel langage de programmation (sauf quelques rares exceptions) permet d’écrire des programmes qui bouclent, et ne terminent donc jamais.
La deuxième question est alors: en supposant u faiblement normalisant — autrement dit, u a au moins une forme normale —, cette forme normale est-elle unique ? Cette question a, elle, une réponse affirmative. C’est une conséquence des résultats qui suivent: Si u →* v1 et u →* v2, alors il existe w tel que v1 →* w et v2 →* w. Nous démontrerons ce résultat à la fin de cette section.
On utilisera pour écrire ce théorème la notation diagrammatique plus parlante:
où les lignes pleines indiquent des réductions universellement quantifiées, et les lignes pointillées des réductions dont l’existence est affirmée. Les astérisques sur les flèches dénotent la clôture réflexive transitive.
Une technique de preuve qui marche presque est la suivante. On vérifie par énumération exhaustive de tous les cas que:
c’est-à-dire que la relation → est localement confluent. Noter que u se réduit ici vers v1 ou v2 en une étape.
Puis on colle autant de ces petits diagrammes qu’il en faut pour obtenir:
mais ça ne marche pas: les petits diagrammes à mettre à l’intérieur du cône ci-dessus ne se recollent pas bien les uns aux autres. En fait, supposons qu’on ait quatre termes a, b, c, d tels que a → b, b → a, a → c et b → d et c et d sont normaux et distincts, alors on aurait a → c d’un côté, et a →* d (en passant par b). Mais c et d étant normaux et distincts, il n’existe pas de w tel que c →* w et d →* w, et le théorème serait faux. Pourtant, on peut vérifier qu’on a tous les “petits diagrammes” ci-dessus:
On peut réparer ce défaut lorsque la relation → termine… ce qui ne sera malheuresement pas le cas du λ-calcul:
Alors → est confluente.
Preuve : Comme → termine, on dispose du principe de récurrence le long de →: pour démontrer une propriété P des éléments u de A, il suffit de la démontrer sous l’hypothèse (dite de récurrence) que (*) P (v) est vraie pour tout v tel que u → v. (Il n’y a pas besoin de cas de base séparé: lorsque u est normal, (*) est trivialement vérifiée, et l’on doit donc vérifier que P (u) est vrai pour tout élément normal.)
En effet, supposons le contraire, c’est-à-dire qu’il existe une propriété P telle que pour tout u, si (*) P (v) est vraie pour tout v tel que u → v, alors P (u) est vraie; mais qu’il existe un élément u0 tel que P (u0) soit fausse. On note qu’il existe nécessairement un u1 tel que u0 → u1 et tel que P (u1) soit faux: sinon, (*) impliquerait que P (u0) soit vrai. De même, il existe un u2 tel que u1 → u2 et P (u2) est faux. Par récurrence sur k, on en déduit l’existence d’une réduction infinie u0 → u1 → … → uk → … où P (uk) est faux: contradiction.
Soit u →* v1 et u →* v2. Montrons que v1 et v2 ont un réduit commun, par récurrence sur u le long de →. Si la longueur de réduction de u à v1 vaut 0, c’est évident (prendre v2), et de même si la longueur de réduction de u à v2 vaut 0. Sinon, les deux réductions données se décomposent en u → u1 →* v1 et u → u2 →* v2 respectivement, et l’on a:
où le losange du haut est par l’hypothèse de confluence locale, et les deux plus bas sont par hypothèse de récurrence, sur u1 et u2 respectivement. ♦
Il y a différentes techniques pour montrer le théorème [Bar84]. Une de celles-ci est donnée à l’exercice 8.
)
On définit une nouvelle règle de réduction ⇒
par:
Autrement dit, ⇒ est la plus petite relation binaire vérifiant ces conditions et contenant le α-renommage. Vérifier que:
Montrer que → ⊆ ⇒ ⊆ →*, et en déduire le théorème 1.
Pour démontrer le théorème 1, nous allons passer par le théorème dit des développements finis. Ceci introduira au passage une technique de démonstration de la terminaison qui formera la base de techniques plus avancées que l’on verra en partie 2.
Considérons pour ceci le calcul suivant, qu’on appellera le λ*-calcul. Les λ*-termes sont définis par la grammaire:
| Λ* ::= V ∣ Λ* Λ* ∣ λ V · Λ* ∣ (λ* V · Λ*) Λ* |
de nouveau, à α-équivalence près. Il y a une construction supplémentaire par rapport au λ-calcul: la construction (λ* x · u) v. Attention: ceci n’est pas l’application d’un terme de la forme λ* x · u à v: il n’y a tout simplement pas de terme de la forme λ* x · t dans le langage. La notation peut prêter à confusion, donc, et il serait peut-être plus clair de noter la construction (λ* x · u) v sous une forme plus proche de la notation OCaml let x=v in u. Néanmoins, nous conservons la notation (λ* x · u) v par commodité: la technique qui consiste à effacer les étoiles, que nous utiliserons ci-dessous, est bien plus simple à expliquer avec cette notation. Formellement, l’effacement d’étoiles est la fonction E définie par:
| E (x)=x E (uv) = E (u) E (v) E (λ x · u) = λ x · E (u) E ((λ* x · u) v) = (λ x · E (u)) E (v) |
Le λ*-calcul n’a qu’une règle de réduction, la β*-réduction:
| (β*) (λ* x· u) v → u [x:=v] |
On notera que, du coup, (λ x · u) v n’est jamais un rédex en λ*-calcul.
Preuve : Nous allons tenter de montrer que le λ*-terme t est fortement normalisant par récurrence structurelle sur t. Ceci échoue lorsque t est de la forme (λ* x · u) v, il est possible que t se réduise en (λ* x · u′) v′ avec u →* u′, v →* v′, puis en u′ [x:=v′], sur lequel on ne sait plus rien dire.
À la place, nous allons montrer que t σ est fortement normalisant pour toute substitution σ fortement normalisante. Une substitution est une liste [x1:=t1, …, xn:=tn] où les variables x1, …, xn sont deux à deux disjointes. L’application de la substitution à t est définie comme pour la substitution ordinaire: xi σ = ti (1≤ i≤ n), y σ = y pour toute variable hors de {x1, …, xn}, (st) σ = (s σ) (t σ), et (λ x · t) σ = λ x · (t σ), où x n’est libre dans aucun ti, et est différent de xi, pour tout i, 1≤ i ≤ n. On notera qu’il s’agit d’une substitution parallèle, et qu’en général, par exemple, t [x1:=t1, x2:=t2] ≠ t [x1:=t1] [x2:=t2]. La substitution σ est fortement normalisante si et seulement si tous les ti le sont, 1≤ i≤ n.
On démontre que t σ est fortement normalisant pour toute substitution fortement normalisante, par récurrence structurelle sur t.
♦
Il est facile, quoique pénible, de vérifier que la β*-réduction est localement confluente. Par le lemme de Newman (lemma 2), tout λ*-terme u a donc une unique forme normale u↓. Remarquons que u ↓ ne peut pas contenir d’étoile: les étoiles apparaissent uniquement sur les β*-rédex. Donc u ↓ est en fait un λ-terme. Définissons une relation →1 sur les λ-termes par: u →1 v si et seulement s’il existe un λ*-terme u′ tel que u = E (u′) et v = u′↓. Ceci revient à ajouter des étoiles sur certains rédex de u, puis à les réduire jusqu’à ce que tous aient été éliminés.
La relation →1 est fortement confluente (voir l’exercice 7). En effet, si u →1 u1 et u →1 u2, c’est qu’on peut rajouter des étoiles à certains rédex de u de sorte que le λ*-terme obtenu se réduise en u1, et des étoiles à certains rédex (en général différents) de u de sorte que le λ*-terme obtenu se réduise en u2. Pour fixer les idées, imaginons que l’on colorie les étoiles: les étoiles ajoutées dans le premier cas sont bleues, celles du second cas sont rouges. Il est facile de vérifier que, si l’on pose u′ le terme où l’on a rajouté à la fois les étoiles bleues et les étoiles rouges, alors la réduction u →1 u1 se relève en une réduction de u′ vers un terme u′1 qui est u1, avec possiblement des étoiles rouges ici ou là; et que de même u′ se réduit en λ*-calcul à un terme u′2 qui est u2 avec des étoiles bleues ici ou là. Comme le λ*-calcul est confluent et terminant, u′1 et u′2 ont la même forme normale pour (β*), disons v: mais alors u1 →1 v et u2 →1 v.
Preuve : Comme →1 est fortement confluente, elle est confluente (exercice 7). Or → ⊆ →1 ⊆ →*: si u → v, alors il suffit de poser une étoile sur l’unique rédex contracté, ce qui montre que u →1 v; si u →1 v, alors u′ →* v en λ*-calcul pour un certain u′ tel que E (u′) = u; mais l’effacement des étoiles s’étend aux réductions, montrant que u →* v.
Donc si u →* v1 et u →* v2, on a u →1* v1 et u →1* v2. Comme →1 est confluente, il existe un w tel que v1 →1* w et v2 →1* w. On en déduit v1 (→*)* w, donc v1 →* w, et de même v2 →* w. ♦
Preuve : Par le théorème 1, il existe w tel que u1 →* w et u2 →* w. Comme ui est normal (i ∈ {1, 2}), ui →* w implique ui = w. Donc u1 = u2. ♦
Donc si l’on estime que la valeur d’un programme u est sa forme normale (par exemple, la valeur de (λ x · x+1) 4 serait 5, en supposant que 4+1 →* 5 et que 5 est normal), alors ce corollaire nous permet d’affirmer qu’en effet cette valeur est uniquement définie.
La question que nous abordons maintenant est de savoir quelles fonctions on peut représenter en λ-calcul. Dans nos exemples, nous avons souvent utilisé des symboles qui ne faisaient pas partie du vocabulaire du λ-calcul pur, comme +, 1, 4 ou 5. Il y a deux façons de les intégrer dans le langage:
On va commencer par coder les entiers naturels dans le λ-calcul. Il y a plusieurs façons de le faire, mais la plus simple et la plus connue est d’utiliser les entiers de Church:
On pose d’autre part:
L’entier de Church ⌈n⌉ est donc la fonctionnelle qui prend une fonction f et un argument x, et qui retourne f composée n fois appliquée à x.
On sait donc calculer sommes, produits et exponentielles:
On dispose aussi des booléens. Pour les coder, l’idée c’est qu’un booléen sert à faire des tests if …then …else. Si on choisit V =def λ x,y · x pour le vrai et F =def λ x,y · y, on voit que le test “if b then x else y” se représente juste par l’application b x y. En effet, “if V then x else y” est V x y, qui se réduit en x, et “if F then x else y” est F x y, qui se réduit en y.
On peut donc presque coder la factorielle, l’exemple du début de ce chapitre. Pour cela, il nous manque quand même quelques ingrédients, notamment le test d’égalité entre entiers et le calcul du prédécesseur n−1 d’un entier n. C’est le sujet des exercices qui suivent.
)
On veut définir une fonction prédecesseur, c’est-à-dire un
λ-terme P tel que P (S ⌈n⌉) →* ⌈n⌉
pour tout entier n. Par convention, on posera que P (⌈0⌉) →* ⌈0⌉.Montrer que P =def λ k · π2 (k (λ s · ⟨ S (π1 s), π1 s ⟩) ⟨ ⌈0⌉, ⌈0⌉ ⟩) est une fonction prédecesseur acceptable (effectuer une récurrence sur n). Décrire intuitivement comment le prédécesseur est calculé étape par étape. Que pensez-vous de l’efficacité de l’algorithme ?
|
|
)
Étant donnés deux termes a et b dans lesquels x n’est
pas libre, et posant F =def λ f, g · gf, on définit
Ga,b =def λ n, m · n F (λ x · a) (m F
(λ x · b)). Montrer que:
|
Il nous manque enfin un ingrédient pour pouvoir coder la factorielle (et en fait n’importe quelle fonction calculable sur les entiers): la récursion. C’est un point délicat, et nous allons venir à la solution par étapes.
On veut définir ⌈fact⌉ comme une fonction d’elle-même, autrement dit on veut:
| ⌈fact⌉ =βλ n · ⌈if⌉ (⌈zero?⌉ n) ⌈1⌉ (⌈×⌉ n (⌈fact⌉ (P n))) |
où ⌈if⌉ b x y abrège bxy, dans un but de lisibilité. Il s’agit d’une équation à résoudre, et son côté droit est une fonction de l’inconnue ⌈fact⌉. En fait, on peut même écrire le côté droit sous la forme F ⌈fact⌉, où F est le λ-terme:
| λ f · λ n · ⌈if⌉ (⌈zero?⌉ n) ⌈1⌉ (⌈×⌉ n (f (P n))) |
(On a renommé l’inconnue ⌈fact⌉ par une variable f.)
Notre équation devient alors: ⌈fact⌉ =βF ⌈fact⌉. Ce genre d’équation est appelé une équation de point fixe, car si ⌈fact⌉ en est une solution, elle est par définition un point fixe de la fonction représentée par le λ-terme F.
Le miracle du λ-calcul est que tous les termes ont des points fixes; encore mieux, ces points fixes sont définissables dans le λ-calcul lui-même:
En fait, il existe un λ-terme Y sans variable libre tel que pour tout F, Y F soit un point fixe de F. Un tel Y est appelé un combinateur de point fixe.
Preuve : Ce théorème est surprenant, mais voyons comment on peut le démontrer, en utilisant le fait que nous connaissons déjà un terme qui boucle, à savoir Ω =def (λ x · xx) (λ x · xx).
On veut que Y F =βF (Y F), pour tout F, donc en particulier lorsque F est une variable. On peut donc définir Y sous la forme λ f · A (f), où A (f) est un terme à trouver de variable libre f. Ce qui faisait boucler Ω, c’était une savante dose d’auto-application. On va réutiliser l’astuce, et essayer de trouver A (f) sous la forme de l’application d’un terme B (f) à lui-même. Autrement dit, on veut que B (F) (B (F)) =βF (B (F) (B (F))). Pour cela, on va supposer que le premier B (F) à gauche est une abstraction λ x · u, et que u est l’application de F à un terme inconnu, de sorte à obtenir le F en tête de F (B (F) (B (F))). En somme, on suppose que B (F) =def F (C (F, x)), où C (F, x) est un terme à trouver. En simplifiant juste le rédex de gauche, ceci se ramène à F (C (F, B (F))) =βF (B (F) (B (F))), ce qui sera réalisé dès que C (F, B (F)) = B (F) (B (F)). On peut par exemple poser C (f, x) = xx. En résumé, on a trouvé le combinateur de point fixe:
| Y =def λ f · (λ x · f (xx)) (λ x · f (xx)) |
Ce combinateur s’appelle le combinateur de point fixe de Church. ♦
On notera que Y F =βF (Y F), mais il est faux que Y F →* F (Y F). Il arrive que l’on souhaite cette dernière réduction. En fait, c’est réalisable: le combinateur Θ de point fixe de Turing a comme propriété que Θ F →* F (Θ F).
On peut l’obtenir par un raisonnement similaire, c’est-à-dire en utilisant un choix d’arguments parmi: 1. si on veut ab →* c et a est inconnu, alors on peut choisir a sous forme d’une abstraction; 2. si on veut a →* f(b) et a est inconnu, où f est une variable, on peut choisir a de la forme f (c), avec c à trouver tel que c →* b; 3. on peut toujours choisir un terme inconnu a de la forme bb, avec b à trouver.
Voici le raisonnement menant au combinateur de Turing. Ce qui faisait boucler Ω, c’était une savante dose d’auto-application. On va réutiliser l’astuce, et essayer de trouver Θ sous la forme de l’application d’un terme A à lui-même. On cherche donc A tel que AAF →* F (AAF). Pour que AAF se réduise, quel que soit F, donc même lorsque F est une variable, il est raisonnable de penser que A va devoir s’écrire λ g · B(g) pour un certain terme B(g) à trouver ayant g pour variable libre. Alors AAF → B (A) F, qui doit se réduire en F appliqué à quelque chose. On va donc choisir B(g) =def λ h · h (C (g,h)), où C (g,h) est à trouver. Ce faisant, AAF → B(A) F = (λ h · h (C (A, h))) F → F (C (A, F)), et une solution est alors de définir C (A, F) =def AAF, autrement dit C (g, h) =def ggh. En résumé, on obtient:
| Θ =def (λ g, h · h (ggh)) (λ g, h · h (ggh)) |
La découverte de combinateurs de points fixes est un exercice de voltige, et si vous n’avez pas tout suivi, essayez simplement de vérifier que Y F =βF (Y F) pour tout F, et que Θ F →* F (Θ F) pour tout F.
Il est aussi clair que l’on ne codera pas les fonctions récursives dans une réalisation informatique du λ-calcul par l’utilisation de Y ou de Θ tels que définis ci-dessus. Par contre, on supposera souvent qu’on a un mécanisme permettant de réécrire Y F en F (Y F), pour Y un terme sans variable libre fixé à l’avance (typiquement une constante que l’on aura rajouté au langage). Ce mécanisme ne change rien aux propriétés du λ-calcul, car on peut le coder dans le λ-calcul lui-même: c’est tout l’intérêt des constructions du théorème 2.
)
On code les listes de termes comme suit. La liste u1, …,
un est représentée par [u1, …, un] =def λ f, x
· f u1 (f u2 … (f un x) …). En particulier, la
liste vide est ⌈nil⌉ =def λ f,x · x, et la
fonction ⌈cons⌉ qui prend un élément u0 et une liste
[u1, …, un] et retourne [u0, u1, …, un] est
⌈cons⌉ =def λ a, l, f, x · f a (l f x).Montrer que ⌈hd⌉ =def λ l · l (λ y,z · y) ⌈nil⌉ est telle que:
|
et donc calcule le premier élément de la liste en argument, quand elle est non vide.
Montrer que ⌈map⌉ =def λ g, l · l (λ a, l′ · ⌈cons⌉ (g a) l′) ⌈nil⌉ est telle que:
| ⌈map⌉ g [u1, …, un] =β[g u1, …, g un] |
(On pourra utiliser le fait que si l = [u1, u2, …, un], alors l h r =βh u1 (l′ h r), où l′ = [u2, …, un], et effectuer une récurrence sur n.)
Montrer que ⌈tl⌉ =def λ l · π2 (l (λ s, p · ⟨ ⌈cons⌉ s (π1 p), π1 p ⟩) ⟨ ⌈nil⌉, ⌈nil⌉ ⟩) envoie la liste [u1, u2, …, un] vers [u2, …, un]. (Ceci est analogue au codage du prédécesseur dans les entiers.)
Que fait ⌈app⌉ =def λ l, l′ · l ⌈cons⌉ l′ ?