Previous Up Next

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 Ω =defx · 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* 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 ab, ba, ac et bd et c et d sont normaux et distincts, alors on aurait ac 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 (Newman)   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 uv. (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 uv, 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 u0u1 et tel que P (u1) soit faux: sinon, (*) impliquerait que P (u0) soit vrai. De même, il existe un u2 tel que u1u2 et P (u2) est faux. Par récurrence sur k, on en déduit l’existence d’une réduction infinie u0u1 → … → 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 uu1* v1 et uu2* 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 différentes techniques pour montrer le théorème [Bar84]. Une de celles-ci est donnée à l’exercice 8.

Exercice 7 (Confluence forte)   Supposons que la relation binaire soit fortement confluente, c’est-à-dire que si uu1 et uu2, alors u1 et u2 se réécrivent au même terme en au plus une étape. Montrer que est confluente.
Exercice 8 (Réductions parallèles )   On définit une nouvelle règle de réduction par:
  1. uu pour tout terme u;
  2. si uu et vv, alors uvuv;
  3. si uu, alors λ x · u ⇒ λ x · u;
  4. si uu et vv, alors x · u) vu′ [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 (uE (v)    E (λ x · u) = λ x · E (u)    E ((λ* x · uv) = (λ x · E (u)) E (v)

Le λ*-calcul n’a qu’une règle de réduction, la β*-réduction:

  (β*)      (λ* x· uv → u [x:=v]

On notera que, du coup, (λ x · u) v n’est jamais un rédex en λ*-calcul.

Lemme 3 (Développements finis)   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 [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≤ in), 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≤ in. 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≤ in.

On démontre que t σ est fortement normalisant pour toute substitution fortement normalisante, par récurrence structurelle sur t. Lorsque t est une variable xi, alors t σ = ti 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 [x1:=t1, …, xn:=tn], σ′ est la substitution parallèle [x1:=t1, …, xn:=tn, x:=vσ]. On démontre en effet que l’égalité tient dès que x ∉{x1, …, xn} et x n’est libre dans aucun ti, 1≤ in, par récurrence structurelle sur u. Or, par hypothèse σ, donc t1, …, tn 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 →1 sur les λ-termes par: u1 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 u1 u1 et u1 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 u1 u1 se relève en une réduction de u′ vers un terme u1 qui est u1, avec possiblement des étoiles rouges ici ou là; et que de même u′ se réduit en λ*-calcul à un terme u2 qui est u2 avec des étoiles bleues ici ou là. Comme le λ*-calcul est confluent et terminant, u1 et u2 ont la même forme normale pour (β*), disons v: mais alors u11 v et u21 v.

Théorème 1 (Confluence)   Si u* v1 et u* v2, alors il existe w tel que v1* w et v2* w.

Preuve : Comme →1 est fortement confluente, elle est confluente (exercice 7). Or → ⊆ →1 ⊆ →*: si uv, alors il suffit de poser une étoile sur l’unique rédex contracté, ce qui montre que u1 v; si u1 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 u1* v1 et u1* v2. Comme →1 est confluente, il existe un w tel que v11* w et v21* w. On en déduit v1 (→*)* w, donc v1* w, et de même v2* w.     ♦

Corollaire 1 (Unicité des formes normales)   Si u1 et u2 sont deux formes normales de u, alors u1 = u2.

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.

Exercice 9   Démontrer que la relation 1 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:

  1. 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.
  2. 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 nN, on pose n⌉ =def λ f, x · fn x, où fn t est défini par: f0 t =def t, fn+1 t =def f (fn t).

On pose d’autre part:

  1. S =def λ n, f, x · f (n f x);
  2. ⌈+⌉ =def λ m, n · m S n;
  3. ⌈×⌉=def λ m, n, f · m (n f);
  4. 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 Sn⌉ →*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⌉ →*nm.

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 π1 =def λ s · s V, π2 =def λ s · s F. Montrer que π1u, v ⟩ →* u et π2u, v ⟩ →* v. Montrer par contre qu’en général, ⟨ π1 s, π2 s ⟩ ≠βs.
Exercice 12 ()   On veut définir une fonction prédecesseur, c’est-à-dire un λ-terme P tel que P (Sn⌉) →*n pour tout entier n. Par convention, on posera que P (⌈0⌉) →* ⌈0⌉.

Montrer que P =def λ k · π2 (ks · ⟨ S1 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 ?

Exercice 13   On définit let⌉  x=u ⌈in⌉  v par x· v) u. Montrer que let⌉  x=u ⌈in⌉  vv[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 ⇒ uS mf(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 · kz · f (P k)) x. Montrer qu’en général ce terme ne vérifie pas intcase⌉  ⌈n+1⌉  u f* fn.
Exercice 15   On va définir une fonction de soustraction partielle par mn =def max(mn, 0). Montrer que ⌈∼⌉ =def λ m,n · n P m en est une réalisation correcte.
Exercice 16   Montrer que zero?⌉ =def λ n · nz · 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 bb (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 mn et nm, déduire des exercices précédents un terme de test d’égalité entre entiers.
Exercice 19 (B. Maurey )   É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 Fx · a) (m Fx · b)). Montrer que:
      Ga,b ⌈0⌉   ⌈m*a 
      Ga,b ⌈n+1⌉   ⌈m=βGb,a ⌈m⌉  ⌈n
En déduire que GV, F est une réalisation correcte de , et GF, 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 Ffact⌉, 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⌉ =βFfact⌉. 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 Ω =defx · 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* FF).

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 AAFB (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, AAFB(A) F = (λ h · h (C (A, h))) FF (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 (λ gh · h (ggh)) (λ gh · 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* FF) 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 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 · ly,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 · la, 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 (lh r), où l′ = [u2, …, un], et effectuer une récurrence sur n.)

Montrer que tl⌉ =def λ l · π2 (ls, p · ⟨ ⌈conss1 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′ · lconsl ?


Previous Up Next