[stack] Concatenative operators as functions over stacks.

I've long been intrigued by Manfred's statement that Joy operators are
best described as functions from stacks to stacks and last night
decided to put pencil to paper and try to put that idea into some sort
of formal form -- both to aid my understanding of the implications of
this statement, and to see if something useful might emerge from the
effort. Here's a synopsis of what I've come up with so far:

A stack S is a sequence (ordered collection) of terms S = s0, s1, ...,
s(t-1), s(t) where only the most recently added term, s(t) is
available. (Note: "t" can be though of as standing for "top") Except
for the identity function, id : S --> S, all functions on S must begin
with some operation on s(t).

The function notation I use is
f : S --> S\modifications
which reads "function f is a mapping from stack S onto stack S
modified by whatever follows the backslash." So we can define push and
pop as:

push(x,S) : S --> S\t=t+1 s(t)=x
x = pop(S) : S --> S\x=s(t) t=t-1

Given any pair x,S where x is a term and S a stack, we can compute,

pop(push(x,S)) = pop(S\t=t+1 s(t)=x) = x,S\t=t+1-1 = x,S 

which is as expected.

So, here's the question -- can all required operations of a
concatenative language be defined in terms of these two primitive
stack operations and function composition?

To simplify the notation, we can get rid of the S (actually, make the
S implicit)
in the function definitions by push(x,S) = pushS(x) and pop(S) =
popS() and then
redefine them as push(x) and pop assuming there is only one stack
under  consideration.

The shuffle operators now become,

dup : S --> S\x=pop push(x) push(x)
swap : S --> S\x=pop y=pop push(x) push(y)
etc...

As Manfred points out, even concatenative literals behave as
functions. For any literal value v,
v : S --> S\push(v)

The arithmetic operators become,
add : S --> S\x=pop y=pop push(x+y)
etc...

Actually we can generalize arithmetic and relational operators as
binary operators,

binop(op) : S --> S\x=pop y=pop push(x op y) for op in
(+,-,*,/,mod,=,!=,...)

By adding additional notation for lists, sets, ..., this method seems
able to account for any concatentative operation. For example, if we
use the Haskell list notation [x|xs], then cons becomes,

cons : S --> S\x=pop [xs]=pop push([x|xs])

If we say that [Q] is a quoted program, we can define map as,

map : S --> S\[Q]=pop [y]=pop push([Q(y0) Q(y1) ... ])

The above seems to be the lambda calculus version of the situation as
it uses dummy variables. If variables are forbidden, the situation
becomes different quickly. If we try to write swap, for instance,
without dummy variables,

swap : S --> S\pop pop ? push push

we have an immediate problem -- how do we change the order of  the two
popped values? What replaces the question mark? Of course it is the C
combinator and now we're off down the combinator trail which Manfred
seems to prefer anyway.
If someone wants to take the time to produce a combinator version of
this notation, it would be a useful addition to our knowledge base, imho.

This is getting very long and I won't bore anyone with further details
but I'd like to know if anyone considers this a useful avenue for
further exploration. I'm thinking of writing a tiny interpreter using
only the methods given and hinted at here just to see how it goes and
what kind of program results.

One thing of interest is that the notation above lends itself to
direct compilation from a specification, if we remove the arrows and
just write

dup ::=  x=pop push(x) push(x)
etc...
--
Don Groves