Homework Assignment

constants of type e : a b c
constants of type <e,t> : P-Q
constants of type <e*e,t> : R
variables of type e : u-z
variables of type <e,t> : X Y


exercise lambda conversion
title Lambda Conversion
directions After checking that the type of the function and the type of the
directions argument(s) match, simplify the following expressions performing
directions one lambda-conversion at a time.
points per exercise 10

Lx.[P(x) & T(y,x)]     (a)
Lx.Ly.[Q(y) & R(x,y)]   (a)   (b)
Lx.Ly.[R(x,y) & R(y,x)]   (a)  (b)
Lx.Ly.Ey[R(x,y) & Q(x)] (a) (b)
Lx.Ly.Lz.[R(y,y) V R(x,z)]    (a)    (b)   (c)
Ly.[Q(b) V R(b,b)]    (a)
Lx.Ly.Az[R(y,z) -> Ey(R(x,y))]   (a)   (b)
# Ly.Lx.~Ey[Q(y) & Ax(R(x,y))]   (a)   (b)
Lx.Ly.Lx.[R(x,b) & T(y)]   (a)  (b)  (c)
Lx.Ey[R(x,y) & T(y)]    (y)
# Lx.Ly.[ExEy[R(x,y)] -> P(x) & Q(y)]  (a)  (b)
Lx.Ly.[T(x) & Az[P(z) -> R(x,y)]]  (z) (z)