[<<][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][>>][..]