Lambda-Calculus
typing off;
order normal;
true = lambda x.lambda y.x;
false = lambda x.lambda y.y;
if = lambda b.lambda t.lambda f.b t f;
not = lambda b.b false true;
and = lambda b1.lambda b2.b1 b2 false;
or = lambda b1.lambda b2.b1 true b2;
and true false;
and true (not true);
zero = lambda f.lambda x.x;
one = lambda f.lambda x.f x;
two = lambda f.lambda x.f (f x);
three = lambda f.lambda x.f (f (f x));
succ = lambda n.lambda f.lambda x.f (n f x);
succ two;
add = lambda n1.lambda n2.n1 succ n2;
add two three;
times = lambda n1.lambda n2.n1 (add n2) zero;
times two three;
iszero = lambda n.n (lambda b.false) true;
iszero zero;
iszero one;
iszero two;
pair = lambda x.lambda y.lambda f.f x y;
fst = lambda p.p true;
snd = lambda p.p false;
pred = lambda n.fst (n (lambda p.pair (snd p) (succ (snd p))) (pair zero zero));
pred two;
facti = lambda f.lambda n. if (iszero n) one (times n (f f (pred n)));
order cbv;
fact = facti facti;
fact3 = fact three;
order normal;
fact3;
order cbn;
factp = lambda f.lambda n.if (iszero n) one (times n (f (pred n)));
y = lambda f.(lambda x.f (x x)) (lambda x.f (x x));
fact = y factp;
fact;
step 5;
order cbv;
trace on;
y factp;
trace off;
order cbn;
step *;
order cbv;
z = lambda f.(lambda x.f (lambda y.x x y)) (lambda x.f (lambda y.x x y));
dummy = lambda x.x;
factv = lambda f.lambda n.if (iszero n) (lambda _.one) (lambda _.(times n (f (pred n) dummy)));
z factv;
z factv three;
thetai = lambda t.lambda f.f (t t f);
theta = thetai thetai;
order cbn;
theta factp;
order normal;
theta factp three;