# Lambda-Calculus

## Encodings

zero = lambda s.lambda z.z; one = lambda s.lambda z.s z; two = lambda s.lambda z.s (s z); three = lambda s.lambda z.s (s (s z)); succ = lambda n.lambda s.lambda z.s (n s z); plus = lambda n.lambda m.lambda s.lambda z.n s (m s z); times = lambda n.lambda m.lambda s.lambda z.n (m s) z; true = lambda x.lambda y.x; false = lambda x.lambda y.y; if = lambda p.lambda a.lambda b.p a b; 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)); iszero = lambda n.n (lambda x.false) true;

## Natural Numbers

order normal; plus two three;
order cbv; trace on; plus two three; trace off;
order cbn; trace on; plus two three; trace off;

## Factorial

fct = lambda f.lambda n.if (iszero n) one (times n (f (pred n))); fct_direct = lambda n.n (lambda x.pair (plus (fst x) one) (times (snd x) plus (fst x) one)) (pair zero one);
order normal; snd (fct_direct three);

## Fixedpoint

typing off; step 5; trace on; (lambda x. x x) (lambda x. x x); order normal; lambda f. (lambda x.f (x x)) (lambda x.f (x x));
order cbn; y = lambda f.(lambda x.f (x x)) (lambda x.f (x x)); yfct = y fct; r = yfct three; order normal; r;
order cbv; y = lambda fun.(lambda f.(f f)) (lambda f.fun (lambda x.(f f) x)); dummy = lambda x.x; fct = lambda f.lambda n.if (iszero n) (lambda _.one) (lambda _.times n (f (pred n) dummy)); yfct = y fct; r = yfct three dummy; order normal; r;

## Interesting Types

lambda x. x; lambda f.lambda x.f x; lambda x.lambda f.lambda g.g (f x);

## References

1. Types and Programming Languages by Pierce, 2002.
2. Lambda-Calculus and Combinators, an Introduction by Hindley and Seldin, 1986, 2008.
3. Propositions as Types by Wadler, 2015.