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

> Let me first say that recasting combinatorial operations in terms of a
> flat concatenative language has made it MUCH easier for me to reason
> about them. I definitely don't understand them completely, but somehow
> the reasoning seems more in line with my brain's workings. One of my
> friends felt the same way. Am I just mentally disturbed from years of
> Forth use and abuse, or is there actually something simpler here?

Well, although building flat bases (e.g., {o, k}) has been great fun, to me it seems like this system is only simpler in a fairly artificial way. This is because the system, in a sense, is not flat at all. True, we can express programs using flat syntax; but, once these programs start executing, they start building programs on the stack that aren't flat. So the system has to deal with non-flat programs in the course of execution anyway. And to do anything non-trivial the programmer needs non-flat programs, only he isn't allowed to express them directly, but rather is forced to construct them in a flat manner, with his hands tied behind his back, so to speak.

So, we ask, is it possible to modify our approach to give us a more "genuine" flat system? Well, to really be flat, we would have to not be able to push programs onto the stack, since that's the first level of non-flatness. And if we can't do that, that leaves literally nothing left that we can do, assuming we've started with just the concatenative combinators, where programs are the only type of data. So, a "genuine" flat system would have to be quite different. Special support would be needed for loops and conditionals, since these could no longer be implemented with the (rather meager) remaining set of combinators (which could only shuffle the stack, not perform restructuring or execution).

I don't know. The way I see it, non-flatness is roughly equivalent to the ability to do higher-order programming, which is a good property of a system. It seems to be a fundamental part of the Joy programming paradigm. And for that matter, any programming language that supports loops and conditionals is going to be (conceptually) non-flat in the sense that programs have structure; we think of them as being divided into pieces, subpieces, etc. The syntax may or may not reflect this; but if it doesn't, I would say it's just because it's been artificially obscured. 

But, if you can show me a really nice flat programming language, you may be able to change my mind :-)

> I find it interesting that completeness is different between
> applicative and concatenative languages (for example, {s,k} is a
> complete applicative basis, but not is not complete when
> concatenative).

Right. When we map the applicative combinators to concatenative ones in the obvious way, the image of this map is not a complete (concatenative) set. But it's interesting to note that, in the other direction, things turn out differently. I.e., the image of the natural map (or at least, what I'm calling the natural map) from concatenative combinators to applicative ones _is_, remarkably enough, a complete applicative set. Here's the map I'm talking about: Call the map P, defined recursively as follows:

P(id)   = \c.c
P(x)    = \c.xc
P(f g)  = \c.F(Gc)
P([f])  = \c.cF
P(x\ f) = \cx.Fc

where "f" and "g" are arbitrary concatenative expressions, F is P(f), G is P(g), "x" is any variable, and "c" is some variable distinct from "x" and which does not occur in "f" or "g". Actually, to make P well-defined as a map from concatenative lambda-forms to applicative lambda-forms (not merely over the equivalence classes of such forms), we need to restrict "f" (or, alternatively, "g") to be either a variable or a quotation (but not a concatenation) in order to force a unique parsing of the concatenative expression. This is a technical detail which may or may not be important to us, depending on what we're trying to do with the map.

It would take some work (which I'll skip, for now) to show that this map respects the reduction rules of the two systems (i.e., that f reduces to g if and only if P(f) reduces to P(g)). 

Anyhow, although the map may at first appear strange and complicated, it really isn't so bad. Essentially, it maps any concatenative program to a function whose first parameter is treated as a continuation (hence the name "c"); an additional parameter is taken (in curried fashion, of course) for each input stack item, top item first; the body of the function is an application of the continuation to each output stack item. Note that although concatenation maps to function composition (a nifty property), we aren't exactly modelling concatenative programs as functions from a stack to a stack (if we were, concatenation would actually need to map to _reverse_ composition). It's possible to construct a map which does precisely that, but it's considerably more complicated and not as natural, in my opinion.

Anyhow, here are what some standard Joy combinators map to by P (Exercise: verify these):

P(id)   = \c.c == I
P(i)    = \cx.xc == T
P(dup)  = \cx.cxx == W
P(zap)  = \cx.c == K
P(cons) = \cxy.c(\d.ydx) == \cxy.c(Cyx)
P(cat)  = \cxy.c(\d.x(yd)) == \cxy.c(Bxy)
P(dip)  = \cxy.x(cy) == CB

where I, B, C, W, and K are the following standard applicative combinators:

Ix   == x
Bfgx == f(gx)
Cfxy == fyx
Wfx  == fxx
Kxy  == x

Now, it is well-known that {I, B, C, W, K} form a complete applicative basis. So far, we have I, W, and K, so we only need to show that we can construct B and C.

Well, B comes easily: Just apply I to P(cat) (let's define Cat = P(cat)). We get

Cat I 
== (\cxy.c(Bxy)) I
== \xy.I(Bxy)
== \xy.Bxy
== B

Now, we can almost get C by applying I to P(cons) (defining Cons = P(cons)):

Cons I
== (\cxy.c(Cyx)) I
== \xy.I(Cyx)
== \xy.Cyx
== CC

This is just a varient of C that takes its first two parameters in reverse order. And there is a construction of C from this combinator (which I found by computer search, although it's quite simple):

C = CC(CC)(CC)

The verification:

CC(CC)(CC)fxy
== C(CC)(CC)fxy
== CCf(CC)xy
== C(CC)fxy
== CCxfy
== Cfxy

So there we have it! The image of P is a complete applicative set! What is perhaps even more surprising is that we didn't need to use the image of "i" or "dip". So the image under P of the _incomplete_ set {id, dup, zap, cons, cat} is a complete applicative set. This set, {id, dup, zap, cons, cat}, is not only incomplete, it's really severely incomplete. These are proper combinators, none of which performs any reordering on its parameters; therefore it is impossible to construct "dip", or even "swap", from them. Moreover, none of them perform dequotation, so it is not even possible to construct "i" from them.

In any case, note that I'm not claiming P is surjective (i.e., that it maps onto to every applicative combinator), only that it maps onto a complete subset of the applicative combinators. If P (or rather, the version of P which operates on equivalence classes of lambda-forms rather than the forms themselves -- call it P^, "P-hat") is surjective, then it would be an isomorphism between the concatenative and applicative systems of combinators (the well-definedness and injectivity of P^ follow from the fact that P respects reduction). I doubt that such an isomorphism exists but don't know how to prove this. This is really the fundamental question about the relationship between concatenative and applicative combinators: are the two systems isomorphic? 

Well, actually, this is two questions, since there are two main versions of both systems, namely one with the "principle of extensionality" (i.e., one with an "eta-reduction" rule, ensuring "[] dip == id" in the concatenative system, and "BI == I" in the applicative), and one without. The map P above is designed to work either way (although the two systems must either both have, or both not have, eta-reduction). The part to be careful with is

P(x) = \c.xc

in the definition of P. If we have eta-reduction, we can replace this with

P(x) = x

However, if we don't have eta-reduction, this change will break the essential property of P, i.e., that it respects reduction. For then we would have

P([x] y\ y)
=  \c.(\d.dx)((\ey.ye)c))
=> \c.(\d.dx)(\y.yc)
=> \c.(\y.yc)x
=> \c.xc

P(x) = x

where 

  [x] y\ y => x

but not
  
 P([x] y\ y) => P(x)

since without eta-reduction, \c.xc does not reduce to x. So P, in this case, would not respect reduction. For this argument, I'm using a special case of the Church-Rosser property, that an (applicative) combinator has a unique normal form (i.e., a form with no redexes) if it has one at all. (The general case states that if A, B, and C are lambda-forms with A=>B and A=>C, then there is a form D such that B=>D and C=>D. This essentially says that if you can get a form to reduce to two different forms (by choosing different redexes to reduce), you can perform further reduction to converge again to a common form. This an intuitive idea which is nevertheless highly non-trivial to prove). Although I'm not relying on it here, it would also be nice to know if an analogous "Church-Rosser" property holds for concatenative combinators.

> [B] [A] cake == [[B] A] [A [B]]
>
> Clearly, A and B are not siblings here. Of course, constructing concat
> is possible, which obviously makes siblings out of A and B, but is it
> somehow less theoretically pure to have a basis in which the siblings
> are not explicit in the provided basis combinators? 

Well, the construction of "cat" in terms of {cake,k} relies on transparent quotation; ultimately, it's the same construction as this one from i, dip, and cons:

  cat == [[i] dip i] cons cons

which works like so:

[B] [A] [[i] dip i] cons cons
== [B] [[A] [i] dip i] cons
== [[B] [A] [i] dip i]
== [[B] i [A] i]
== [B A]

To construct "cat" from {cake,k}, transparent quotation is fundamentally necessary. For, if we assume opaque quotation and consider reducing the expression

  [B] [A] x

where "x" is a combination over {cake,k}, we see that each reduction step preserves the property that no quotation contains (in the shallow sense) more than one (dequoted) indeterminate, so that we can never reach [B A]. Therefore, "cat" is inconstructible in {cake,k} under opaque quotation. So, {cake,k} is not complete in as strong a sense as, for example, {q,k} (from which all combinators are constructible, even assuming opaque quotation):

  [B] [A] q == [[B]] [A B]
  [B] [A] k == A

In addition, I'd say "q" is a bit nicer than "cake" since, aside from being simpler, it has the pretty property that it produces a (unit) quotation and a concatenation, which correspond precisely to the two syntactic constructions of the language. This may not be particularly significant in the grand scheme of things, but we have to admit that it's a bit nifty. So I'm perfectly fine with "condemning {cake,k} to contempt and contumely" :-)

> -William (Billy)

- Brent