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 <[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. -- 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.
