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:

1. x x (x x x) x
2. v w (\x y. v x)
3. (\x y. x) u v
4. w (\x y z. x z (y z)) u v

Mark all occurrences of x y in the following terms:

5. (\x y. x y) x y
6. (\x y. x y) (x y)
7. \x y. x y (x y)

Reduce to beta-normal forms:

8. (\x. x (\y. y x)) (v w)
9. (\x. x (\x. y x)) (v w)
10. (\x. x (\y. y x)) (v x)
11. (\x. x (\y. y x)) (v y)

12. (\x y. x y y) u v
13. (\x y. y x) (u v) z w
14. (\x y. x) (\u u)
15. (\x y z. x z (y z)) (\u v. u)

Combinatory Logic

Reduce the following forms, if possible:

16. Kxy
17. KKxy
18. KKKxy
19. SKKxy
20. SIII
21. SII(SII)

22. Give Combinatory Logic combinators that behave like our boolean functions. You'll need combinators for true, false, neg, and, or, and xor.

Using the mapping specified in the lecture notes, translate the following lambda terms into combinatory logic:

23. \x.x
24. \xy.x
25. \xy.y
26. \xy.yx
27. \x.xx
28. \xyz.x(yz)
29. 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
make-list ≡ \hd tl. \f z. f hd (tl f z)
isempty ≡ \lst. lst (\hd sofar. false) true
extract-head ≡ \lst. lst (\hd sofar. hd) junk

The junk in extract-head is what you get back if you evaluate:

extract-head empty

As we said, the predecessor and the extract-tail functions are harder to define. We'll just give you one implementation of these, so that you'll be able to test and evaluate lambda-expressions using them in Scheme or OCaml.

predecesor ≡ (\shift n. n shift (make-pair zero junk) get-second) (\pair. pair (\fst snd. make-pair (successor fst) fst))

extract-tail ≡ (\shift lst. lst shift (make-pair empty junk) get-second) (\hd pair. pair (\fst snd. make-pair (make-list hd fst) fst))

The junk is what you get back if you evaluate:

predecessor zero

extract-tail 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:

(make-list a (make-list b (make-list c (make-list d (make-list e empty)))))

16. What would be the result of evaluating (see Assignment 2 hint for a hint):

    LIST make-list empty
    

17. Based on your answer to question 16, how might you implement the map function? Expected behavior:

    map f LIST <~~> (make-list (f a) (make-list (f b) (make-list (f c) (make-list (f d) (make-list (f e) empty)))))
    

18. 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, and e such that f applied to them evaluates to true.

19. What goes wrong when we try to apply these techniques using the version 1 or version 2 implementation of lists?

20. Our version 3 implementation of the numbers are usually called "Church numerals". If m is a Church numeral, then m s z applies the function s to the result of applying s to ... to z, for a total of m applications of s, where m is the number that m represents or encodes.

    Given the primitive arithmetic functions above, how would you implement the less-than-or-equal function? Here is the expected behavior, where one abbreviates succ zero, and two abbreviates succ (succ zero).

    less-than-or-equal zero zero ~~> true
    less-than-or-equal zero one ~~> true
    less-than-or-equal zero two ~~> true
    less-than-or-equal one zero ~~> false
    less-than-or-equal one one ~~> true
    less-than-or-equal one two ~~> true
    less-than-or-equal two zero ~~> false
    less-than-or-equal two one ~~> false
    less-than-or-equal 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.