[racket] [redex] Structured Semantics

On Thu, Jul 8, 2010 at 1:41 AM, Casey Klein
<clklein at eecs.northwestern.edu> wrote:
> 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)))))

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 <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://teammccarthy.org/jay

"The glory of God is Intelligence" - D&C 93