On Mon, May 6, 2019 at 2:11 PM William J. Bowman <[email protected]> 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 [email protected]. 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.
