On Mon, May 6, 2019 at 2:11 PM William J. Bowman <w...@williamjbowman.com> wrote: > > 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'
I can agree that the current definition isn't the best one, but this one doesn't seem right. I mean, this requires that both sides step? It is a kind of parallel reduction? That doesn't seem like something commonly wanted. > ... > > (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 is basically what redex does, but perhaps not in the way you mean it. What I'm saying is that when redex sees a language with n non-terminals, it computes n^2 new non-terminals, one for each pair. For the pair (x,y), it has a pattern that is internally `(cross x-y)` (or something like that). This non-terminal corresponds with putting a hole at each place in `x` where there is a reference to `y` (which requires duplicating productions in general, repeating each production once for each occurrence of `y` in a given production, allowing the hole to be there). In the earlier example when I wrote out the two non-terminals, TT was `(cross t-t)` and TV was `(cross t-v)`. And when you do compatible closure of `t`, redex uses `(cross t-t)`. (I hope this makes a little bit more sense.) Robby -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdONnd1j%3DDRrQOD6SqoP3doRQHhZb7ex8CxZ04fbz4MUgWw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
