let x = 2;; let y = 2;; x y;; let rec church n = fun f x -> if n = 0 then x else f (church (n - 1) f x);; let zero = "";; let succ = fun x -> "|" ^ x;; church 5 succ zero;; let add = fun m n f x -> m f (n f x);; add (church 3) (church 6) succ zero;; let exp = fun m n -> n m;; exp (church 3) (church 3);; exp (church 3) (church 3) succ zero;; let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));; let f x = x x;; !def T = \x y. x !def F = \x y. y !def ite = \c t e. c t e ite T x y !trace ite T x y ite F x y !def pair = \x y f. f x y !def fst = \p. p T fst (pair T F) !def 0 = \f x. x !def 1 = \f x. f x !def 3 = \f x. f (f (f x)) !def add = \m n f x. m f (n f x) add 3 3 !def exp = \m n. n m exp 3 3 !def nil = \x. x !def null = fst null null nil !def Y = \f. (\x. f (x x)) (\x. f (x x)) !def len = Y (\f x. ite (null x) 0 (add 1 (f (tl x)))) length nil !trace length (cons 1 nil) length (cons 1 (cons 1 nil)) len (cons 1 (cons 1 nil))