Previous Up Next

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:
  ⌈fact⌉ (⌈+⌉   ⌈1⌉   ⌈2⌉)
→* (λ n ⋅ ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (⌈fact⌉ (P n)))) (⌈+⌉   ⌈1⌉   ⌈2⌉)
→ ⌈if⌉ (⌈zero?⌉ (⌈+⌉   ⌈1⌉   ⌈2⌉))   ⌈1⌉  (⌈×⌉ (⌈+⌉   ⌈1⌉   ⌈2⌉)  (⌈fact⌉ (P (⌈+⌉   ⌈1⌉   ⌈2⌉))))
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:
  fact (1+2)
→* (λ n ⋅ if n=0 then 1 else n × fact (n−1)) (1+2)
→ if (1+2)=0 then 1 else (1+2) × fact ((1+2)−1)
  ...où l'on passe quelques temps à réduire (1+2)=0 en F ...
→* if F then 1 else (1+2) × fact ((1+2)−1)
→ (1+2) × fact ((1+2)−1)
→* ...où 1+2 n'est toujours pas évalué à 3 ...
  ...on réduit comme ça jusqu'à la fin de la récursion ...
→* (1+2) × (((1+2)−1) × ((((1+2)−1)−1) × 1))
→* ...et après un temps certain, on obtient le résultat final,
→* 6


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:

  fact (1+2)
→* (λ n ⋅ if n=0 then 1 else n × fact (n−1)) (1+2)
→* (λ n ⋅ if n=0 then 1 else n × fact (n−1)) (3)
→ if 3=0 then 1 else 3 × fact (3−1))
→* if F then 1 else 3 × fact (3−1))
→ 3 × fact (3−1)
→* 3 × (λ n ⋅ if n=0 then 1 else n × fact (n−1)) (2)
→* ...par le même procédé ...
  3 × (2 × fact (2−1))
→* 3 × (2 × (1 × 1))
→* 6


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:
Y F → (λ x ⋅ F (xx)) (λ x ⋅ F (xx)) → F ((λ x ⋅ F (xx)) (λ x ⋅ F (xx))) → F ( F ((λ x ⋅ F (xx)) (λ x ⋅ F (xx)))) → …
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:
⌈fact⌉ = Yv [F]
▷* (λ f ⋅ λ n ⋅ ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (f (P n)))) (Yv [F])
= (λ f ⋅ λ n ⋅ ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (f (P n)))) ⌈fact⌉
▷ λ n ⋅ ⌈if⌉ (⌈zero?⌉ n)   ⌈1⌉  (⌈×⌉ n  (⌈fact⌉ (P n))
où le dernier terme est une valeur, et donc la définition de ⌈fact⌉ ne boucle plus.

Exercice 21   Définissons Yv [F] =def λ y ⋅ (λ x ⋅ F (λ z ⋅ xxz)) (λ x ⋅ F (λ z ⋅ xxz)) y. Montrer que Yv [F] ▷* F (Yv [F]) V pour toute valeur V.


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:

  if F then 1 else 3 × fact (3−1)
▷ 3 × fact (3−1)


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:

Théorème 3   Si u est faiblement normalisant, alors la stratégie externe gauche calcule la forme normale de u par une réduction finie.


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: 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 plus petite relation binaire telle que:
  1. si v est une variable, alors pour tout terme u tel que u →t* v, on a u ⇒s v;
  2. sinon, v s'écrit sous forme de tête λ x1, …, xn ⋅ v0 v1 … vm, avec n≥ 1 ou m≥ 1. Alors, pour tout u tel que u se réduit par réduction de tête en la forme de tête λ x1, …, xn ⋅ u0 u1 … um, si ui ⇒s vi pour tout i, 0≤ i≤ n, alors u ⇒s v.
Ceci est une définition correcte de u ⇒s v, par récurrence sur la taille de v. En effet, dans le cas 2, par la condition n≥ 1 ou m≥ 1, tous les vi sont strictement plus petits que v.

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 forme normale de tête λ 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:
u →t* λ x1, …, xn ⋅ u0 u1 u2 … um
→* λ x1, …, xn ⋅ v0 u1 u2 … um
→* λ x1, …, xn ⋅ v0 v1 u2 … um
→* λ x1, …, xn ⋅ v0 v1 v2 … um
→* …
→* λ x1, …, xn ⋅ v0 v1 v2 … vm = v
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 4 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 récurrence sur la taille de v. Si v est une variable, u=v implique u →t* v, donc u ⇒s v. Sinon, on peut écrire v en forme de tête λ x1, …, xn ⋅ v0 v1 v2 … vm, avec n≥ 1 ou m≥ 1, mais alors u = λ x1, …, xn ⋅ v0 v1 v2 … vm se réduit de tête (en 0 étape) en la forme de tête λ x1, …, xn ⋅ v0 v1 v2 … vm, avec vi ⇒s vi pour tout i par hypothèse de récurrence.
  2. Ensuite, si u →t* v, alors u ⇒s v. Ceci est encore par récurrence sur la taille de v. Si v est une variable, c'est évident, par la clause 1 de la définition de ⇒s. Sinon, écrivons v en forme de tête λ x1, …, xn ⋅ v0 v1 v2 … vm, avec n≥ 1 ou m≥ 1. Comme u se réduit par réduction de tête en v, et que vi ⇒s vi pour tout i par le point 1 ci-dessus, il s'ensuit que u ⇒s v.

  3. Si u' ⇒s w' et u1 ⇒s w1, alors u' [x:=u1] ⇒s w' [x:=w1]. Ceci se démontre par récurrence sur la taille de w'.

    Si w' est la variable x, alors u' →t* x, donc u' [x:=u1] →t* u1. De u1 ⇒s w1, on en déduit que u' [x:=u1] ⇒s w1 = w' [x:=w1].

    Si w' est une autre variable y, alors u' →t* y = w' [x:=w1], et l'on conclut par le point 2.

    Sinon, puisque u' ⇒s w', on peut écrire u' →t* λ x1, …, xn ⋅ u'0 u'1 … u'm, u'0 ⇒s w'0, ..., u'm ⇒s w'm et w' = λ x1, …, xn ⋅ w'0 w'1 … w'm. Par α-renommage, on peut supposer que x1, ..., xn sont fraîches. Par hypothèse de récurrence on a u'0 [x:=u1] ⇒s w'0 [x:=w1], u'1 [x:=u1] ⇒s w'1 [x:=w1], ..., u'm [x:=u1] ⇒s w'm [x:=w1]. Donc u' [x:=u1] ⇒s w' [x:=w1].

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

    Si u ⇒s w par la clause 1 de la définition de ⇒s, c'est que w est une variable, et est donc normale. Mais ceci contredit w → v, donc ce cas ne s'applique pas.

    Sinon, u ⇒s w par la clause 2, donc 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, et n≥ 1 ou m≥ 1. 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. 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 la clause 2 de la définition de ⇒s.

    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, et le coeur de la preuve.

    Dans ce cas, w0 est une abstraction λ x ⋅ w' et la réduction donnée de u vers v est de la forme:
    u →t* λ x1, …, xn ⋅ (λ x⋅ u') u1 u2 … um
    →* λ x1, …, xn ⋅ (λ x⋅ w') w1 w2 … wm
    → λ x1, …, xn ⋅ w' [x:=w1] w2 … wm = v
    avec u' ⇒s w', u1 ⇒s w1, ..., um ⇒s wm et m ≥ 1. Noter en particulier que la tête de u, qui se réécrit en λ x⋅ w' est bien une abstraction, donc nécessairement de la forme λ x ⋅ u' avec u' ⇒s w': si ce n'était pas le cas, la tête de u n'étant jamais une application ne pourrait être qu'une variable, qui serait normale et donc ne pourrait se réduire vers λ x ⋅ w'.

    Mais du coup on pouvait déjà directement réduire (λ x⋅ u') u1 sans attendre que u1 se réduise en w1, et produire la réduction:
    u →t* λ x1, …, xn ⋅ (λ x⋅ u') u1 u2 … um →t λ x1, …, xn ⋅ u' [x:=u1] u2 … um
    Par le point 3 ci-dessus, u' [x:=u1] ⇒s w' [x:=w1], et comme u2 ⇒s w2, ..., un ⇒s wn, il s'ensuit que u ⇒s v par la clause 2 de la définition de ⇒s.
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 22   Montrer que si u →* x, où x est une variable, alors il existe une réduction de tête de u à x. (Regarder la preuve du théorème 3.)


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. Disons tout de suite que ce n'est pas, en fait, une panacée.

Previous Up Next