Thu Jun 26 12:18:20 CEST 2008

rewrite semantics

a remaining problem in my reasoning about rewrite semantics is this:

  * Manfred talks about giving Joy a semantics through rewrite
    rules. This REPLACES the stack semantics, but stack semantics is
    later re-introduced as a STRATEGY for implementing the rewrite

  * I talk about rewriting target programs. The definition of the
    function + can be written as

      [qw 1] [qw 2] +  -> [qw 3]

    This syntax represents the definition of a function which maps a
    target program of 2 instructions to one of 1 instruction. (Let's
    not use parameterized numeric values for simplicity.)

    But this is trivially changed into a system of purely syntactic
    rewrite rules like:

      [qw 1] [qw 2] [qw +] -> [qw 3]

What's the difference? They are really the same, no?

Extending the function system with functions that are
'self-compiling', i.e. :

       123 -> [qw 123]

and extending the rewriting system with a preprocessing step that maps
all syntax elements X to [qw X], we have two ways of interpreting:

      1 2 +

As functions, and inside the rewrite system.