I took a quick look at the implementation of `cross` and `compatible-closure`, and couldn't make sense of any of it. For now, I guess I'll manually write out the contexts, and discuss a feature request.
I spoke to Max a bit about what a compatible closure "ought" to be for mutually defined syntax. I think right now, Redex is doing the "wrong" thing. Suppose I have some relation "->" on my nonterminals `v` and `t`. Right now, `compatible-closure` is computing something like this: t -> t' v = v' ------------ t v -> t' v' That is, to compute the congruence rule for the `(t v)`, we lift the relation `->` to apply under `T`, but it appears to compute the simplest possible relation on `v`: syntactic identity. This is the reason I don't get reduction of `t`s under a `thunk`. Instead, it "ought" to compute these rules: (extending t -> t to closure) t -> t' v -> v' ------------ t v -> t' v' ... (generated definition of v -> v) t -> t' ------------ λ x. t -> λx. t' This lifts `->` to `v` while computing the closure of `->`. I think this should be the default behavior of `compatible-closure` on mutually defined nonterminals. I think in general, we actually want something more: for mutually defined syntax/judgments, I might want to define `->t` and `->v` (generally, `->ᵢ ...`), and compute the closure of `->` w.r.t. `t` and the closure of `->v`. This would require a lot more changes and different interface, I think. A quick version would give the user access to computed contexts, allowing `(cross t)` (or something) in language definitions. Then, we could implement this easily enough in user libraries. -- William J. Bowman On Fri, May 03, 2019 at 10:09:45PM -0400, William J. Bowman 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 <w...@williamjbowman.com> > > 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 > > > > <w...@williamjbowman.com> > > > 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 <ro...@cs.northwestern.edu> > > > 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 < > > > w...@williamjbowman.com> 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 racket-users+unsubscr...@googlegroups.com. > > > > > >> 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 racket-users+unsubscr...@googlegroups.com. > > > > > 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 racket-users+unsubscr...@googlegroups.com. > > > > 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 racket-users+unsubscr...@googlegroups.com. > > > 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 racket-users+unsubscr...@googlegroups.com. > > 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 racket-users+unsubscr...@googlegroups.com. > 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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
