Two-combinator base !
Brent L Kerby — 2002-04-04 21:52:25
Yep, there is a complete two-combinator Joy base, namely {z, k} where
[D] [C] [B] [A] z == [[D] C] A [D] B
[B] [A] k == A
I don't plan to permanently reserve the name "z" for this combinator, seeing as
it is so weird :-)
Essentially, "z" is a modified "s" combinator, where
[C] [B] [A] s == [[C] B] [C] A
In fact, "s" can be constructed simply as
s == [] z
This was a main point in the design of "z". Because, having "s" and "k" allows
us to construct a huge amount of combinators; in fact it allows us to construct
all applicative combinators. I should define "applicative combinator" formally,
but instead, I'll just say that we can construct, for example, all these fun
combinators, "i", "b", "c", "w":
[A] i == A
[C] [B] [A] b == [[C] B] A
[C] [B] [A] c == [B] [C] A
[B] [A] w == [B] [B] A
These are constructed the classic way from applicative combinatory logic (I
should give more detail on this ...):
i == [][k]s
b == [k][[s]k]s
c == [[k]k][[s][b]b]s
w == [[i]k][s]s
Having "b", "c", "w", and "k" gives us the ability to construct "cons", "swap",
"dup", and "zap":
cons == [] b == [[]k]s
swap == [] c == [k][[[]s]k]s
dup == [] w == [i][]s
zap == [] k
To be on the safe side, I'll verify these by hand for you:
(first, here's cons:)
[B] [A] [[] k] s
== [[B] A] [B] [] k (by s)
== [[B] A] (by k)
(now, swap:)
[B] [A] [k] [[[] s] k] s
== [B] [[A] k] [A] [[] s] k (by s)
== [B] [[A] k] [] s (by k)
== [[B] [A] k] [B] (by s)
== [A] [B]
(now, dup:)
[A] [i] [] s
== [[A] i] [A] (by s)
== [A] [A] (by i)
Obviously, these constructions (particularly, of swap and dup) rely on the
transparency of quotation; but this is quite acceptable, I think.
Anyway, this gives us "i", "cons", "dup", and "zap". All we're lacking for
completeness now is "dip". And this is where the fun comes in! :-)
To get "dip", we have to use "z", because "dip" is not constructible from just
"s" and "k". Fortunately, "z" is specially designed to allow us to get "dip" out
of it.
dip == [] swap [] swap [k] cons z
It works like this:
[B] [A] [] swap [] swap [k] cons z
== [B] [] [A] [] swap [k] cons z (by swap)
== [B] [] [] [A] [k] cons z (by swap)
== [B] [] [] [[A] k] z (by cons)
== [[B]] [A] k [B] (by z)
== A [B] (by k)
Or, I'll give you the brute-searcher's construction of dip in terms of just "z"
and "k" (I was surprised to find that a construction even as simple as this
exists):
dip == [k] [[] [[]]] [] z z z
Here's how it works: ( :-) )
[B] [A] [k] [[] [[]]] [] z z z
== [B] [[A] k] [A] [] [[]] z z (by z)
== [B] [[[A] k] A] [] [[A] k] z (by z)
== [[B] [[A] k] A] [A] k [B] (by z)
== A [B] (by k)
To summarize, here are the constructions "i", "cons", "dip", "dup", and "zap" in
terms of just "z" and "k"
i == [] [k] [] z
cons == [[] k] [] z
dip == [k] [[] [[]]] [] z z z
dup == [[] [k] [] z] [] [] z
zap == [] k
Just for fun, here's "sip", too (as found by the searcher):
sip == [k] [] [[] [[]] z k] z
Here's how it works:
[B] [A] [k] [] [[] [[]] z k] z
== [B] [[A] k] [] [[]] z k [A] (by z)
== [[B] [A] k] [] [B] k [A] (by z)
== [A] [] [B] k [A] (by k)
== [A] B [A] (by k)
Wow, isn't this interesting!
Now, the question is: is there a simpler two-combinator base? (maybe a base in
which the combinators take at most three parameters, or maybe only two).
A word of warning to those who might be trying to use my searcher ... it has a
little bug somewhere that I can't explain. It causes the program to be
unsuccessful in many cases at finding constructions of "cons", or combinators
similar to it, even when a simple construction is right there.
(all these results really do need to go into an article, as Manfred suggested; I
think I'm about ready to start on it, for real, especially now that this
particular question, about the existence of a two-combinator base, is solved)
- Brent