Théorèmes principaux, confluence, expressivité

2 Théorèmes principaux, confluence, expressivité

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 ?

2.1 Terminaison

La première question a en fait une réponse négative:

Lemme 1 La β-réduction ne termine pas en général.

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:

Définition 2 Un terme u est fortement normalisant si et seulement si toutes les réductions partant de u sont finies.

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:

Exercice 6 Montrer que (λ x ⋅ y) Ω est faiblement normalisant, mais pas fortement normalisant.

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.

2.2 Confluence

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 →^* v₁ et u →^* v₂, alors il existe w tel que v₁ →^* w et v₂ →^* 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 v₁ ou v₂ 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:

Lemme 2 Soit → une relation binaire sur un ensemble A, et supposons que → est localement confluente et fortement normalisante. (Par fortement normalisante, nous entendons qu'il n'y a aucune réduction infinite partant d'aucun élément de A le long de →.)

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 u₀ tel que P (u₀) soit fausse. On note qu'il existe nécessairement un u₁ tel que u₀ → u₁ et tel que P (u₁) soit faux: sinon, (*) impliquerait que P (u₀) soit vrai. De même, il existe un u₂ tel que u₁ → u₂ et P (u₂) est faux. Par récurrence sur k, on en déduit l'existence d'une réduction infinie u₀ → u₁ → … → u_k → … où P (u_k) est faux: contradiction.

Soit u →^* v₁ et u →^* v₂. Montrons que v₁ et v₂ ont un réduit commun, par récurrence sur u le long de →. Si la longueur de réduction de u à v₁ vaut 0, c'est évident (prendre v₂), et de même si la longueur de réduction de u à v₂ vaut 0. Sinon, les deux réductions données se décomposent en u → u₁ →^* v₁ et u → u₂ →^* v₂ 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 u₁ et u₂ respectivement. ♦

Il y différentes techniques pour montrer le théorème [Bar84]. Une de celles-ci est donnée à l'exercice 8.

Exercice 7 Supposons que la relation binaire → soit fortement confluente, c'est-à-dire que si u → u₁ et u → u₂, alors u₁ et u₂ se réécrivent au même terme en au plus une étape. Montrer que → est confluente.

Exercice 8 On définit une nouvelle règle de réduction ⇒ par:

u ⇒ u pour tout terme u;
si u ⇒ u' et v ⇒ v', alors uv ⇒ u'v';
si u ⇒ u', alors λ x ⋅ u ⇒ λ x ⋅ u';
si u ⇒ u' et v ⇒ v', alors (λ x ⋅ u) v ⇒ u' [x:=v'].

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.

Lemme 3 La β^*-réduction termine.

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 [x₁:=t₁, …, x_n:=t_n] où les variables x₁, ..., x_n sont deux à deux disjointes. L'application de la substitution à t est définie comme pour la substitution ordinaire: x_i σ = t_i (1≤ i≤ n), y σ = y pour toute variable hors de {x₁, …, x_n}, (st) σ = (s σ) (t σ), et (λ x ⋅ t) σ = λ x ⋅ (t σ), où x n'est libre dans aucun t_i, et est différent de x_i, 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 [x₁:=t₁, x₂:=t₂] ≠ t [x₁:=t₁] [x₂:=t₂]. La substitution σ est fortement normalisante si et seulement si tous les t_i le sont, 1≤ i≤ n.

On démontre que t σ est fortement normalisant pour toute substitution fortement normalisante, par récurrence structurelle sur t. Lorsque t est une variable x_i, alors t σ = t_i est fortement normalisant par hypothèse. Lorsque t est une autre variable y, t σ = y est fortement normalisant. Lorsque t est une application uv, toute réduction infinie partant de tσ = (u σ) (v σ) devrait effectuer une infinité de réductions à partir de u σ ou à partir de v σ, puisque jamais aucune règle ne s'applique aux applications en λ^*-calcul (on se rappellera que la construction (λ^* x ⋅ u) v n'est pas une application). Mais, par hypothèse de récurrence, on ne peut faire qu'un nombre fini de réductions depuis u σ et depuis v σ.

Finalement, lorsque t est de la forme (λ^* x ⋅ u) v, toute réduction infinie à partir de t σ est nécessairement de la forme t σ = (λ^* x ⋅ u σ) (v σ) →^* (λ^* x ⋅ u') v' → u' [x:=v'] → …, où u σ →^* u' et v σ →^* v', et la réduction (λ^* x ⋅ u') v' → u' [x:=v'] est la première qui utilise (β^*) au sommet du terme. Une telle réduction finit nécessairement par arriver, car u σ et v σ sont fortement normalisants par hypothèse de récurrence. Mais il est facile de voir que u σ [x:=vσ] = u σ' où, si σ s'écrit [x₁:=t₁, …, x_n:=t_n], σ' est la substitution parallèle [x₁:=t₁, …, x_n:=t_n, x:=vσ]. On démontre en effet que l'égalité tient dès que x ∉{x₁, …, x_n} et x n'est libre dans aucun t_i, 1≤ i≤ n, par récurrence structurelle sur u. Or, par hypothèse σ, donc t₁, ..., t_n sont fortement normalisants; v σ est fortement normalisant par hypothèse de récurrence; donc σ' est fortement normalisante, ce qui permet d'affirmer que u σ' est fortement normalisant, de nouveau par hypothèse de récurrence. Or u σ' = u σ [x:=vσ] →^* u' [x:=v'], et il existe une réduction infinie partant de u' [x:=v'] (voir plus haut): contradiction. ♦

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 →₁ sur les λ-termes par: u →₁ 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 →₁ est fortement confluente (voir l'exercice 7). En effet, si u →₁ u₁ et u →₁ u₂, c'est qu'on peut rajouter des étoiles à certains rédex de u de sorte que le λ^*-terme obtenu se réduise en u₁, et des étoiles à certains rédex (en général différents) de u de sorte que le λ^*-terme obtenu se réduise en u₂. 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 →₁ u₁ se relève en une réduction de u' vers un terme u'₁ qui est u₁, avec possiblement des étoiles rouges ici ou là; et que de même u' se réduit en λ^*-calcul à un terme u'₂ qui est u₂ avec des étoiles bleues ici ou là. Comme le λ^*-calcul est confluent et terminant, u'₁ et u'₂ ont la même forme normale pour (β^*), disons v: mais alors u₁ →₁ v et u₂ →₁ v.

Théorème 1 Si u →^* v₁ et u →^* v₂, alors il existe w tel que v₁ →^* w et v₂ →^* w.

Preuve : Comme →₁ est fortement confluente, elle est confluente (exercice 7). Or → ⊆ →₁ ⊆ →^*: si u → v, alors il suffit de poser une étoile sur l'unique rédex contracté, ce qui montre que u →₁ v; si u →₁ 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 →^* v₁ et u →^* v₂, on a u →₁^* v₁ et u →₁^* v₂. Comme →₁ est confluente, il existe un w tel que v₁ →₁^* w et v₂ →₁^* w. On en déduit v₁ (→^*)^* w, donc v₁ →^* w, et de même v₂ →^* w. ♦

Corollaire 1 Si u₁ et u₂ sont deux formes normales de u, alors u₁ = u₂.

Preuve : Par le théorème 1, il existe w tel que u₁ →^* w et u₂ →^* w. Comme u_i est normal (i ∈ {1, 2}), u_i →^* w implique u_i = w. Donc u₁ = u₂. ♦

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.

Exercice 9 Démontrer que la relation →₁ ci-dessus coïncide en fait avec la relation ⇒ de l'exercice 8.

2.3 Pouvoir expressif

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:

les ajouter au langage, et se donner quelques règles de réduction supplémentaires comme 4+1 → 5. Ceci demande à redémontrer la confluence, par exemple, mais est une façon de faire standard pour définir de vrais langages de programmation.
Ou bien les définir dans le langage, c'est-à-dire trouver des termes dans le λ-calcul pur qui aient le comportement attendu. Il s'agit de l'approche la plus simple d'un point de vue logique, et bien que n'étant pas d'une utilité informatique immédiate, elle apporte de nombreux éléments.

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:

Définition 3 Pour tout n ∈ N, on pose ⌈n⌉ =_def λ f, x ⋅ fⁿ x, où fⁿ t est défini par: f⁰ t =_def t, fⁿ⁺¹ t =_def f (fⁿ t).

On pose d'autre part:

S =_def λ n, f, x ⋅ f (n f x);
⌈+⌉ =_def λ m, n ⋅ m S n;
⌈×⌉=_def λ m, n, f ⋅ m (n f);
⌈exp⌉ =_def λ m, n ⋅ m n.

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:

Exercice 10 Montrer que S ⌈n⌉ →^* ⌈n+1⌉, autrement dit S représente la fonction successeur, qui à n associe n+1. De même, montrer que ⌈+⌉ ⌈m⌉ ⌈n⌉ →^* ⌈m+n⌉, ⌈×⌉ ⌈m⌉ ⌈n⌉ →^* ⌈mn⌉, ⌈exp⌉ ⌈m⌉ ⌈n⌉ →^* ⌈n^m⌉.

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.

Exercice 11 On code les couples ⟨ u, v ⟩ par la fonction λ z ⋅ z u v. On définit les projections π₁ =_def λ s ⋅ s V, π₂ =_def λ s ⋅ s F. Montrer que π₁ ⟨ u, v ⟩ →^* u et π₂ ⟨ u, v ⟩ →^* v. Montrer par contre qu'en général, ⟨ π₁ s, π₂ s ⟩ ≠_βs.

Exercice 12 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 ⋅ π₂ (k (λ s ⋅ ⟨ S (π₁ s), π₁ 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 ?

Exercice 13 On définit ⌈let⌉ x=u ⌈in⌉ v par (λ x⋅ v) u. Montrer que ⌈let⌉ x=u ⌈in⌉ v → v[x:=u]. En déduire que ⌈let⌉ … ⌈in⌉ … est un mécanisme de nommage (de u par la variable x) correct.

Exercice 14 On veut maintenant fabriquer une construction de pattern-matching “case n of 0 ⇒ u ∣ S m ⇒ f(m)” qui calcule u si n=0, et sinon calcule f(m), où m est le prédécesseur de n. On va coder ceci par un terme ⌈intcase⌉ tel que ⌈intcase⌉ ⌈n⌉ u f représente le résultat désiré, autrement dit:

⌈intcase⌉ ⌈0⌉ u f	→^*	u
⌈intcase⌉ ⌈n+1⌉ u f	=_β	f ⌈n⌉

Montrer que l'on peut prendre ⌈intcase⌉ =_def λ k, x, f ⋅ k (λ z ⋅ f (P k)) x. Montrer qu'en général ce terme ne vérifie pas ⌈intcase⌉ ⌈n+1⌉ u f →^* f ⌈n⌉.

Exercice 15 On va définir une fonction de soustraction partielle ∼ par m ∼ n =_def max(m−n, 0). Montrer que ⌈∼⌉ =_def λ m,n ⋅ n P m en est une réalisation correcte.

Exercice 16 Montrer que ⌈zero?⌉ =_def λ n ⋅ n (λ z ⋅ F) V est une fonction de test de nullité, autrement dit:

⌈zero?⌉ ⌈0⌉	→^*	V
⌈zero?⌉ ⌈n+1⌉	→^*	F

En déduire que ⌈≤⌉=_def λ m, n ⋅ ⌈zero?⌉ (⌈∼⌉ m n) est un terme qui réalise le test ≤ d'inégalité.

Exercice 17 Définir ⌈∧⌉, un λ-terme prenant deux booléens b et b' et retournant leur conjonction b ∧ b' (le “et”). Faire la même chose pour le “ou” ∨, pour l'implication ⇒, la négation ¬.

Exercice 18 Sachant que m=n si et seulement si m≤ n et n≤ m, déduire des exercices précédents un terme de test d'égalité entre entiers.

Exercice 19 É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 G_a,b =_def λ n, m ⋅ n F (λ x ⋅ a) (m F (λ x ⋅ b)). Montrer que:

G_a,b ⌈0⌉ ⌈m⌉	→^*	a
G_a,b ⌈n+1⌉ ⌈m⌉	=_β	G_b,a ⌈m⌉ ⌈n⌉

En déduire que G_{V, F} est une réalisation correcte de ≤, et G_{F, V} une réalisation correcte de >.

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:

Théorème 2 Tout λ-terme F a un point fixe x, autrement dit un λ-terme x tel que x =_βF x.

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.

Exercice 20 On code les listes de termes comme suit. La liste u₁, …, u_n est représentée par [u₁, …, u_n] =_def λ f, x ⋅ f u₁ (f u₂ … (f u_n x) …). En particulier, la liste vide est ⌈nil⌉ =_def λ f,x ⋅ x, et la fonction ⌈cons⌉ qui prend un élément u₀ et une liste [u₁, …, u_n] et retourne [u₀, u₁, …, u_n] 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:

⌈hd⌉ (⌈cons⌉ a l)	→^*	a
⌈hd⌉ ⌈nil⌉	→^*	⌈nil⌉

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 [u₁, …, u_n] =_β[g u₁, …, g u_n]

(On pourra utiliser le fait que si l = [u₁, u₂, …, u_n], alors l h r =_βh u₁ (l' h r), où l' = [u₂, …, u_n], et effectuer une récurrence sur n.)

Montrer que ⌈tl⌉ =_def λ l ⋅ π₂ (l (λ s, p ⋅ ⟨ ⌈cons⌉ s (π₁ p), π₁ p ⟩) ⟨ ⌈nil⌉, ⌈nil⌉ ⟩) envoie la liste [u₁, u₂, …, u_n] vers [u₂, …, u_n]. (Ceci est analogue au codage du prédécesseur dans les entiers.)

Que fait ⌈app⌉ =_def λ l, l' ⋅ l ⌈cons⌉ l' ?