Re: [stack] S-K Construction of Dip?

> I may have found a counter-example:

The only problematic construction is "cat":

> cat = swap [i] cons swap cons

"[i] cons" is a no-op acting on one stack item:

   [A] [i] cons
== [[A] i]
== [A]

So that would make

   cat = swap swap cons == cons

which can't be right.

In any case, I confess it was a bit rash of me to make that claim (that "dip" cannot be constructed from {s,k}) without offering any substantial justification. So let's see if we can remedy that. 

To do this carefully, we need to make a recursive definition: Say that a concatenative expression "x1 x2 x3 ... xn" (where each term xi is either an atom or a quotation) is "dip-free" relative to a set of indeterminates {A, B, ...}  if the following property holds for each xi:

a) If xi is an atom, then for any j > i, xj must neither be, nor (in the case xj is a quotation) contain, any of the indeterminates {A, B, ...}.

b) If xi is a quotation, then its body must be dip-free.

I.e, an expression is dip-free if no indeterminates (whether quoted or not) occur to the right of any (dequoted) atom, and if the same holds for any (sub-)quotation.

So, for example, the following expressions are dip-free relative to {A, B}:

[B] [A]
[B] A []
[A] B s [k]
[[B] A] [A []] B [s] k

while the following are not:

A [B]
[B A]
k [A] [B]
[A] [k] [k] s [B] 

Now the key observation is that a dip-free expression remains dip-free when the reduction rules for "s" and "k" are applied

[C] [B] [A] s => [[C] B] [C] A
    [B] [A] k => A

(Although the converse is not true: it is possible for a non-dip-free expression to become dip-free after application of "k"'s rule, e.g., "A [B] [] k => A").

To see this, consider an arbitrary expression containing an "s" or "k" redex (i.e., an expression matching the left side of the reduction rule for "s" or "k"). For the moment, assume the redex occurs at the top level of the expression, i.e., not inside a quotation. So, in the case of "s", we have an expression

x1 x2 ... xn [q1] [q2] [q3] s z1 z2 ... zn

(where the xi's and zi's are atoms or quotations, while the qi's are arbitrary concatenative expressions), which we assume is dip-free, and which reduces to

x1 x2 ... xn [[q1] q2] [q1] q3 z1 z2 ... zn

which we verify is also dip-free, by carefully checking that each term satisfies the property in the definition: Each xi satisfies it, since (in the case xi is an atom) no new indeterminates have been introduced to the right of xi, and in the case xi is a quotation, its body remains unchanged and hence dip-free. It is satisfied for [[q1] q2] since q1 and q2, and hence "[q1] q2", are dip-free (Take a moment to check this most important step. It would break down if, for example, the quotation had been [q1 [q2]] or [q1 q2], since q1 might include an atom and q2 could contain an indeterminate). It is satisfied for [q1] since q1 is dip-free. Now, before looking at q3, notice that z1, z2, ..., zn do not contain any indeterminates, since they follow the atom "s" in the original expression. So then, for each term in q3, the property is satisfied since, if the term is an atom then it will contain no indeterminates after it since "q3" is dip-free and z1, z2, ..., zn contain no indeterminates, while if the term is a quotation, its body remains unchanged. Likewise, we easily verify that the property holds for z1, z2, ..., zn. A similar argument applies to "k". 

And now, suppose the redex occurs inside a quotation, so that we have an expression

x1 x2 ... xn [q] z1 z2 ... zn

assumed to be dip-free, reducing to

x1 x2 ... xn [q'] z1 z2 ... zn

Then q must be dip-free, so by the above argument (and applying induction on the depth of nested quotations in which the redex appears), q' must also be dip-free. So the property holds for [q']. And, the property holds for each xi and zi in the new expression, since for the atoms, no new indeterminates have been introduced to their right, while for the quotations, their bodies remains unchanged and hence dip-free.

That proves that the reduction rules for "s" and "k" preserve the dip-free property. So then, finally, suppose "x" were some concatenative expression over {s,k} constituting a construction "dip", so that we have a reduction

[B] [A] x ==> A [B]

This is impossible because the left side is dip-free relative to {A, B} but the right side is not, while the right-hand side is obtained from the left-hand side only applying the reduction rules for {s, k}, which we showed preserve the dip-free property. So we cannot construct "dip" from {s,k}. Therefore, we cannot construct "cat" from {s,k} either, since otherwise this would enable the construction of "dip" which you mentioned

  dip = swap unit cat i

Alternatively, we could prove directly that "cat" is inconstructible from {s,k} since "[B A]" is not dip-free relative to {A, B}.

So there we have it! It took some work, but considering the somewhat counterintuitive yet fundamental nature of the result, I think it was worth taking the time to address properly.

Does that clear things up?

- Brent

P.S., Manfred, 

Christopher and I are using "b" to refer to the following combinator:

[Z] [Y] [X] b == [[Z] Y] X

which is the concatenative version of the classical "B" combinator (as "s", "c", "w", "k", and "i" are the concatenative versions of the classical S, C, W, K, and I combinators), while your "b" is 

[Y] [X] b == Y X

I didn't notice you had already defined "b", so sorry about that; I wasn't intending to create a conflict in the notation.