+
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 ------------------------------------------ -23. Find a term in CL that behaves like Omega does in the Lambda -Calculus. Call it Skomega. +26. Find a term in CL that behaves like Omega does in the Lambda +Calculus. Call it `Skomega`. -24. Are there evaluation strategies in CL corresponding to leftmost -reduction and rightmost reduction in the lambda calculus? -What counts as a redex in CL? +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? -25. 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? +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? -26. What should count as a thunk in CL? What is the equivalent +29. What should count as a thunk in CL? What is the equivalent constraint in CL to forbidding evaluation inside of a lambda abstract? @@ -92,15 +101,15 @@ 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)` +
+
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)` +
9. `(\x y. x y y) u v` +
10. `(\x y. y x) (u v) z w` +
11. `(\x y. x) (\u u)` +
12. `(\x y z. x z (y z)) (\u v. u)`