La récursion

1.6 La récursion

En essayant de définir l'addition, on serait tenté de la définir de la façon suivante:

add = lmn. if (iszero n) then m else s(add m (pred n))

Or ceci ne marche pas, car ``add'' est purement une abbréviation, si bien qu'il faudrait remplacer son occurrence dans le corps de la définition par la définition elle même, qui contient une occurrence de ``add'' qui doit être remplacée ...et ainsi de suite.

La solution est donnée par l'opérateur de point fixe Y, qui a la propriété suivante : pour toute fonction F,

(Y F) @ F(Y F)

où @ est l'équivalence engendrée par ®, appelée b-conversion. Plusieurs opérateurs, munis de cette propriété, ont été définis. Par exemple:

Y = (l f. (l s. f (s s)) (l s. f (s s)))

La somme sera alors définie en faisant d'abord une abstraction sur le symbole add dans la définition précédente, puis en appliquant Y:

add1 = l fmn. if (iszero n) then m else succ (f m (pred n))
add = Y add1

Exercice: démontrer que (Y F) @ F(Y F).

Exemple:

add 9 1	@	(Y add1) 9 1
	=	(l f. (l s. f (s s)) (l s. f (s s))) add1 9 1
	®	(l s. add1 (s s )) (l s. add1 ( s s)) 9 1
	®	add1 ((l s. add1 (s s)) (l s. add1 (s s))) 9 1
	=	add1 (Y add1) 9 1
	=	( l fmn. if (iszero n) then m else succ (f m (pred n)) ) (Y add1) 9 1
	®	if (iszero 1) then 9 else succ ((Y add1) 9 0)
	®	succ add1 (Y add1) 9 0
	®	succ (if (iszero 0) then 9 else succ ((Y add1) 9 (pred 0)) )
	®	succ 9
	®	10