(fun  (z)  fun  (t)  fun  (f)  (z t) f) (fun  (x)  fun  (y)  x) 1 2 ® ((fun  (t)  fun  (f)  (z t) f) {z ¬ fun  (x)  fun  (y)  x}) 1 2 º (fun  (t)  fun  (f)  (fun  (x)  fun  (y)  x) t f) 1 2 ® ((fun  (f)  ((fun  (x)  fun  (y)  x) t) f) {t ¬ 1}) 2 º (fun  (f)  (fun  (x)  fun  (y)  x) 1 f) 2 ® (((fun  (x)  fun  (y)  x) 1) f) {f ¬ 2} º ( (fun  (x)  fun  (y)  x) 1 2) ® ((fun  (y)  x) {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