I'm just searching a way to format it so that it is
more readable in the archive.
I will provide a detailed solution of the last problem
for those who have perhaps missed the beginning.
Verify that S = B(BW)(BBC). That is
verify that B(BW)(BBC)xyz = xz(yz)
This should be much easier.
One awful solution would be, reminding that
B = S(KS)K, and that W = SS(KI)
and that C = S(BBS)(KK), that is
S((S(KS)K)(S(KS)K)S)(KK), to substitute
those the occurence of B, W and C by they
S = B(BW)(BBC) =
... and then applying that _expression_ on xyz.
Obviously we have not programmed the elementary
compositor B, the elementary permutator C and the
elementary duplicator W for not using them. Yet this
gave an interesting definition of S in term of itself and
this rises the question if there is not some general
recursion phenomenon there and indeed there will be
a very general such phenomenon captured by a
combinator which is neither an eliminator, nor a
permutator, nor a duplicator, nor even an identificator
(like Ix = x) and which was called the paradoxical
combinators by Curry and Feys and is known today
as the fixed point combinator but that's for later.
So I recall:
Bxyz = x(yz)
Wxy = xyy
Cxyz = xzy
Kxy = x
Sxyz = xz(yz)
And let us verify that S = B(BW)(BBC)
I recall "=" means "act similarly"; thus we must
B(BW)(BBC)xyz = Sxyz = xz(yz)
Well Bxyz = x(yz) and please remember that
Bxyz abbreviates (((B x) y) z) and in particular
B(BW)(BBC)x abbreviates (((B (BW)) (BBC)) x)
and that that matches!
Another practical way (more practical than
by adding the left parenthesis!) is to fully
abbreviate the _expression_ (like I do usually) and
remember that B (here) is trigged by its dynamic
when presented with three arguments and that
argument are *arbitrary* combinators:
so the _expression_ B(BW)(BBC)xyz is
B (BW) (BBC) x y z
1 2 3
and you can write the dynamic of B by B123 = 1(23), meaning
that 1 denotes its first argument (BW), 2 its second (BBC) and
3 denotes x, so that
B(BW)(BBC)x gives (BW)((BBC)x) that is (fully abbreviated)
BW(BBCx). We must yet apply it to y and then z:
Oh! here we have a choice! Indeed
the B-dynamic match the first occurrence
of B and the second one. A famous result,
known as Church Rosser Theorem tells
us that as far as thereduction will converge
on some stable molecule, the path, and
thus those choice does not matter: we will
get the same stable molecule. Soon or
later we will come back on this, but let us
just choose the leftmost reduction (another
theorem will make some advertising for that
strategy, but things will appear to be non
trivial though ...). So we apply the B-rule
on leftmost B in: B W (BBCx) y giving
W((BBCx)y) that is (fully abbrev.)
W(BBCxy), and now we have also a
choice: either we apply W(BBCxy)
directly on z, or we reduce it further.
You could verify those alternate path
as exercise; let us apply W(BBCxy)
directly on z. This gives W(BBCxy)z
(and Wab = abb) thus W(BBCxy)z gives
(BBCxy)zz = (fully abbrev.) BBCxyzz,
and this gives by the B-rule B123 = 1(23),
(where 1, the first argument of B
is B itself, and 2 is C and 3 is x)
B(Cx)yzz which by the B
rule again (with 1 = (Cx), 2 = y, 3 = z)
gives (Cx)(yz)z, which by the C-rule C123= 132
(with 1 = x, 2 = (yz) 3 = z gives xz(yz). That's Sxyz
and so we have shown that
B(BW)(BBC) behaves like S.
To sum up: S = B(BW)(BBC) because
= xz(yz) which what Sxyz gives.
Of course the original exercise I gave was harder: program
S from B, W and C. It consisted in finding that B(BW)(BBC) or
something similar. But how could we have found such _expression_?
A nice thing is that the verification above, which just use the
dynamics of B, C and W gives us the answer: just copy the
execution above in the reverse order (cf programming here is
inverse execution). I do it and I comment:
?xyz = < B, C, ...>xyz = xz(yz)
xz(yz) so this is what we want as the
result of B C W application
on xyz. So we must transform
xz(yz) as <B,C ..>xyz, that is
get those final "x)y)z)", or
xyz in fully abb. form.
Cx(yz)z what a clever move! we are
at once close to xyz, except
that we have two parentheses
too much, and one z to much.
To suppress one z we will
isolate it by moving the right
parenthesis to the left. That's
the inversion of the B-rule, so
we arrive at:
B(Cx)yzz and applying again the
B-rule, we get
(BBCxy)zz I let some left parenthesis
so that the W-rule
applicability is highlightened
W(BBCxy)z And now there just
remains a right parenthesis
we would like to push on the
left, which we can do by
two successive inverse B rule:
The first gives (with 1 = W, 2
= (BBCx) and 3 = y:
BW(BBCx)yz the second gives
with 1 = (BW), 2 = (BBC)
and 3 = x:
B(BW)(BBC)xyz we got what we wanted:
S = B(BW)(BBC). Both gives xz(yz) when
given x y and z (in that order!).
Question: is there a systematic method such
that giving any behavior like
Xxyztuv = x(yx)(uvut) <or what you want)
can generate systematically a corresponding
SK or BWCK -combinator?
The answer is yes. I let you meditate the question.
(This point will be made clear when we will meet
the terrible little cousins of the combinators
which are the *lambda _expression_*, (and which
in our context will just abbreviate complex
combinators), but I propose to progress
and make sure that the
SK combinator are Turing Universal.
I am not yet decided when I really should
introduce you to the paradoxical combinators,
which are rather crazy. Smullyan call
them wise birds, but I guess
it is an euphemism!
Mmhhh... Showing turing-universality
through the use of some paradoxical
combinator is easy (once we have defined
the numbers), but there is a risk you take
bad habits! Actually we don't need the
paradoxical combinators to prove the turing
universality of the SK forest, mmmmh...
Well actually I will be rather buzy so I give
you the definition of a paradoxical combinator
and I let you search one.
First show that for any combinator A there
is a combinator B such that AB = B.
B is called a fixed point of A. (like the center
of a wheel C is a fixed point of the rotations of
the wheel: RC = C). It is a bit amazing that
all combinators have a fixed point and that is
what I propose you try to show. Here are hints for
different arguments. 1) Show how to find a fixed
point of A (Arbitrary combinator) using just B, M
and A. (Mx = xx I recall). 2) The same using just the
Lark L (Lxy = x(yy) I recall).
Now, a paradoxical combinator Y is just a
combinator which applied on that A will give the
fixed point of A; that is YA will give a B such that
AB = B, that is A(YA) gives YA, or more generally
Y is a combinator satisfying Yx = x(Yx).
COMBINATORS I is
COMBINATORS II is
COMBINATORS III is
COMBINATORS IV is
COMBINATORS V is
Kxy = x
Sxyz = xz(yz)