+
1. `Kxy` +
2. `KKxy` +
3. `KKKxy` +
4. `SKKxy` +
5. `SIII` +
6. `SII(SII)` +
-16. Give Combinatorial Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`. +18. Give Combinatory Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. Provide combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`. Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic: -17. `\x x` -18. `\x y. x` -19. `\x y. y` -20. `\x y. y x` -21. `\x. x x` -22. `\x y z. x (y z)` +
+
1. `\x x` +
2. `\x y. x` +
3. `\x y. y` +
4. `\x y. y x` +
5. `\x. x x` +
6. `\x y z. x (y z)` +
-23. For each of the above translations, how many `I`s are there? Give a rule for describing what each `I` corresponds to in the original lambda term. +25. For each of the above translations, how many `I`s are there? Give a rule for describing what each `I` corresponds to in the original lambda term. + +Evaluation strategies in Combinatory Logic +------------------------------------------ + +26. Find a term in CL that behaves like Omega does in the Lambda +Calculus. Call it `Skomega`. + +27. Are there evaluation strategies in CL corresponding to leftmost +reduction and rightmost reduction in the Lambda Calculus? +What counts as a redex in CL? + +28. Consider the CL term `K I Skomega`. Does leftmost (alternatively, +rightmost) evaluation give results similar to the behavior of `K I +Omega` in the Lambda Calculus, or different? What features of the +Lambda Calculus and CL determine this answer? + +29. What should count as a thunk in CL? What is the equivalent +constraint in CL to forbidding evaluation inside of a lambda abstract? + + +More Lambda Practice +-------------------- + +Reduce to beta-normal forms: + +
+
1. `(\x. x (\y. y x)) (v w)` +
2. `(\x. x (\x. y x)) (v w)` +
3. `(\x. x (\y. y x)) (v x)` +
4. `(\x. x (\y. y x)) (v y)` + +
5. `(\x y. x y y) u v` +
6. `(\x y. y x) (u v) z w` +
7. `(\x y. x) (\u u)` +
8. `(\x y z. x z (y z)) (\u v. u)` +
+