`[<<][staapl][>>][..]`
Wed May 6 11:20:19 CEST 2009

## proof that [ a + b + ] == [ a b + + ]

```Funny, it's been a while since I did this kind of stuff.  But maybe
trying to do this unprepared will reveal some tricks.

To prove this, lets try to prove [ x a + b + ] == [ x a b + + ] first.

Note that a, b, x need to be values (self-quoting operators), not
generic operators (which might be non-invertible).

To prove this we relate the semantics of '+ in the concatenative code
to the semantics of '+ in a nested expression:

([qw a] [qw b] +) -> ([qw (+ a b)])

LHS:

x       [qw x]
a       [qw x] [qw a]
+       [qw (+ x a)]
b       [qw (+ x a)] [qw b]
+       [qw (+ (+ x a) b)]

RHS:

x       [qw x]
a       [qw x] [qw a]
b       [qw x] [qw a] [qw b]
+       [qw x] [qw (+ a b)]
+       [qw (+ x (+ a b))]

By unification we now need to prove

(+ (+ x a) b)  == (+ x (+ a b))

Wich is easier to see with infix notation:

(x + a) + b    == x + (a + b)

This is true by the associative property of '+

Generalizing this to all 'a we could attempt (*) derive the property

[ + b + ] == [ b + + ]

[ + (b +) ] == [ (b +) + ]

Then chopping off the last '+ gives

[ + b ] == [ b + ]

In general, this is only works in one direction:

[ + b ] ---> [ b + ]
[ b + ] -/-> [ + b ]

because the former replaces a strong typing constraint (need two input
values) with a weaker one (need one input value).

So (*) introducing variables to be able to prove relations makes
typing stricter.  This is a significant insight.

So, the associativity law in concatenative code looks like:

[ a b c + + ] == [ a b + c + ]

Equivalent and with a 2-value type constraint:

[ x + ] == [ + x ]

Associativity is commutation of variable quote and apply.  Actually
this is not so strange: associativity is about changing the order of
function application.

To write this without variable quote we get, typed with 3-value
arguments:

[ + + ] == [ >r + r> + ]

or with dip notation

[ + + ] == [ [ + ] dip + ]

The variable quote form is simpler: '+ commutes with single result
functions.

```
`[Reply][About]`
`[<<][staapl][>>][..]`