Combinatory Completeness in Joy

[iepos@tunes.org]

I've been thinking a bit about the basic primitives of Joy,
and thought I'd share a few results... (this doesn't
exactly apply to Joy directly, but to a modified Joy, in which
the quotation construct is non-opaque)

A while back we discussed how it is possible from
the four primitives "swap", "dup", "pop", and "dip" to form
all stack-manipulators of a certain kind... among those that
could be formed:

  xyz--zyx
  xyz--zxy
  xy--yx    (swap)
  x--xx     (dup)
  x--       (pop)
  x--x      (id)

These kinds of combinators I will call the "regular combinators"
of Joy (because they correspond to the regular combinators of
applicative systems); unlike "dip", "cons", and "concat", 
regular combinators do not have any quoting or unquoting effects.

Anyway, irregular combinators are quite important too, and should
not be neglected... As yet, I haven't said much about them, or
how they can be constructed from one another. It turns out
that the above four combinators, along with "i" and "cons", are enough
to form all combinators (regular and irregular); moreover,
"swap" is not necessary, as it can be constructed from the others as

  [] cons dip
 
All right, now to show how it is that "dup", "pop", "dip", "cons", and "i"
form a complete base... first of all, I need to clarify on the kind
of completeness I'm talking about... to do this, I have to introduce
the analogue of the Lambda construct (this was alluded to before,
several posts ago); I'll do this with an example:

  x\ 9 x x * -

This is the lambda way of writing a program that squares a number
and subtracts it from 9. One way of thinking of it is that "x\"
is a program that pops a value off the stack and binds to "x"
a program that pushes it back. Anyway, the example could be
written without the lambda by instead using the "dip" and "dup"
combinators:

  [9] dip dup * -

But, conversely, the "dip" and "dup" combinators may be written
using lambdas:

  dup:  x\ x x
  dip:  f\ x\ f i x

Note that "i" was still needed in the lambda construction of
"dip" ("i" is the only such combinator that is needed though, if
for some reason one really wants to go all the way with
the lambda approach). Here how some other combinators can be
written using lambdas:

  swap:   x\ y\ x y
  pop:    x\
  cons:   f\ x\ [x f i]
  concat: f\ g\ [g i f i]

Note the parameters are taken in the reverse order from your "--",
in that swap is written as "x\ y\ x y" instead of "x\ y\ y x"...
The natural order to use the parameters is in the reverse order
that they were pushed, and "swap" uses the parameters in an
unnatural order (the same order in which they were pushed).

Anyway, this whole thing illustrates that lambda-like things are
not a characteristic of just applicative systems; they can be
used naturally in concatenative systems too (but, they can also be
eliminated in both applicative systems and concatenative systems).

By the way, if one were going to use lambdas in a real concatenative
system, a scoping mechanism would need to be provided, so that
one could write something like this, using parentheses:

  (x\y\ x y div x y mod) (x\y\ x square y square +)

This would be a program that takes two numbers off the stack,
calculates their quotient and remainder, then takes those two
results, squares each, and finally yields their sum. Of course,
in this case, the explicit scoping is not strictly necessary...
Different letters could have just been used in the second case
(or the same letters might could have been used actually, if the
system permits overriding of scopes, under the rule that the
innermost takes precedence).

By the way, in case it is not clear, this kind of thing would
not be legal with the lexical kind of lambda construct I am
speaking of:

  foo == x\
  myprog == 3 foo x x *

It some strange system this might work, with "myprog" yielding "9";
but, in the type of system I'm talking about, this would not work,
because the two "x"s referred to in "myprog" are not bound; "foo"
only had the effect of popping off the top item on the stack...
the "x" cannot be used outside of "foo".

Anyway, you are probably thinking now that lambdas are just annoying
and that I need to get back to my main point, the completeness
of the base {dup, pop, cons, dip, i}. I needed to bring
in lambdas so I could clarify on the kind of completeness I'm
talking about... In saying that this base is complete, I mean this:

  The combinators in the base are sufficient to eliminate all
  lambdas. Moreover, all combinators can be formed (using
  concatenation and quotation) from the combinators in the base.

The second statement is almost a direct consequence of the first;
if all combinators can be written using just lambdas, then it
would be... but, some combinators also require use of "i" when
being written in lambda form; anyhow, the base explicitly contains
"i", so in this case the second statement will follow from
the first...

Now, it is finally time to show how it is that {dup, pop, cons, dip, i}
can be used to eliminate lambdas... before detailing the algorithm,
I'll give an illustration of how it is used on this program:

  x\ y\ x y div x y mod

To begin, we focus only on the innermost lambda (as if the "x\" was
not even there):

  x\ y\ x y div x y mod
  x\ [x] dip y\ y div x y mod
  x\ [x] dip dup y\ div x y mod
  x\ [x] dip dup [div x] dip y\ y mod
  x\ [x] dip dup [div x] dip y\ y mod
  x\ [x] dip dup [div x] dip mod

Now, the inner lambda is gone... we gradually pushed it further
and further to the right using "dip" and "dup". Now, to eliminate
the remaining lambda:

  x\ [x] dip dup [div x] dip mod
  dup [x\ x] cons x\ dip dup [div x] dip mod
  dup [] cons x\ dip dup [div x] dip mod
  dup [] cons [dip dup] dip x\ [div x] dip mod
  dup [] cons [dip dup] dip [x\ div x] cons dip mod
  dup [] cons [dip dup] dip [[div] dip x\ x] cons dip mod
  dup [] cons [dip dup] dip [[div] dip] cons dip mod

I don't know... maybe this isn't a really good algorithm;
here is how I would actually write the original program:

  dup2 [div] dip2 mod

or even more likely:

  [div] sip2 mod

where "sip2" is a combinator I made up, a generalization of a "sip"
which I think may actually be of great significance:

  sip == x\y\ y x i y == dupd dip

It is closely related to the "S" of applicative systems... 
it executes a program, but saves a copy of the first stack item
first, which is restored after the program is finished. It is
like "dip", except that the executed program gets a copy of
the top stack item too.

Anyway, here is how I spell out the algorithm used above...
Here are the rules; the first one that applies must be used:
(where "F" and "G" stand for arbitrary expressions and 
 where "C" stands for an arbitrary expression not involving "x"):

  x\ C    =>  pop C
  x\ x    =>
  
  x\ C F  =>  [C] dip x\ F
  x\ F C  =>  (x\ F) C
  x\ F G  =>  dup [x\ F] dip x\ G

  x\ [F]  =>  [x\F] cons

It is obviously correct and also clearly yields very compact
results... The second to last rule could be alternatively modified to

  x\ F G  =>  [x\ F] sip x\ G

"sip" is a very fun combinator. It along with "pop", "cons", and "i" forms
a complete base. It eliminates the strict need for "dip" and "dup" in the
algorithm, in rule "x\ F G"... The rule "x\ C F" (which used "dip")
is not essential (and wasn't to begin with, actually, although it did,
and still would, help give more compact results). 

For curiousity, here are some other constructions using "sip"
(as determined by the algorithm):

  dup    == [] sip
  dip    == [[pop pop] sip i] cons sip
  swap   == [[pop pop] sip] cons sip
  concat == [[pop i] sip i] cons cons

The first one might be useful, but I probably wouldn't use the
last three in a real system because of the unnecessary duplications;
"swap" and "concat" can be much more elegantly defined if "dip" is
available too:

  swap   == [] cons dip
  concat == [[i] dip i] cons cons

Well... that's enough for now...

As you can see, abstraction algorithms of this kind are useful
for demonstrating the completeness of bases. I think they may
also be useful for other purposes, for instance the purpose
of finding a complete set of Combinatory Axioms... But that
is the topic of another (future) post...

Oh, and by the way, the abstraction algorithm given is of the
"eta-strong" style; it could be modified to be of the beta-strong
style; the rules would be modified to:

  x\ C    =>  pop C
  x\ x    =>  [] dip
  
  x\ C x  =>  [C] dip
  x\ C F  =>  [C] dip x\ F

  x\ F C  =>  (x\ F) C

  x\ F x  =>  [x\ F] sip
  x\ x F  =>  []     sip x\ G
  x\ F G  =>  [x\ F] sip x\ G

  x\ [x]  =>  [] cons
  x\ [F]  =>  [x\F] cons

Okay, this is the end now...

- "iepos" (Brent Kerby)