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 <j...@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
