[racket] [redex] Structured Semantics

This isn't truly a structured semantics, though yes it comes close. 

Do we show the GC rules in the Redex book? It would do the same. 

-- Matthias




On Jul 7, 2010, at 11:53 PM, Jay McCarthy 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. 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.
> 
> 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?
> 
> Jay
> 
> -- 
> Jay McCarthy <jay at cs.byu.edu>
> Assistant Professor / Brigham Young University
> http://teammccarthy.org/jay
> 
> "The glory of God is Intelligence" - D&C 93
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/users