Lambda Calculus Homework.
			
			    Sample Solutions


No more than two people can collaborate on this assignment.  Show work.


0. Identify the free and bound variables in the following term:

   lambda u. lambda x. x (lambda y.x u) y u
                                        ^
    >> The y on the right is the only free variable relative to 
    the whole term.


1. Determine if the following pairs of terms are alpha-equivalent.

   a.  lambda x.lambda y. (x y x)  and
       lambda x.lambda y. (y x y)

      >> NO

   b.  lambda x. lambda y. x (lambda y.x) y   and 
       lambda a. lambda b. a (lambda u.a) b
     
      >> YES - convert inner lambda y to lambda u first to see why.
      

For the rest of the problems, find the beta-normal forms of the
following terms.  Remember: you can rename bound variables to
avoid clash, but never free variables.

2. (lambda x.lambda y. (x y)) (lambda x.x) u

   -> (lambda y. ((lambda z.z) y)) u   - note alpha conversion 
   -> (lambda z.z) u
   -> u

   >> WARNING: I will sometimes combine up to 2 steps (-->) in the
      following solutions.  I'll also use the book's notation lambda
      xy to mean lambda x.lambda y - use the form you're comfortable
      with.


3. given S, K, I as they are in the handout, find the normal forms
   of KIK and SIK

   >> S = (lambda xyz.(x z)(y z))
      K = (lambda xy.x)
      I = lambda x.x

    KIK = [(lambd xy.x) (lambda u.u)] K
    -> (lambda y.lambda u.u) K 
    -> lambda u.u   
   (there's no y in the body (lambda u.u), so it doesn't change)

   SIK = (lambda xyz.(x z)(y z)) I K 
   -> (lambda yz.(I z) (y z)) K 
   -> lambda z.(I z) (K z)   (I will choose to reduce (I z) first:)
   =  lambda z.([lambda u.u] z) ([lambda ab.a] z)
   -> lambda z.z ([lambda ab.a] z)
   -> lambda z.z (lambda b.z)


4. given A = lambda m.lambda n.lambda f.lambda x. m f (n f x),
         T = lambda f.lambda x.f (f x)

   find the normal form of (A T T).
   Conjecture what would happen if T = lambda f.lambda x.f (f (f x)).

  >> ATT = (lambda mnfx.m f (n f x)) T T 
  --> lambda fx. T f (T f x)    
  = lambda fx. (lambda gy.g (g y)) f (T f x)  - I choose call by name
  -> lambda fx. (lambda y.f (f y)) (T f x)
  -> lambda fx. f (f (T f x))
  =  lambda fx. f (f ([lambda gy.g (g y)] f x))
  -> lambda fx. f (f ([lambda y.f (f y)] x))
  -> lambda fx. f (f (f (f x)))

  ** Call by value alternative: **
  ... lambda fx. T f (T f x) 
  = lambda fx. T f ([lambda gy.g (g y)] f x)
  -> lambda fx. T f ([lambda y.f (f y)] x)
  -> lambda fx. T f (f (f x))
  = lambda fx. (lambda gy. g (g y)) f (f (f x)) - careful with the ()'s!
  -> lambda fx. (lambda y. f (f y)) (f (f x))
  -> lambda fx. f (f (f (f x)))

  A is the "Church combinator" for addition.


5. Given T = lambda x. lambda y. x
         F = lambda x. lambda y. y
         A = lambda p.lambda q. (p q F)   (where F is as above)
    
   Find the normal forms of:
      
      a. (A F F)
      b. (A F T)
      c. (A T F)
      d. (A T T)

>> You now know that A is boolean conjunction, so the results are
   predicatable.  T chooses the first of 2 arguments, and F chooses
   the second.  When you solve such problems, be careful with the
   syntax but also keep in mind the intended *meaning* of the lambda
   terms.

   AFF = (lambda pq.p q F) F F
   -> (lambda q.F q F) F
   -> F F F
   = (lambda xy.y) F F   
   -> (lambda y.y) F
   -> F

   AFT = (lambda pq.p q F) F T
   --> F T F
   = (lambda xy.y) T F
   --> F

   ATF = (lambda pq.p q F) T F
   --> T F F
   = (lambda xy.x) F F
   -> (lambda y.F) F
   -> F

   ATT = (lambda pq.p q F) T T
   --> T T F
   = (lambda xy.x) T F
   --> T


6. Let T and F be as they were in the above problem, and let
   N = lambda x. (x F T)

   what are the normal forms of 

      a. (N F)
      b. (N T)
      c. (N (N F))

 >> NF = lambda x.(x F T) F
    -> F F T
    = (lambda xy.y) F T
    -> (lambda y.y) T
    -> T

    NT = lambda x.(x F T) T
    -> T F T
    = (lambda xy.x) F T
    -> F

    N (N F) = (lambda x.(x F T)) (N F) - becareful reading the parentheses!
    = (N F) F T  - now I'll borrow the normal form of (N F) found above:
    --->  T F T
    = (lambda xy.x) F T
    --> F

  N is boolean negation.


---

Here's the extra example I had posted on the homepage:

SKI =
(lambda xyz.(x z) (y z)) K I    ->
(lambda yz. (K z) (y z)) I      ->
lambda z. (K z) (I z) =
lambda z. ([lambda xy.x] z) ([lambda u.u] z)   ->   (choice point)
lambda z. (lambda y.z) ([lambda u.u] z)   ->
lambda z.z = 
I

In the last step, the term lambda y.z is applied to the large term
([lambda u.u] z) - but it doesn't matter how large this term is,
lambda y.z applied to ANYTHING will simply return z!  In other words,
delaying the reduction of ([lambda u.u] z) allowed me to avoid it
altogether - since it disappears when applied to lambda y.z.  At the
(choice point) step, we could also do:

lambda z. ([lambda xy.x] z) ([lambda u.u] z)   ->  
lambda z. ([lambda xy.x] z) z  ->
lambda z. (lambda y.z) z -> 
lambda z.z