3  Stratégies de réduction et langages de programmation

On a vu qu’un λ-terme pouvait contenir plusieurs rédex. Si l’on vu calculer la forme normale d’un terme u (si elle existe), on va pouvoir l’obtenir en choisissant un rédex dans u, en le contractant, et en répétant le processus jusqu’à ce qu’il n’y ait plus de rédex. Ce choix du rédex à chaque étape de réduction est appelé une stratégie de réduction.

3.1  Stratégies internes

Prenons le cas d’un langage de programmation usuel, comme OCaml ou Pascal ou C. Dans ces langages, un terme de la forme uv (noté u(v) en Pascal ou en C) s’évalue typiquement en calculant d’abord la valeur f de u, qui doit être une fonction, puis en calculant la valeur a de v, puis en appliquant f à a. (En général, u est un identificateur qui dénote déjà une fonction, sans qu’on ait à calculer quelle fonction c’est exactement.) Remis dans un cadre λ-calculatoire, on peut dire qu’on a d’abord réduit les rédex de u, puis quand il n’y en a plus eu, on a réduit les rédex de v, enfin on regarde ce qu’est devenu u, et s’il est devenu un terme de la forme λ x · t, on applique cette dernière fonction à v pour donner t[x:=v], et on continue.

Ce genre de stratégie est appelée une stratégie interne (innermost en anglais), parce qu’elle réduit d’abord les rédex les plus à l’intérieur des termes d’abord. La stratégie particulière présentée préfère de plus les rédex de gauche à ceux de droite: elle ne réduit les rédex de droite que quand il n’y en a plus à gauche. Il s’agit d’une stratégie interne gauche. Une stratégie interne droite est évidemment envisageable, et se rapprocherait de la sémantique de OCaml. Un petit test qui le montre est de taper:

let a = ref 0;;
let f x y = ();;
f (a:=1) (a:=2);;
a;;

qui crée une référence (une cellule de valeur modifiable par effet de bord), puis une fonction bidon f qui ignore ses deux arguments. Ensuite on calcule f appliquée à deux arguments qui affectent 1, resp. 2 à a. Le langage étant séquentiel, la valeur finale de a permettra de savoir lequel des arguments a été évalué en dernier. En OCaml, la réponse est 1, montrant que c’est l’argument de gauche qui a été évalué en dernier.

Évidemment, en λ-calcul on n’a pas d’affectations, et le fait qu’une stratégie interne soit gauche ou droite ne change rien au résultat final.

3.2  Stratégies externes

On peut aussi décider d’utiliser une stratégie externe, qui réduit les rédex les plus externes d’abord. Autrement dit, alors qu’une stratégie interne réduit (λ x · u) v en normalisant λ x· u vers λ x · u′, en normalisant v vers v′, puis en réduisant u′ [x:=v′], une stratégie externe commence par contracter (λ x· u) v en u [x:=v], qu’il réduit à son tour.

Vu au travers du filtre des langages de programmation usuels, voici ce que ces stratégies donnent pour l’évaluation de fact (1+2), en supposant la définition de fact donnée au début de ce chapitre, et les règles de réduction typiques de +, ×, etc. Pour se fixer les idées, on utilisera celles de ⌈fact⌉, ⌈+⌉, ⌈×⌉.

On commence par regarder la stratégie externe gauche. Comme ⌈fact⌉ = Y (λ f · λ n · ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (f (P n)))), par une stratégie externe on aura ⌈fact⌉ →^* λ n · ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (⌈fact⌉ (P n)))). On obtient alors:

mais ici on voit que l’argument (⌈+⌉   ⌈1⌉   ⌈2⌉) a été copié en trois endroits. Chaque occurrence devra être réduite en ⌈3⌉ indépendamment des autres; autrement dit, on va devoir calculer 1+2 = 3 trois fois !

Pour voir ça plus clairement, reprenons une notation plus proche de la notation OCaml, et en particulier plus agréable. Nous réécrivons la réduction ci-dessus et la complétons:

3.3  Stratégies internes faibles, appel par valeur

Maintenant, examinons ce qui se passe avec une stratégie interne. Nous allons commencer par supposer que la factorielle ⌈fact⌉ s’évalue par la stratégie interne en λ n · ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (⌈fact⌉ (P n)), et que ceci est normal. (Il y a un problème avec cette hypothèse, que nous résoudrons par la suite.) Alors le même calcul, par la stratégie interne, est beaucoup plus direct. Dans un souci de lisibilité, nous l’écrivons en notation pseudo-OCaml:

ce qui correspond beaucoup plus à ce à quoi on s’attend de la part d’un langage de programmation.

Cependant, dans l’exemple ci-dessus, nous avons triché deux fois.

Première tricherie: Nous avons supposé que ⌈fact⌉ s’évaluait par la stratégie interne en λ n · ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (⌈fact⌉ (P n)), et que ceci était normal. Mais c’est faux ! En fait, ⌈fact⌉ est de la forme Y F, pour un certain F, et on a:

qui ne termine jamais !

Le remède est que dans les langages de programmation usuels, on ne réduit pas sous les λ. Autrement dit, on considère que λ x · u est déjà suffisamment évalué. De telles stratégies s’appellent des stratégies de réduction faible. Elles ne sont évidemment pas suffisantes pour obtenir une forme normale — par exemple, aucune règle de réduction faible ne s’applique pour réduire λ x · (λ y · y) x. Mais ça n’est pas très important dans un langage de programmation; en un sens, par programme on veut calculer des entiers, des listes, des structures de données en somme. Si un programme retourne une fonction, c’est qu’il attend encore au moins un argument pour pouvoir continuer le calcul.

La stratégie de réduction interne faible peut maintenant se formaliser par les règles suivantes, où u ▷ v signifie “u se réduit en une étape en v” par cette stratégie:

L’argument V de l’abstraction dans la règle (β▷) est contraint à être une valeur. On définit ici les valeurs V par récurrence sur la structure de V comme étant les variables, les applications V₁ V₂ d’une valeur V₁ qui n’est pas une abstraction à une valeur V₂, et les abstractions quelconques λ x · u. De façon équivalente:

Ces règles sont une façon commode de dire que ▷ est la plus petite relation binaire telle que (λ x· u) V ▷ u [x:=V] pour tout terme u et toute valeur V, et passant aux contextes applicatifs (règles (App₁▷) et (App₂▷)), mais ne passant pas nécessairement aux contextes d’abstraction. Formellement, les formules (ici, de la forme u ▷ v) au-dessus des barres sont des prémisses, qu’il faut vérifier avant de pouvoir appliquer la règle et d’en déduire la conclusion qui est en-dessous de la barre.

Pour corriger le problème de non-terminaison de la définition de ⌈fact⌉ en tant que point fixe, on va définir ⌈fact⌉ =_def Y_v [F] au lieu de Y F, où F est la fonctionnelle définissant ⌈fact⌉, soit:

et Y_v [F] est définie de sorte d’une part que Y_v [F] V ▷^* F (Y_v [F]) V pour toute valeur V, et d’autre part que Y_v [F] soit une valeur. On peut y arriver en effectuant quelques η-expansions dans Y F, comme le montre l’exercice 21. Selon la stratégie interne faible, on aura alors:

où le dernier terme est une valeur, et donc la définition de ⌈fact⌉ ne boucle plus.

Deuxième tricherie: Le calcul que l’on a fait de la factorielle de 3 par stratégie interne, maintenant modifiée en une stratégie interne faible, n’est toujours pas correct, même si on remplace → par ▷. En effet, la réduction:

est incorrecte: ce n’est pas une réduction par stratégie interne. En effet, revenons à une écriture plus formelle, alors la ligne du dessus est F ⌈1⌉ (⌈×⌉  ⌈3⌉   (⌈fact⌉ (P ⌈3⌉))), mais la réduction par stratégie interne demande que l’on calcule d’abord la valeur ⌈6⌉ de ⌈×⌉  ⌈3⌉   (⌈fact⌉ (P ⌈3⌉)) avant de conclure que l’on peut normaliser F ⌈1⌉ ⌈6⌉ en ⌈6⌉. Or ce que nous avons fait ici, c’est utiliser une étape de stratégie externe, pour éviter de garder l’argument ⌈1⌉ en attente, puisque son destin est d’être éliminé de toute façon.

Une conclusion provisoire est que les langages de programmation utilisent en fait une stratégie interne faible pour les appels de fonction normaux, mais une stratégie externe (faible elle aussi) pour les tests. La raison est pragmatique: il est plus avantageux de calculer de façon interne les appels de fonctions normaux, parce que leurs arguments devront en général être utilisés par la fonction, et que s’ils sont utilisés plusieurs fois, on n’aura pas à recalculer leur valeur plusieurs fois; mais d’autre part, les arguments en position “then” et “else” d’un if ne sont jamais utilisés plus d’une fois, et en fait l’un des deux ne sera pas utilisé, il est donc plus intéressant d’utiliser une stratégie externe dans ce cas, ce qui économise l’évaluation de l’argument qui ne sera jamais évalué.

3.4  Standardisation, appel par nom

Il est bon de remarquer, cependant, que changer de stratégie n’est pas innocent: certains termes ont une réduction interne qui termine mais aucune réduction externe finie. (Prendre l’exemple de l’exercice 6.) En revanche, et aussi bizarre que ça paraisse, la réduction externe gauche, aussi inefficace qu’elle puisse être en pratique, est optimale dans le sens suivant:

Autrement dit, la stratégie externe est peut-être lente, mais elle est sûre: elle ne se laisse pas embarquer dans des bouclages inutiles.

Preuve :

Avant de commencer, faisons quelques remarques sur les stratégies externes:

• D’abord, on peut écrire tout λ-terme u de façon unique sous la forme λ x₁, …, x_n · h u₁ … u_m, où h u₁ … u_m n’est pas une abstraction, h n’est pas une application, et n et m valent possiblement 0. Le sous-terme h est appelé la tête de u, et la notation λ x₁, …, x_n · h u₁ … u_m est la forme de tête de u.

  En effet, si u est une abstraction λ x· u′, on prend x₁=x et on continue le processus sur u′; après un nombre fini détapes, on aboutit ainsi à écrire u sous la forme λ x₁, …, x_n · v, où v n’est pas une abstraction. Dans ce cas, soit v est directement la tête h, soit v s’écrit v′ u_m, et on recommence le processus avec v′ à la place de v. Ce processus s’arrête lorsque v′ devient un terme qui n’est pas une application, et on obtient ainsi v sous la forme désirée h u₁ … u_m. (Exercice: formaliser cet argument.)

• Si la tête h de u est une abstraction λ x· v, alors nécessairement m≥ 1 (sinon h u₁ … u_m serait une abstraction), et le sous-terme (λ x· v) u₁ de u est un rédex. En fait, dans ce cas (λ x· v) u₁ est un rédex le plus externe possible, et c’est le plus à gauche dans u de tous les rédex externes.

  Dans ce cas spécial, on dit que (λ x· v) u₁ est le rédex de tête de u, et l’étape de réduction:

  u = λ x1, …, xn · (λ x · v) u1 … um → λ x1, …, xn · v [x:=u1] u2 … um

  est appelée réduction de tête.

  Notons →_t la réduction de tête en une étape, et →_t^* sa clôture réflexive transitive.

• Si par contre la tête h de u n’est pas une abstraction, auquel cas il n’y a pas de rédex de tête et le terme u est dit normal de tête (car il n’y a pas de réduction de tête), alors h est une variable. Cette variable est appelée la variable de tête de u.

  La propriété importante est que dans une forme normale de tête u = λ x₁, …, x_n · h u₁ … u_m, les seules réductions possibles prennent place dans les u_i, et en fait sans aucune interférence entre les différents u_i. L’en-tête λ x₁, …, x_n · h … ne bougera plus jamais dans la réduction.

Nous donnons maintenant une preuve du théorème due à René David. On peut définir de façon astucieuse la notion de réduction standard ⇒_s de u vers v, comme étant la relation binaire définie par récurrence sur la taille de v, par u ⇒_s v si et seulement si:

1. v s’écrit sous forme de tête λ x₁, …, x_n · v₀ v₁ … v_m,
2. u se réduit par réduction de tête en une forme de tête λ x₁, …, x_n · u₀ u₁ … u_m,
3. si v₀ est une variable x, alors u₀=x, et si v₀ est une abstraction λ x · v′ alors u₀ est de la forme λ x · u′ et u′ ⇒_s v′;
4. u₁ ⇒_s v₁, …, u_m ⇒_s v_m.

Il est clair que la stratégie externe gauche est une stratégie standard. En effet, la stratégie externe gauche commence par calculer la forme normale de tête (par →_t^*) λ x₁, …, x_n · u₀ u₁ … u_m, puis normalise u₁ par la stratégie externe gauche, puis u₂, …, enfin u_m; u₀ étant une variable, sa normalisation est immédiate. La notion de réduction standard est plus souple en ce sens qu’on ne demande pas que u₀ soit une variable, et que l’on peut alterner des réductions dans u₁ avec des réductions dans u₂, …, u_m, et même dans u₀.

On va démontrer que: (*) si u →^* v, alors u ⇒_s v, pour tous termes u, v. Ceci impliquera le théorème: si u a une forme normale v, alors u ⇒_s v par (*), et il ne reste plus qu’à démontrer par récurrence sur la taille de v que cette réduction standard induit une réduction externe gauche de u vers v. Si v est une variable, alors cette réduction standard est une réduction de tête, qui est bien une réduction externe gauche. Sinon, écrivons v sous la forme λ x₁, …, x_n · v₀ v₁ … v_m. Alors nécessairement la réduction standard de u vers v commence par effectuer une réduction de tête de u vers une forme de tête λ x₁, …, x_n · u₀ u₁ … u_m suivie de réductions standard u₀ ⇒_s v₀, u₁ ⇒_s v₁, …, u_m ⇒_s v_m. Ces réductions standard induisent des réductions externes gauches par hypothèse de récurrence, donc la réduction:

est une réduction externe gauche.

Montrons maintenant (*). En première lecture, il est conseillé de sauter la démonstration, qui est assez technique. L’idée est de permuter les applications de la règle (β), et la difficulté est de le faire dans le bon ordre.

() On va démontrer (*) par étapes. Le point important est le numéro 10 ci-dessous, les précédents sont des points techniques:

1. D’abord, on remarque que si u=v, alors u ⇒_s v; autrement dit, ⇒_s est réflexive. Ceci se démontre par une récurrence facile sur la taille de v, où les réductions de tête impliquées sont toutes de longueur nulle;
2. Ensuite, si u →_t^* v, alors u ⇒_s v. Écrivons v sous forme de tête λ x₁, …, x_n · v₀ v₁ … v_m. Par hypothèse, u →_t^* λ x₁, …, x_n · u₀ u₁ … u_m où u_i = v_i pour tout i. En particulier, par le point 1, u_i ⇒_s v_i pour tout i ≥ 1. De plus, si u₀=v₀ est une abstraction λ x · u′, alors u′ ⇒_s u′ par le point 1.
3. Si u →_t^* v et v ⇒_s w, alors u ⇒_s w: analyse de cas facile.
4. Si λ x · u′ ⇒_s v, alors v est de la forme λ x · v′ et u′ ⇒_s v′. Pour ceci, on applique la définition de nouveau, en observant d’abord que si λ x · u′ →_t w, alors w s’écrit λ x · w′ avec u′ →_t w′.
5. Si u se réduit par réduction de tête en une forme de tête λ x₁, …, x_n · u₀ u₁ … u_m où n=0, alors il s’y réduit par une réduction de tête faible, c’est-à-dire opérant sous un nombre nul de λ (ceci permet de réécrire λ x₁, …, x_n · (λ x · t) s₁ … s_m → λ x₁, …, x_n · t [x:=s₁] s₂ … s_m uniquement si n=0). En effet, tout réduction de tête qui n’est pas faible ne peut se réduire qu’en des termes qui ont au moins un λ en tête.
6. Si u ⇒_s v et u′ ⇒_s v′, alors uu′ ⇒_s vv′. Par définition, v s’écrit sous forme de tête λ x₁, …, x_n · v₀ v₁ … v_m, u se réduit par réduction de tête en une forme de tête λ x₁, …, x_n · u₀ u₁ … u_m, de sorte que les conditions 3 et 4 de la définition de ⇒_s soient vérifiées.

   Si n=0, par le point 5, u se réécrit par réduction de tête faible en u₀ u₁ … u_m. L’intérêt de la réduction de tête faible est qu’alors uu′ se réduit par réduction de tête (faible de nouveau) en u₀ u₁ … u_m u′. Ce genre de propriété de stabilité n’est pas vraie pour les réductions de tête générales. On en conclut immédiatement uu′ ⇒_s vv′.

   Si n≠ 0, considérons le plus grand préfixe de la réduction de tête de u à λ x₁, …, x_n · u₀ u₁ … u_m qui forme une réduction de tête faible. On a donc un terme t, et une suite de réductions de tête u →_t^* t →_t^* λ x₁, …, x_n · u₀ u₁ … u_m où les réductions de tête de u à t sont faibles, et les suivantes non. Comme n ≠ 0, on note que t s’écrit lui-même comme une abstraction λ x₁ · t′, soit parce que t = λ x₁, …, x_n · u₀ u₁ … u_m, soit parce qu’il y a au moins une étape de réduction de tête de t vers λ x₁, …, x_n · u₀ u₁ … u_m, et qu’elle n’est pas faible. On note alors que t′ →_t^* λ x₂, …, x_n · u₀ u₁ … u_m.

   On en déduit que uu′ →_t^* (λ x₁ · t′) u′ (par la propriété de stabilité des réductions de tête faibles remarquée plus haut), t′ ⇒_s λ x₂, …, x_n · v₀ v₁ … v_m (en utilisant le point 3), u′ ⇒_s v′, donc uu′ ⇒_s (λ x₁ · (λ x₂, …, x_n · v₀ v₁ … v_m)) v′ = vv′ par définition.

7. Si u ⇒_s v alors λ x · u ⇒_s λ x · v. C’est une récurrence immédiate sur v, en notant que si u →_t^* u′ implique λ x · u →_t^* λ x · u′ (propriété vraie de la réduction de tête, mais pas de la réduction de tête faible cette fois-ci!).
8. Si u₀ ⇒_s w₀, u₁ ⇒_s w₁, …, u_m ⇒_s w_m, alors λ x₁, …, x_n · u₀ u₁ … u_m ⇒_s λ x₁, …, x_n · w₀ w₁ … w_m. Ceci peut sembler être juste une reformulation de la définition, mais la définition requiert que λ x₁, …, x_n · u₀ u₁ … u_m et λ x₁, …, x_n · w₀ w₁ … w_m soient des formes de tête, ce que l’on ne demande pas ici. La propriété se démontre par application itérée des points 6, puis 7.
9. Si u′ ⇒_s w′ et u₁ ⇒_s w₁, alors u′ [x:=u₁] ⇒_s w′ [x:=w₁]. Ceci se démontre par récurrence sur la taille de w′. Écrivons w′ sous forme de tête λ y₁, …, y_n · w′₀ w′₁ … w′_m. Par hypothèse u′ →_t^* λ y₁, …, y_n · u′₀ u′₁ … u′_m, où u′₁ ⇒_s w′₁, …, u′_m ⇒_s w′_m, et soit u′₀ et w′₀ sont des variables identiques, soit u′₀ = λ x · s, w′₀ = λ x · t et s ⇒_s t. Par hypothèse de récurrence, u′₁ [x:=u₁] ⇒_s w′₁ [x:=w₁], …, u′_m [x:=u₁] ⇒_s w′_m [x:=w₁]. De plus, u′₀ [x:=u₁] ⇒_s w′₀ [x:=w₁], par l’argument suivant: si u′₀=w′₀=x, ceci provient de u₁ ⇒_s w₁, si u′₀ et w′₀ sont égaux à la même variable y et y ≠ x, alors y ⇒_s y par le point 1, et si u′₀ = λ x · s, w′₀ = λ x · t et s ⇒_s t, alors ceci vient de s [x:=u₁] ⇒_s t [x:=w₁] (hypothèse de récurrence) et du point 7.

   Comme u′_i [x:=u₁] ⇒_s w′_i [x:=w₁] pour tout i, 0≤ i≤ m, le point 8 entraîne que (λ y₁, …, y_n · u′₀ u′₁ … u′_m) [x:=u₁] = λ y₁, …, y_n · u′₀ [x:=u₁] u′₁ [x:=u₁] … u′_m [x:=u₁] ⇒_s λ y₁, …, y_n · w′₀ [x:=w₁] w′₁ [x:=w₁] … w′_m [x:=w₁] = w′ [x:=w₁]. Puisque u′ →_t^* λ y₁, …, y_n · u′₀ u′₁ … u′_m, on a aussi u′ [x:=u₁] →_t^* (λ y₁, …, y_n · u′₀ u′₁ … u′_m) [x:=u₁], et le point 3 implique donc u′ [x:=u₁] ⇒_s w′ [x:=w₁].

10. Si u ⇒_s w → v, alors u ⇒_s v. La démonstration est par récurrence sur la taille de w.

    Par définition, u se réduit par réduction de tête en une forme de tête λ x₁, …, x_n · u₀ u₁ u₂ … u_m, w a la forme de tête λ x₁, …, x_n · w₀ w₁ w₂ … w_m et u_i ⇒_s w_i pour tout i ≥ 1, et soit u₀ et w₀ sont la même variable, soit u₀ = λ x · u′, w₀ = λ x · w′ pour certains terms u′ et w′ tels que u′ ⇒_s w′.

    La réduction de w vers v peut maintenant se produire en deux types d’endroits.

    Cas 1: elle se produit dans l’un des w_j (et si j=0, dans w′). Alors v = λ x₁, …, x_n · v₀ v₁ v₂ … v_n, avec v_i = w_i pour tout i≠ j, et w_j → v_j sinon. Noter que u_j ⇒_s w_j → v_j, et que la taille de w_j est plus petite que celle de w, donc on peut appliquer l’hypothèse de récurrence et conclure que u_j ⇒_s v_j. D’autre part, pour i≠ j on a u_i ⇒_s w_i = v_i. Donc dans tous les cas, pour tout i, u_i ⇒_s v_i. Il s’ensuit que u ⇒_s v, en utilisant le point 8.

    Cas 2: la réduction de w vers v est une réduction de tête. C’est l’unique cas intéressant de la démonstration. Noter qu’alors on a nécessairement u₀ = λ x · u′, w₀ = λ x · w′ pour certains terms u′ et w′ tels que u′ ⇒_s w′. De plus, v = λ x₁, …, x_n · w′ [x:=w₁] w₂ … w_m.

    L’idée est qu’au lieu de contracter le rédex (λ x · w′) w₁ dans w (donc tard dans la réduction) on va contracter le rédex qui lui fait pendant beaucoup plus tôt dans la réduction, (λ x · u′) u₁. Formellement, on étend la réduction de tête partant de u en:

    u →t*         λ x1, …, xn · (λ x· u′) u1 u2 … um          →t λ x1, …, xn · u′ [x:=u1] u2 … um.

    Puis l’on note que u′ [x:=u₁] ⇒_s w′ [x:=w₁] par le point 9, u_i ⇒_s w_i pour tout i ≥ 2 par hypothèse, donc λ x₁, …, x_n · u′ [x:=u₁] u₂ … u_m ⇒_s λ x₁, …, x_n · w′ [x:=w₁] w₂ … w_m = v par le point 8.

Nous démontrons maintenant (*), à savoir que u →^* v implique u ⇒_s v, par récurrence sur la longueur k de la réduction donnée de u vers v. Si cette longueur est 0, alors u=v et on conclut par le point 1. Sinon, c’est que cette réduction s’écrit u →^* w → v, où la réduction de u à w est de longueur k−1. Par hypothèse de récurrence, u ⇒_s w, et par le point 4 ci-dessus, u ⇒_s v.     ♦

La stratégie externe gauche (leftmost outermost strategy en anglais) est souvent appelée réduction gauche, ou stratégie d’appel par nom. Cette dernière dénomination vient du langage Algol, et caractérise le fait que dans (λ x · u) v, on remplace d’abord x par v dans u avant de réduire v — le terme non réduit v étant pris comme nom de sa valeur.

Exercice 23 ()   Utiliser la notion de réduction standard, et en particulier le point (*) de la démonstration du théorème 3 pour montrer directement que le λ-calcul est confluent.

D’un point de vue pratique, sachant que ni les stratégies externes (appel par valeur) ni les stratégies internes (appel par nom) ne sont des panacées, pourquoi ne pas utiliser d’autres stratégies ? Une qui semble intéressante est la stratégie d’appel par nécessité, utilisée dans les langages comme Miranda ou Haskell. L’idée, c’est de partager tous les sous-termes d’un λ-terme, et de considérer les λ-termes comme des graphes. On verra comment faire cela dans la troisième partie de ce cours, intitulée “Machines, Interprètes”. Disons tout de suite que ce n’est pas, en fait, une panacée.