1.8 La réduction standard du l-calcul
On a vu précédemment qu'un terme normalisable n'est pas nécessairement
fortement normalisable. Il existe de ``mauvaises'' stratégies qui, sur
un terme donné, ne terminent pas alors que d'autres terminent.
On donne ici une stratégie qui termine sur tout terme normalisable.
Si elle est sure, elle n'est généralement pas optimale, hélas.
On remarque facilement que tout l-terme M est de la forme
l x1x2··· xn.M1 M2 ··· Mk
où M1 est soit une variable, soit une abstraction.
Définition 3 Si M1 est une variable x, cette variable est appelée variable de tête
de M. On dit alors que M est en forme normale de tête.
Dans le cas contraire, on a M1=l y.N1, et le redex
(l y.N1)M2 est appelé ``redex de tête'' de M. La stratégie
standard consiste
-
dans le cas où il y a un redex de tête, à le réduire,
- et si, par contre, M est en forme normale de tête, à appliquer la
réduction standard à chacun des M2, ..., Mk
(ce sont des réductions indépendantes ; on pourrait les mener en
parallèle).
Voici (sans démonstration) le résultat annoncé :
Théorème 3 Appliquée à un terme normalisable, la réduction standard termine.
Deux situations sont possibles, quand on applique la réduction
standard à un terme :
-
on aboutit à une forme normale de tête.
Le terme est alors dit solvable.
- Cela ne termine pas, et il n'y a jamais de forme normale de tête. Terme
non solvable. C'est le cas de W.
Un terme solvable n'est pas forcément normalisable ; il se peut que la
réduction standard produise une suite infinie de formes normales de
têtes. On peut alors voir chaque variable de tête successive comme un
``bout d'information'' sur une donnée infinie qu'on n'atteindra jamais dans
sa totalité. Exemple : soit A=l xy.y(x x) alors le terme
A A est de cette sorte, puisqu'en effet :
AA® l y.y(AA)®l y.y(l y.y(AA))®···
et on produit ainsi la liste des variable de tête y,y....
Pour finir, voici un exemple qui montre que la réduction standard n'est pas
optimale en général. Soit I=l x.x l'identité. On considère
B=(l y.y y)(I I). Si on applique la stratégie standard :
B® II(II)® I(II)® II® I
mais on aurait pu réduire d'abord à droite (le redex II) dans B,
ce qui aurait donné par exemple :
B®(l y.y y)I® II® I
soit trois étapes au lieu de quatre.