[<<][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 + + ]
which should be read as
[ + (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][>>][..]