1.7 Les théorèmes du l -calcul
Voici le premier théorème de ce cours. Il affirme que ce qu'on vient de
définir est bien un calcul, au sens où le résultat ne dépend pas de
l'ordre des réductions. C'est la moindre des chose ; par exemple, dans
l'arithmétique, quand on calcule (2+3)*(1+5), le résultat n'est pas
différent si vous réduisez d'abord 2+3 en 5 ou 1+5 en 6.
On note ®* la fermeture réflexive-transitive de la relation de
conversion ® définie précédemment. (Donc
M®*N si et seulement si il existe une suite finie
(M1,...,Mn) avec n³ 1 telle que M=M1,
N=Mn et M1® M2··· Mn.)
Théorème 1 (Church-Rosser)
Soit M un l-terme. Soient M1 et M2 des termes tels que
M®*M1 et M®*M2. Il existe un terme N tel que
M1®* N et M2®* N.
On ne donnera pas la preuve qui est plutôt technique et ne présente pas
beaucoup d'intérêt en soi (pour le non spécialiste). Ce théorème a une
conséquence intéressante.
Définition 2 On dit qu'un terme est en forme normale s'il ne possède aucun redex.
On dit qu'un terme a une forme normale, ou qu'il est normalisable, s'il
existe une réduction de ce terme (pour ®*) qui mène à une forme
normale. On dit qu'il est fortement normalisable si toute réduction pour
®* mène à une forme normale.
Alors, bien sûr
Théorème 2 Si un terme est normalisable, il a une unique forme normale.
C'est une conséquence immédiate du théorème de Church-Rosser.
(Pourquoi ?)
Remarquons qu'il existe des termes non normalisables :
soit W=(l x.x x)(l x.x x). On a
W®0W®0W®0···
Il existe aussi des termes normalisables
qui ne sont pas fortement normalisables.
C'est le cas le (l xy.y)W. Si l'on choisit de réduire d'abord le
redex qui se trouve à l'intérieur de W, et de continuer ensuite
dans cette voie, on est perdu. Sinon,
c'est-à-dire si l'on réduit le ``redex de tête''
(qui est le terme lui-même), on a gagné, car W disparaît.
Cet exemple laisse entrevoir que le choix de la stratégie de réduction est
crucial en l-calcul.