Assignment 6

Home

Lambda Calculus

Related Reading: Handout on Lambda Calculus

Due:  Midnight Sunday March 2, 2008

  1. Give both normal-order and applicative-order reduction sequences for the following lambda expressions:
     
    bullet(λf. λx. f (f x)) (λb. λx. λy. b y x) (λz. λw. z)
    bullet(λd. d d) (λf. λx. f (f x))
     
  2. Using the following definition of a fixed point operator in Haskell:
     
        y f = f (y f)
     
    do the following:
    bulletRewrite the following definition of an exponentiation function:
        exp x n = if n==0 then 1 else x * exp x (n-1)
    in a non-recursive way.  Test your program.
     
    bulletRewrite the following infinite list of ones:
        ones = 1 : ones
    in a non-recursive way.  Test your program by "take"ing the first 10 elements.
     
  3. Define a lambda calculus term iszero such that: iszero n returns true (as defined in the LC handout) if n is zero, and returns false otherwise.
     
  4. Using cond, one, and Y from the LC handout; iszero defined above; and these definitions of the predecessor function and multiplication, respectively:
     
        pred
    = λ n. λ s. λ z. n (λ n. λ f. f (n s)) (λ f. z) (λ x.x)
        mult = λm. λn. λf . m (n f)
     

    give a pure-lambda calculus definition of the exponentiation function that we defined in Haskell above.  To test your program, try using the interactive lambda calculus reducer found here:
    http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html .