lambda calculus Flashcards
x is free in (E,F) iff
x is free in E or x is free in F
x is free in (Ly . E) iff
x and y are diff var and x is free in E
x is bound in (E,F) iff
x is bound in E or x is bound in F
x is bound in (Ly. E) iff
x and y are same var and x occurs free in E or x occurs bound in E
x [M/x] =
M
c [M/x] (whr c is any var or constant other than x)= =
c
(E F) [M/x]
= (E [M/x]) (F [M/x])
(Lx. E) [M/x] (whr y is any var other than x) = two answers
= Ly.(E[M/x]) if x does not occur free in E or y does not occur free in M
= Lz.(E[z/y])[M/x] otherwise, whr z is new var and is not free in E or M
a-conversion:
if y is not free in E then
(Lx.E) ?
(Ly.E[y|x])
b-conversion:
(Lx.E)M ?
E[M|x]
n-conversion:
if x is not free in E and E denotes a func
(Lx. Ex) ?
E
define normal form
(Lx.xx)(Lx.xx) cannot be reduced ; no redex’s
define delta-reduction
built in constant functions i.e. + or -
y combinator:
Yf = ?
f (Yf)
y combinator:
y returns the fixpoint of f; y is expressed in lambda calc as:
Y = (Lh. (Lx. h(x x)) (Lx.h(x x)))
y combinator:
write factorial function FAC =
Y (Lfac. Ln. if (= n 0) 1 (* n (fac (- n 1 ))))
applicative order reduction
leftmost, innermost redex first
normal order evaluation
leftmost, outermost redex first
church-rosser theorem I
if E1 E2, then there exists an expression E such that E1 => E; E2 => E;
No expression can be converted to two distinct normal forms (normal forms that are not a-interconvertible)
church-rosser theorem ii
if E1 => E2 and E2 is in norm form, then there exists a norm reduction seq from E1 to E2
