On Tue, May 7, 2019 at 9:19 PM William J. Bowman <w...@williamjbowman.com> wrote: > > On Tue, May 07, 2019 at 03:55:09PM -0500, Robby Findler wrote: > > 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. > Yeah, that was a mistake, and not the only one I made in that email. > Let me try again. > > In this model, I'm actually trying to define two reduction relations and take > the compatible-closure of these two mutually defined relations.
For the record, this situation isn't one that I'd considered when designing this part of redex. I'd just been thinking about a single relation and automatically giving you the compatible closure of it. (I thought of the context-closure operation only as a stepping stone to that.) > The first is of the form `t -> t'` and the second of the form `v -> v'`. > `v -> v'` is trivial (contains no reductions), but it's compatible closure > contains an the following interesting reduction rule. > > t -> t' > ------------ > thunk t -> thunk t' > > It looks like the compatible-closure of `t -> t'` is doing the right thing: it > does apply the above rule, as long as I was reducing a `t` to begin with. > The real problem is that I can't access the `v -> v'` relation directly, so I > can't apply any reduction relation at all to `v`s. It sounds to me like you want to use the (cross t-v) (or maybe (cross v-t), I get them mixed up) context to close the `t` relation. Does that sound right? > This is particularly annoying, since Redex has computed that relation and can > use it internally. (I look at it as if the interesting thing it computed is the context not the relation per se but I think I'm splitting hairs here.) > I can't define a trivial reduction relation (all reduction relations need > rules), so I can't manually call `compatible-closure` on this trivial > relation. > I also can't access `cross` in my surface language to define contexts, so I > can't take the context closure without writing out about 50 lines of contexts > :(. I have never liked the word "cross" and view this thing as a wart on Redex. What if I were to add a new kind of pattern, something like: (compatible-closure-of t) (compatible-closure-of t #:with-respect-to v) (where the `t` and `v` positions must be names of non-terminals (but aren't pattern variables)). And then you could use context-closure or you could just drop that into an `in-hole` yourself if you wanted to? I'm not sure how to typeset that :) but otherwise adding that seems straightforward because it is really just about exposing existing functionality. 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/CAL3TdOOT316wMR7SL%3DVhKihu9tCH%3DuUOzURrmkGcEfwRWJyrXA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
