1.2 b-réduction
C'est la règle fondamentale du l-calcul. Un terme de la forme
(l x.M)N est appelé redex. Voici la réduction d'un
redex :
(l x.M)N ®0 M[N/x]
à condition que x n'apparaisse pas libre dans N (si c'est le cas,
faire une a conversion sur l x.M) et qu'aucune variable libre
de N ne soit capturée dans M
(là aussi faire une a conversion sur M).
Le terme de droite est appelé réduit.
Ce qu'on appellera b-réduction, c'est la réduction d'un redex à
l'intérieur d'un terme. Plus précisément, c'est la relation de
réduction ® définie par
-
Si M®0 M' alors M® M'.
- Si M® M' alors l x.M®l x.M'.
- Si M® M' alors M N®M' N.
- Si N® N' alors M N®M N'.
C'est grâce à cette règle que le l-calcul est véritablement
un calcul. Voici des exemples.