On Thu, Jul 8, 2010 at 1:41 AM, Casey Klein <clkl...@eecs.northwestern.edu> wrote: > 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)))))
Yes I think that is the right thing. (Although with ->_thread in the where, which I think you meant.) Thanks for pointing out the obvious for me. =) Jay > >> 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. > -- 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
