Home
| |
Lambda Calculus
Related Reading:
Handout on Lambda Calculus
Due: Midnight Sunday March 2,
2008
- Give both normal-order and applicative-order reduction
sequences for the following lambda expressions:
 | (λf. λx. f (f x)) (λb. λx. λy. b y x) (λz. λw. z) |
 | (λd. d d) (λf. λx. f (f x))
|
Using the following definition of a fixed point
operator in Haskell:
y f = f (y f)
do the following:
 | Rewrite 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.
|
 | Rewrite the following infinite list of ones:
ones = 1 : ones
in a non-recursive way. Test your program by "take"ing
the first 10 elements.
|
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.
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 .
|