On Wed, Jul 7, 2010 at 10:53 PM, Jay McCarthy <jay.mccar...@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.
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
