[stack] Re: Flat concatenative basis (was: Concatenative macros?)

> I chose a different basis which results in shorter constructions for
> the primitives we're producing.

Wow! That's much better. Nice work.

> I think it's universally shorter;

Well, what exactly do you mean by that? There's certainly one 
combinator which is shorter in my {o,i}, namely "i". But there 
probably aren't too many more :-) Perhaps only finitely many. That 
would be an interesting question ...

> I still need to explore the effect of using cake instead of q. 

Well, I can show you that {[] [cake] [k], k} is incomplete (and the 
choice of total dequoter "k" is irrelevant to the following argument, 
as is the order of the 3 quotations in 0). It is impossible to 
construct cat. Why? Well, notice that in the right side of the 
rewrite rule for "cat", there is a quotation containing two non-
quoted terms:

[B] [A] cat == [B A]

But if we start with the stack "[B] [A]" and execute only a sequence 
of 0's and 1's (i.e., [] [cake] [k], or k), at each step the property 
will be preserved that each quotation contains at most one non-quoted 
term. This is because "cake" and "k" both preserve this property, as 
we can see from their rewrite rules:

[B] [A] cake == [[B] A] [A [B]]
[B] [A] k    == A

Assuming "A" and "B" each contain at most one non-quoted term (and 
that, if they contain quotations or subquotations, these also contain 
at most non-quoted term each), the same will hold for the right-hand-
side of both rewrite rules. So it is impossible to construct "cat".

Now, to be clear, I'm not claiming that "cat" is inconstructible in 
every basis expressed in terms of "cake" and "k". For example, let

0 = [] [cake] [k k]
1 = k

Then {0,1} is a complete flat basis (albeit a much uglier one than 
the one you've just given). Construct

zapk: 01  (i.e., zapk == zap k == x\ y\ z\ y )
== [] [cake] [k k] k
== [] k k
== zap k

cake: 001
== 0 01
== 0 zap k
== [] [cake] [k k] zap k
== [] [cake] k
== cake

zap: 000 cake zapk k zapk
== 00 [] [cake] [k k] cake zap k k zap k
== 00 [] [[cake] k k] [k k [cake]] zap k k zap k
== 00 [] [[cake] k k] k k zap k
== 00 [cake] k k k zap k
== 0 [] [cake] [k k] [cake] k k k zap k
== 0 [] [cake] cake k k zap k
== 0 [[] cake] k k zap k
== [] [cake] [k k] [[] cake] k k zap k
== [] [cake] [] cake k zap k
== [] [[cake]] [[cake]] k zap k
== [] [cake] zap k
== [] k
== zap

[]: 0 zap zap
== [] [cake] [k k] zap zap
== [] [cake] zap
== []

unit: [] cake zap
[A] [] cake zap
== [[A]] [[A]] zap
== [[A]]

nip: unit k (as in your construction)

[cake]: 0 zap nip
== [] [cake] [k k] zap nip
== [] [cake] nip
== [cake]

cons: cake zap
[B] [A] cake zap
== [[B] A] [A [B]] zap
== [[B] A]

dip: cake k
[B] [A] cake k
== [[B] A] [A [B]] k
== A [B]

swap: unit dip
[B] [A] unit dip
== [B] [[A]] dip
== [A] [B]

i: [] swap k
[A] [] swap k
== [] [A] k
== A

take: cake nip
[B] [A] cake nip
== [[B] A] [A [B]] nip
== [A [B]]

swat: [] swap take take [] swap 0 nip nip cons cons
[B] [A] [] swap take take [] swap 0 nip nip cons cons
== [B] [] [A] take take [] swap 0 nip nip cons cons
== [B] [A []] take [] swap 0 nip nip cons cons
== [A [] [B]] [] swap 0 nip nip cons cons
== [] [A [] [B]] 0 nip nip cons cons
== [] [A [] [B]] [] [cake] [k k] nip nip cons cons
== [] [A [] [B]] [] [k k] nip cons cons
== [] [A [] [B]] [k k] cons cons
== [] [[A [] [B]] k k] cons
== [[] [A [] [B]] k k]
== [A [] [B] k]
== [A B]

[k]: 0 nip cons [] swap cons
== [] [cake] [k k] nip cons [] swap cons
== [] [k k] cons [] swap cons
== [[] k k] [] swap cons
== [] [[] k k] cons
== [[] [] k k]
== [k]

We've constructed [], [cake], [k], "swat", "unit", and "i", so that 
implies completeness. (But note that we had to assume transparent 
quotation in the last two constructions). The reason the above 
argument does not apply here is that [k k], in the basis combinator 
0, is a quotation containing more than one non-quoted term; so the 
initial assumption of the argument is not satisfied.

> I also need to (just as an exercise) express 'dip' and 'swap' in 
this system.

If you still want the exercise, close this message now. I also wanted 
the exercise, so I'm going to spoil it below :-)










(lines intentionally left blank)











(lines intentionally left blank)












(lines intentionally left blank)












(lines intentionally left blank)












So, the (non-flat) construction for dip is

dip == unit [unit] swat i swat i

Putting things in terms of {q,k} (recalling that "swat i" == "q k") 
and flattening, we get:

dip == [] q zap [[] q zap] q k q k
== [] q zap [[] q [] k] q k q k
== [] q zap [k] [[] q []] swat q k q k
== [] q zap [k] [[]] [[] q] swat swat q k q k
== [] q zap [k] [[]] [q] [[]] swat swat swat q k q k
== [] q zap [k] [] unit [q] [] unit swat swat swat q k q k
== 00101 0011 01 0001010011011001010011011 00101 00101001101 
001001010011011 00101 00101001101 0011001010011011 0011001010011011 
0011001010011011 0011 1 0011 1
== 
0010100110100010100110110010100110110010100101001101001001010011011001
0100101001101001100101001101100110010100110110011001010011011001110011
1 (141 bits)

Then, the easiest way to get swap is via the construction

swap == unit dip

Of course, if you could construct swap first some other way, then you 
could use the construction

dip == swap unit cat i
    == swap unit swap swat i
    == swap unit swap q k

to get dip; but I doubt that this is helpful, because "swap" is 
probably more complicated to construct than "dip". At least, in the 
non-flat case, the minimal construction of "swap" in terms of {q,k}, 
according to a computer search (at least, according to my memory -- I 
seem to have accidentally overwritten the log file, and this one took 
quite a while to run), is

[] q [] k [] q [] k [[] q [] k] q k q k

which is just the minimal construction of "unit" concatenated with 
the minimal construction of "dip", so that "unit dip" really is the 
minimal way to construct swap in this situation. Of course, it's 
certainly possible that this could change when we switch to the flat 
basis {0,1}.

By the way, I said "the minimal", but there were actually some other 
solutions of equal size; I didn't take the time to look at them all, 
but they mostly seemed to be trivial varients based on the equivalence

[A] k == [] k A

(which, in fact, could be useful to help flatten out expressions over 
{q,k} without introducing as many "swat"'s).

> > - Brent
> 
> -Billy
>

- Brent