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.
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.
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:
|
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 V1 V2 d’une valeur V1 qui n’est pas une abstraction à une valeur V2, et les abstractions quelconques λ x · u. De façon équivalente:
V ::= V V … V ∣ λ x · Λ |
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 (App1▷) et (App2▷)), 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 Yv [F] au lieu de Y F, où F est la fonctionnelle définissant ⌈fact⌉, soit:
F =def λ f · λ n · ⌈if⌉ (⌈zero?⌉ n) ⌈1⌉ (⌈×⌉ n (f (P n))) |
et Yv [F] est définie de sorte d’une part que Yv [F] V ▷* F (Yv [F]) V pour toute valeur V, et d’autre part que Yv [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é.
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:
En effet, si u est une abstraction λ x· u′, on prend x1=x et on continue le processus sur u′; après un nombre fini détapes, on aboutit ainsi à écrire u sous la forme λ x1, …, xn · v, où v n’est pas une abstraction. Dans ce cas, soit v est directement la tête h, soit v s’écrit v′ um, 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 u1 … um. (Exercice: formaliser cet argument.)
Dans ce cas spécial, on dit que (λ x· v) u1 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.
La propriété importante est que dans une forme normale de tête u = λ x1, …, xn · h u1 … um, les seules réductions possibles prennent place dans les ui, et en fait sans aucune interférence entre les différents ui. L’en-tête λ x1, …, xn · 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:
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*) λ x1, …, xn · u0 u1 … um, puis normalise u1 par la stratégie externe gauche, puis u2, …, enfin um; u0 é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 u0 soit une variable, et que l’on peut alterner des réductions dans u1 avec des réductions dans u2, …, um, et même dans u0.
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 λ x1, …, xn · v0 v1 … vm. 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 λ x1, …, xn · u0 u1 … um suivie de réductions standard u0 ⇒s v0, u1 ⇒s v1, …, um ⇒s vm. 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:
Si n=0, par le point 5, u se réécrit par réduction de tête faible en u0 u1 … um. 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 u0 u1 … um 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 à λ x1, …, xn · u0 u1 … um 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* λ x1, …, xn · u0 u1 … um 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 λ x1 · t′, soit parce que t = λ x1, …, xn · u0 u1 … um, soit parce qu’il y a au moins une étape de réduction de tête de t vers λ x1, …, xn · u0 u1 … um, et qu’elle n’est pas faible. On note alors que t′ →t* λ x2, …, xn · u0 u1 … um.
On en déduit que uu′ →t* (λ x1 · t′) u′ (par la propriété de stabilité des réductions de tête faibles remarquée plus haut), t′ ⇒s λ x2, …, xn · v0 v1 … vm (en utilisant le point 3), u′ ⇒s v′, donc uu′ ⇒s (λ x1 · (λ x2, …, xn · v0 v1 … vm)) v′ = vv′ par définition.
Comme u′i [x:=u1] ⇒s w′i [x:=w1] pour tout i, 0≤ i≤ m, le point 8 entraîne que (λ y1, …, yn · u′0 u′1 … u′m) [x:=u1] = λ y1, …, yn · u′0 [x:=u1] u′1 [x:=u1] … u′m [x:=u1] ⇒s λ y1, …, yn · w′0 [x:=w1] w′1 [x:=w1] … w′m [x:=w1] = w′ [x:=w1]. Puisque u′ →t* λ y1, …, yn · u′0 u′1 … u′m, on a aussi u′ [x:=u1] →t* (λ y1, …, yn · u′0 u′1 … u′m) [x:=u1], et le point 3 implique donc u′ [x:=u1] ⇒s w′ [x:=w1].
Par définition, u se réduit par réduction de tête en une forme de tête λ x1, …, xn · u0 u1 u2 … um, w a la forme de tête λ x1, …, xn · w0 w1 w2 … wm et ui ⇒s wi pour tout i ≥ 1, et soit u0 et w0 sont la même variable, soit u0 = λ x · u′, w0 = λ 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 wj (et si j=0, dans w′). Alors v = λ x1, …, xn · v0 v1 v2 … vn, avec vi = wi pour tout i≠ j, et wj → vj sinon. Noter que uj ⇒s wj → vj, et que la taille de wj est plus petite que celle de w, donc on peut appliquer l’hypothèse de récurrence et conclure que uj ⇒s vj. D’autre part, pour i≠ j on a ui ⇒s wi = vi. Donc dans tous les cas, pour tout i, ui ⇒s vi. 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 u0 = λ x · u′, w0 = λ x · w′ pour certains terms u′ et w′ tels que u′ ⇒s w′. De plus, v = λ x1, …, xn · w′ [x:=w1] w2 … wm.
L’idée est qu’au lieu de contracter le rédex (λ x · w′) w1 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′) u1. Formellement, on étend la réduction de tête partant de u en:
|
Puis l’on note que u′ [x:=u1] ⇒s w′ [x:=w1] par le point 9, ui ⇒s wi pour tout i ≥ 2 par hypothèse, donc λ x1, …, xn · u′ [x:=u1] u2 … um ⇒s λ x1, …, xn · w′ [x:=w1] w2 … wm = 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.
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.