`Kxy ~~> x`

`KKxy ~~> Ky`

`KKKxy ~~> Kxy ~~> x`

`SKKxy ~~> Kx(Kx)y ~~> xy`

`SIII ~~> II(II) ~~> II ~~> I`

`SII(SII) ~~> I(SII)(I(SII)) ~~> SII(SII) ~~> ...`

; the reduction never terminates

`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)
`[\x x] = @x x = I`

`[\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(K`

will behave just like*M*)I

for any expression*M**M*`[\x y. y] = @x [\y. y] = @x (@y y) = @x I = KI`

`[\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`[\x. x x] = @x (x x) = S (@x x) (@x x) = SII`

`[\x y z. x (y z)] =`

; this is the

@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)**B**combinator, which can also be expressed more concisely as`S (K S) K`

`(\x. x (\y. y x)) (v w) ~~> v w (\y. y (v w))`

`(\x. x (\x. y x)) (v w) ~~> v w (\x. y x)`

`(\x. x (\y. y x)) (v x) ~~> v w (\y. y (v x))`

`(\x. x (\y. y x)) (v y) ~~> v w (\u. u (v y))`

`(\x y. x y y) u v ~~> u v v`

`(\x y. y x) (u v) z w ~~> z (u v) w`

`(\x y. x) (\u u) ~~> \y u. u`

, also known as`false`

`(\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`