This page contains proofs to some assertions that are left as exercises in Combinator engine.
I = S K K
To prove this, remember that
S x y z = x z { y z }
and
K x y = x
So what is S K K p?
S K K p = K p { K p } = p
B = S {K S} K
Remember, we want
B x y z = x { y z }
So, let's see:
S { K S } K x y z = K S x { K x } y z = S { K x } y z = K x z { y z } = x { y z }
C = S { B B S } { K K }
We want to have
C f x y = f y x
({C f y} is a notation for currying the second argument of f, just as {f x} curries the first.)
S { B B S } { K K } f x y = B B S f { K K f } x y = B { S f } { K K f } x y = S f { K K f x } y = f y { K K f x y } = f y { K x y } = f y x
T = C I
We want to have:
T x y = y x
Proof:
C I x y = I y x = y x
W = C S I
We want to have
W f x = f x x
Proof:
W f x = C S I f x = S f I x = f x { I x } = f x x
To prove: S { K a } I = a
S { K a } I x = K a x { I x } = a { I x } = x
To prove: S { K a } { K b } = K { a b }
S { K a } { K b } x = K a x { K b x } = a { K b x } = a b = K { a b } x
To prove: S { K a } = B a
S { K a } x y = K a y { x y } = a { x y } = B a x y
To prove: S a { K b } = C a b
S a { K b } x = a x { K b x } = a x b = C a b x