(thunk TT) isn't a TT, tho? It will reduce only in a TT. Robby
On Fri, May 3, 2019 at 7:16 PM William J. Bowman <[email protected]> wrote: > > That looks like the contexts I want, but it doesn't seem to reduce under a > (thunk TT) in my example model. > > -- > Sent from my phoneamajig > > > On May 3, 2019, at 20:02, Robby Findler <[email protected]> wrote: > > > > Redex, when asked to create the compatible closure, creates a context > > and then uses that. In this case, it will create a context something > > like this: > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > > VT ::= (thunk TT) > > > > If you want something else (I'm not sure of an algorithm to handle > > this kind of thing without coming with something like that), it might > > be simplest to write out the contexts that you want directly and use > > context-closure. > > > > Robby > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman <[email protected]> > >> wrote: > >> > >> Hello all, > >> > >> I'm trying to define a model in Redex where values and terms are separate > >> nonterminals, and then define a reduction relation using > >> `compatible-closure` > >> to lift the small steps to the, well, compatible closure. > >> Unfortunately, it doesn't do what I expect, presumably because the > >> nonterminals > >> for values and terms are mutually defined, but `compatible-closure` takes > >> exactly one nonterminal. > >> > >> Is there a way to do what I want? > >> See attached. > >> > >> -- > >> William J. Bowman > >> > >> -- > >> You received this message because you are subscribed to the Google Groups > >> "Racket Users" group. > >> To unsubscribe from this group and stop receiving emails from it, send an > >> email to [email protected]. > >> For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
