Untyped Lambda Calculus


What is the Grammar of Lambda Calculus?

t ::=       terms
    x       variable
    λx.t    abstraction
    t t     application

How are things grouped together? - application associates to the left: s t u = (s t) u - bodies of abstractions are taken to extend as far to the right as possible. λx. λy. x y x = λx. (λy. ((x y) x))

What is [x ↦ t_2]t_12 in (λx.t_12)t_2 ⟶ [x ↦ t_2]t_12? The term obtained by replacing all free occurrences of x in t_12 t_2.

What is a free variable? An occurrence of x is free if it appears in a position where it is not bound by an enclosing straction on x.

What is a redex? A term of the form (λx.t_12) t2

What is a closed term? A term with no free variables

What is a beta reducion? Applying (λx.t_12)t_2 ⟶ [x ↦ t_2]t_12 on a redex

What are the various evaluation strategies? - full beta-reduction: any redex can be reduced at any time - normal order strategy: leftmost, outermost redex is reduced first - call by name: normal order + no reductions inside abstractions. optimized version: call by need - call by value: normal order + redex is reduced only when its rhs is reduced to a value

Programming in the Lambda Calculus

How to get multiple arguments? f = λ(x, y).s can be rewritten as f = λx.λy.s. Instead of f v w, we apply like: ((f v) w).

How to implement Booleans?

tru = λt. λf. t;
fls = λt. λf. f;

How to implement boolean operators?

and  = λb. λc. b c fls;
or   = λb. λc. b tru c;
not  = λb. b fls tru;

How to implement Pairs?

pair = λf. λs. λb b f s;
fst  = λp. p tru;
snd  = λp. p fls;

How to implement Numbers?

c_0 = λs. λz. z; c_1 = λs. λz. s z; c_2 = λs. λz. s (s z); c_3 = λs. λz. s (s (s z)); etc.

takes in a succ (s) and 0 and applies succ to n times to 0.

scc = λn λs. λz. s (n s z)

scc takes in a church numeral and applies the successor to it

Another successor func:

scc = λn λs. λz. n (s (s z))

plus = λm. λn. λs λz. m s (n s z)

times = λm. λn. m (plus n) c_0

Is it possible to define times w/o using plus?

expt = `l