I just kind of made up the algorithm for what Redex does. It seems to coincide with what one expects for some cases at least. :)
Robby On Fri, May 3, 2019 at 9:09 PM William J. Bowman <[email protected]> wrote: > I can't seem to use (cross t). > If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently > happy. > But alas: > https://github.com/racket/redex/issues/92 > https://github.com/racket/redex/issues/54 > https://github.com/racket/redex/pull/147 > > I'll see about tweaking Redex, but now I'm wondering what to call this > "closure". > To me, it's the obvious compatible closure, but apparently not. > (It's the one the paper I'm reading calls "the congruence closure", as far > as I > can tell; the definition is missing, hence my Redex modeling.) > > -- > William J. Bowman > > On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote: > > There isn't a simple way to do that using the exported stuff currently > but > > those nonterminals are hiding inside and one could expose them in the > > pattern language I think. (TT is accessible via (cross t) I think.) > > definitely requires fiddling with intervals but the work would be more > > exposing and documenting and the like, not really deep changes. > > > > But there may be a clever way to make it work with the existing APIs? I > am > > not sure. > > > > Robby > > > > On Fri, May 3, 2019 at 8:38 PM William J. Bowman <[email protected] > > > > wrote: > > > > > Ah, I see. > > > Those are the VT and TT I want, but then I also want to define: > > > > > > (C ::= VT TT) > > > > > > and take the context-closure of C. > > > (see attached) > > > > > > Can I get my hands on the generated VT and TT easily, or would I need > to > > > tweak > > > Redex internals to automate this? > > > > > > -- > > > William J. Bowman > > > > > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > > > > (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. > > > > > > -- > > > 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.
