[racket] [redex] Structured Semantics

On Wed, Jul 7, 2010 at 10:53 PM, Jay McCarthy <jay.mccarthy at gmail.com> wrote:
> How should I use Redex to encode a structured semantics... For example,
>
> Suppose I have the L_thread language and the ->_thread reduction
> relation with contract
>
> (store_global store_local term) ->_thread (store_global store_local term)
>
> and I want to have another language L_system with an ->_system rr with contract
>
> (store_global (store_local term) ...) ->_system (store_global
> (store_local term) ...)
>
> where (among other rules) I have the rule:
>
> (store_global store_local term) ->_thread (store_global' store_local' term')
> ---------------------
> (store_global (store_local term) any_others ...) ->_system
> (store_global' (store_local' term') any_others ...)
>
> I could easily use reduction-relation for ->_thread and most of
> ->_system, but for this particular rule, it doesn't seem possible to
> express in Redex.

Would something like this work? I've taken the liberty of assuming any
thread can move (but maybe you have a separate ->_system rule that
moves a thread to the front).

(--> (store_global (store_local_0 term_0) ...
                   (store_local_i term_i)
                   (store_local_i term_i+1) ...)
     (store_global’ (store_local_0 term_0) ...
                    (store_local_i’ term_i’)
                    (store_local_i term_i+1) ...)
     (where (any_0 ...
             (store_global’ store_local_i’ term_i’)
             any_j+1 ...) ; any one of the thread reducts
            ,(apply-reduction-relation
              ->_system
              (term (store_global store_local_i term_i)))))

> If the reduction-relation? structure were exposed
> (or perhaps had a struct property associated with it), then I could
> code this one rule in Racket and dispatch to the two other rrs when
> necessary, but that seems wrong.

I'm not sure which additional operations you're imaging on
reduction-relation structures.

> Another way I could do it is combine the two languages and rules into
> one with a "mode" switching...
>
> L_synthetic = (THREAD L_thread L_system/thread-hole) + (SYSTEM L_system)
>
> ->_synthetic =
>
> (THREAD thread sys) -> (THREAD thread' sys)
>
> ...
>
> (SYSTEM (in-hole sys thread)) -> (THREAD thread sys)
>
> But that seems like the wrong thing too.
>
> Any other ideas or examples?
>

Overall, I think we need to consider better supporting this style in Redex.