Il existe plusieurs codages des entiers dans le l-calcul.
Le premier, du à Church,fut présenté dans les années 1931-32.
1.5.1 Les numéraux de Church
Un nombre est représenté comme un terme qui représente n applications
successives d'une fonction à un argument (si le nombre en question est
n).
Le nombre n sera représenté par l fx.fnx
0=l fx.x
1=l fx.fx
n=l fx.fnx ce qui équivaut à
l fx.(f(f ... (fx)...))
La fonction successeur, s , doit prendre un numéral n de la forme
l fx.fnx et rendre l fx.f(fnx). On peut ``ouvrir''
le numéral n en l'appliquant à deux arguments quelconques,
par exemple à f et à x :
(l fx.fnx) fx ® fnx
Pour obtenir le successeur de n il faut donc ``capturer'' n,
l'ouvrir,lui ajouter un f en tête, et ``laisser'', à la tête de tout
ca un nouveau l fx.
Ceci est fait par la fonction:
s = l nfx . f(nfx)
Nous pouvons à l'aide de s définir des simples fonctions comme la somme
add = l mn.m s n
.
D'autres fonctions, comme la fonction prédécesseur sont toutefois difficiles à définir avec les numéraux de Church. La récursion est aussi assez
laborieuse.
1.5.2 Une autre représentation des entiers
Cette représentation des entiers, qui vient de Barendregt, nous permettra
d'utiliser le calcul sur les booléens que nous avons déja défini.
Soient:
0 = l x.x
s = ln.lf. ((f F) n)
Si nous appliquons un numéral n
(n = sn 0) à T (i.e. l xy. x)
nous obtenons de façon triviale T ou F, selon que n est 0
ou un autre numéral:
