For these assignments, you'll probably want to use our lambda evaluator to check your work. This accepts any grammatical lambda expression and reduces it to normal form, when possible.
More Lambda Practice
Insert all the implicit ( )
s and λ
s into the following abbreviated expressions:
x x (x x x) x
v w (\x y. v x)
(\x y. x) u v
w (\x y z. x z (y z)) u v
Mark all occurrences of x y
in the following terms:
(\x y. x y) x y
(\x y. x y) (x y)

\x y. x y (x y)
Reduce to betanormal forms:
(\x. x (\y. y x)) (v w)
(\x. x (\x. y x)) (v w)
(\x. x (\y. y x)) (v x)
(\x. x (\y. y x)) (v y)
(\x y. x y y) u v
(\x y. y x) (u v) z w
(\x y. x) (\u u)
(\x y z. x z (y z)) (\u v. u)
Combinatory Logic
Reduce the following forms, if possible:

Kxy

KKxy

KKKxy

SKKxy

SIII

SII(SII)
 Give Combinatory Logic combinators that behave like our boolean functions.
You'll need combinators for
true
,false
,neg
,and
,or
, andxor
.
Using the mapping specified in the lecture notes, translate the following lambda terms into combinatory logic:

\x.x

\xy.x

\xy.y

\xy.yx

\x.xx

\xyz.x(yz)
 For each translation, how many I's are there? Give a rule for describing what each I corresponds to in the original lambda term.
Lists and Numbers
We'll assume the "Version 3" implementation of lists and numbers throughout. So:
zero ≡ \s z. z
succ ≡ \n. \s z. s (n s z)
iszero ≡ \n. n (\x. false) true
add ≡ \m \n. m succ n
mul ≡ \m \n. \s. m (n s)
And:
empty ≡ \f z. z
makelist ≡ \hd tl. \f z. f hd (tl f z)
isempty ≡ \lst. lst (\hd sofar. false) true
extracthead ≡ \lst. lst (\hd sofar. hd) junk
The junk
in extracthead
is what you get back if you evaluate:
extracthead empty
As we said, the predecessor and the extracttail functions are harder to define. We'll just give you one implementation of these, so that you'll be able to test and evaluate lambdaexpressions using them in Scheme or OCaml.
predecesor ≡ (\shift n. n shift (makepair zero junk) getsecond) (\pair. pair (\fst snd. makepair (successor fst) fst))
extracttail ≡ (\shift lst. lst shift (makepair empty junk) getsecond) (\hd pair. pair (\fst snd. makepair (makelist hd fst) fst))
The junk
is what you get back if you evaluate:
predecessor zero
extracttail empty
Alternatively, we might reasonably declare the predecessor of zero to be zero (this is a common construal of the predecessor function in discrete math), and the tail of the empty list to be the empty list.
For these exercises, assume that LIST
is the result of evaluating:
(makelist a (makelist b (makelist c (makelist d (makelist e empty)))))
 What would be the result of evaluating (see Assignment 2 hint for a hint):
LIST makelist empty
 Based on your answer to question 16, how might you implement the map function? Expected behavior:
map f LIST <~~> (makelist (f a) (makelist (f b) (makelist (f c) (makelist (f d) (makelist (f e) empty)))))
 Based on your answer to question 16, how might you implement the filter function? The expected behavior is that:
filter f LIST
should evaluate to a list containing just those of
a
,b
,c
,d
, ande
such thatf
applied to them evaluates totrue
.  What goes wrong when we try to apply these techniques using the version 1 or version 2 implementation of lists?
 Our version 3 implementation of the numbers are usually called "Church numerals". If
m
is a Church numeral, thenm s z
applies the functions
to the result of applyings
to ... toz
, for a total of m applications ofs
, where m is the number thatm
represents or encodes.Given the primitive arithmetic functions above, how would you implement the lessthanorequal function? Here is the expected behavior, where
one
abbreviatessucc zero
, andtwo
abbreviatessucc (succ zero)
.lessthanorequal zero zero ~~> true lessthanorequal zero one ~~> true lessthanorequal zero two ~~> true lessthanorequal one zero ~~> false lessthanorequal one one ~~> true lessthanorequal one two ~~> true lessthanorequal two zero ~~> false lessthanorequal two one ~~> false lessthanorequal two two ~~> true
You'll need to make use of the predecessor function, but it's not essential to understand how the implementation we gave above works. You can treat it as a black box.