lambda calculus

Question 1

x is free in (E,F) iff

Answer 1

x is free in E or x is free in F

Question 2

x is free in (Ly . E) iff

Answer 2

x and y are diff var and x is free in E

Question 3

x is bound in (E,F) iff

Answer 3

x is bound in E or x is bound in F

Question 4

x is bound in (Ly. E) iff

Answer 4

x and y are same var and x occurs free in E or x occurs bound in E

Question 5

x [M/x] =

Answer 5

M

Question 6

c [M/x] (whr c is any var or constant other than x)= =

Answer 6

c

Question 7

(E F) [M/x]

Answer 7

= (E [M/x]) (F [M/x])

Question 8

(Lx. E) [M/x] (whr y is any var other than x) = two answers

Answer 8

= 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

Question 9

a-conversion:
if y is not free in E then
(Lx.E) ?

Answer 9

(Ly.E[y|x])

Question 10

b-conversion:

(Lx.E)M ?

Answer 10

E[M|x]

Question 11

n-conversion:
if x is not free in E and E denotes a func
(Lx. Ex) ?

Answer 11

E

Question 12

define normal form

Answer 12

(Lx.xx)(Lx.xx) cannot be reduced ; no redex’s

Question 13

define delta-reduction

Answer 13

built in constant functions i.e. + or -

Question 14

y combinator:

Yf = ?

Answer 14

f (Yf)

Question 15

y combinator:

y returns the fixpoint of f; y is expressed in lambda calc as:

Answer 15

Y = (Lh. (Lx. h(x x)) (Lx.h(x x)))

Question 16

y combinator:

write factorial function FAC =

Answer 16

Y (Lfac. Ln. if (= n 0) 1 (* n (fac (- n 1 ))))

Question 17

applicative order reduction

Answer 17

leftmost, innermost redex first

Question 18

normal order evaluation

Answer 18

leftmost, outermost redex first

Question 19

church-rosser theorem I

Answer 19

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)

Question 20

church-rosser theorem ii

Answer 20

if E1 => E2 and E2 is in norm form, then there exists a norm reduction seq from E1 to E2