1. `Kxy ~~> x`
2. `KKxy ~~> Ky`
3. `KKKxy ~~> Kxy ~~> x`
4. `SKKxy ~~> Kx(Kx)y ~~> xy`
5. `SIII ~~> II(II) ~~> II ~~> I`
6. `SII(SII) ~~> I(SII)(I(SII)) ~~> SII(SII) ~~> ...`; the reduction never terminates
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`. > As Dan pointed out in the Wednesday session, this problem is easy to solve if you first come up with a Combinatory translation of the schema `\p. if p then M else N`: > [\p. p M N] = > @p. p [M] [N] = > S (@p. p [M]) (@p [N]) = > S (S (@p p) (@p [M])) (@p [N]) = > S (S I (@p [M])) (@p [N]) = > S (S I (K [M])) (K [N]) > The last step assumes that `p` does not occur free in the expressions `M` and `N`. > Next, we translate `true ≡ \y n. y` as `K`, and `false ≡ \y n. n` as `KI`. Then we rely on the following equivalences: > neg ≡ \p. if p then false else true > and ≡ \p. if p then I else K false > ; then: and p q <~~> if p then I q else K false q ~~> if p then q else false > or ≡ \p. if p then K true else I > ; then: or p q <~~> if p then K true q else I q ~~> if p then true else q > xor ≡ \p. if p then neg else I > ; then: xor p q <~~> if p then neg q else I q ~~> if p then neg q else q > Then we just make use of the schema derived above to complete the translations. For example, `and ≡ \p. if p then I else K false` becomes `S (SI (K I)) (K (K false)) ≡ S (SI (K I)) (K (K (KI)))`. > In the case of `neg`, this produces `S (SI (K false)) (K true) ≡ S (SI (K (KI))) (K K)`. A more compact result here can be obtained here by observing that for boolean arguments, `neg` can also be defined as `\p y n. p n y`, which is just the `C` combinator. Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic: Let's say that for any lambda term T, [T] is the equivalent Combinatory Logic term. Then we define the [.] mapping as follows. 1. [a] = a 2. [(\aX)] = @a[X] 3. [(XY)] = ([X][Y]) Wait, what is that @a ... business? Well, that's another operation on (a variable and) a CL expression, that we can define like this: 4. @aa = I 5. @aX = KX if a is not in X 6. @a(Xa) = X if a is not in X 7. @a(XY) = S(@aX)(@aY)
1. `[\x x] = @x x = I`
2. `[\x y. x] = @x [\y. x] = @x. (@y x) = @x (Kx) = S (@x K) (@x x) = S (KK) I`; in general expressions of this form `S(KM)I` will behave just like `M` for any expression `M`
3. `[\x y. y] = @x [\y. y] = @x (@y y) = @x I = KI`
4. `[\x y. y x] = @x [\y. y x] = @x (@y (y x)) = @x (S (@y y) (@y x)) = @x (S I (Kx)) = S (@x (SI)) (@x (Kx)) = S (K(SI)) K` ; this is the T combinator
5. `[\x. x x] = @x (x x) = S (@x x) (@x x) = SII`
6. ```[\x y z. x (y z)] = @x (@y (@z (x (y z)))) = @x (@y (S (@z x) (@z (y z)))) = @x (@y (S (Kx) (@z (y z)))) = @x (@y (S (Kx) y)) = @x (S (@y (S (Kx))) (@y y)) = @x (S (K (S (Kx))) (@y y)) = @x (S (K (S (Kx))) I) = S (@x (S (K (S (Kx))))) (@x I) = S (S (@x S) (@x (K (S (Kx))))) (@x I) = S (S (KS) (@x (K (S (Kx))))) (@x I) = S (S (KS) (S (@x K) (@x (S (Kx))))) (@x I) = S (S (KS) (S (KK) (@x (S (Kx))))) (@x I) = S (S (KS) (S (KK) (S (@x S) (@x (Kx))))) (@x I) = S (S (KS) (S (KK) (S (KS) (@x (Kx))))) (@x I) = S (S (KS) (S (KK) (S (KS) K))) (@x I) = S (S (KS) (S (KK) (S (KS) K))) (KI)```; this is the B combinator, which can also be expressed more concisely as `S (K S) K`
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`. > SII(SII) 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? > A redex is any `I` with one argument, or `K` with two arguments, or `S` with three arguments. > Leftmost reduction corresponds to applying the rules for an `I` or `K` or `S` in head position *before* reducing any of their arguments; rightmost reduction corresponds to reducing the arguments first. 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? > Leftmost reduction terminates with `I`; rightmost reduction never terminates. This is because "leftmost reduction" corresponds to "head-redex first", which gives the head combinator the opportunity to ignore some of its (in this case, unreducible) arguments without trying to reduce them. If the arguments are reduced first, the head combinator loses that opportunity. 29. What should count as a thunk in CL? What is the equivalent constraint in CL to forbidding evaluation inside of a lambda abstract? > Recall that a thunk is a function of the form `\(). EXPRESSION`, where `EXPRESSION` won't be evaluated until the function is applied (to the uninformative argument `()`). We don't really have `()` in the Lambda Calculus. The closest approximation would be `I`, since a triple is `\f. f a b c`, a pair is `\f. f a b`, and following the same pattern a one-tuple would be `\f. f a` (not the same as `a`), and the zero-tuple would be `\f. f` or `I`. But really in the untyped Lambda Calculus, it doesn't matter whether you supply `I` to an abstract that's going to ignore its argument, or any other argument. Instead, you could get the same effect as a thunk by just using `\x. EXPRESSION`, where `x` is a variable that doesn't occur free in `EXPRESSION`. > The way to do the same thing in Combinatory Logic is `K (EXPRESSION)`. The constraint we need is that arguments to `S` and `K` are never reduced until there are enough of them to apply the rule for `S` and `K`. (If we furthermore insist on leftmost reduction, then expressions will *never* be reduced when in the position of an argument to another combinator. Only the reduction rules for the outermost head combinator are ever followed.) More Lambda Practice -------------------- Reduce to beta-normal forms:
1. `(\x. x (\y. y x)) (v w) ~~> v w (\y. y (v w))`
2. `(\x. x (\x. y x)) (v w) ~~> v w (\x. y x)`
3. `(\x. x (\y. y x)) (v x) ~~> v w (\y. y (v x))`
4. `(\x. x (\y. y x)) (v y) ~~> v w (\u. u (v y))`
5. `(\x y. x y y) u v ~~> u v v`
6. `(\x y. y x) (u v) z w ~~> z (u v) w`
7. `(\x y. x) (\u u) ~~> \y u. u`, also known as `false`
8. `(\x y z. x z (y z)) (\u v. u) ~~> \y z. (\u v. u) z (y z) ~~> \y z. z`, also known as `false`