(fun  (z)  fun  (t)  fun  (f)  (z t) f) (fun  (x)  fun  (y)  x)
1 2 ®
((fun  (tfun  (f)  (z t) f) {z ¬ fun  (xfun  (yx}) 1 2 º
(fun  (t)  fun  (f)  (fun  (x)  fun  (y)  x) t f)
1 2 ®
((fun  (f)  ((fun  (xfun  (yx) t) f) {t ¬ 1}) 2 º
(fun  (f)  (fun  (x)  fun  (y)  x) 1 f) 2
®
(((fun  (xfun  (yx) 1) f) {f ¬ 2} º
(
(fun  (x)  fun  (y)  x) 1
2) ®
((fun  (yx) {x ¬ 1}) 2) º
(fun  (y)  1) 2
®
1 {y ¬ 2} º
1
On peut vérifier le résultat de ce calcul en évaluant cette expression écrite dans la syntaxe Ocaml:
(fun z t f -> (z t) f) (fun x y -> x) 1 2;;
- : int = 1