Great! I've pushed it. Hopefully the docs make it clear how to define the C you wanted earlier. If they don't let me know and I'll fix 'em.
Robby On Wed, May 8, 2019 at 11:21 AM William J. Bowman <[email protected]> wrote: > > Yeah, I think I would be. > > On Wed, May 08, 2019 at 11:13:12AM -0500, Robby Findler wrote: > > Hi William: are you agreeing that if redex added a new pattern that > > you would be in good shape or not? > > > > Thanks, > > Robby > > > > On Wed, May 8, 2019 at 10:05 AM William J. Bowman > > <[email protected]> wrote: > > > > > > On Wed, May 08, 2019 at 08:31:26AM -0500, Robby Findler wrote: > > > > On Tue, May 7, 2019 at 9:19 PM William J. Bowman > > > > <[email protected]> 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.) > > > Sure, I can see how the current implementation came about. > > > And this is the first time I've needed this in Redex. > > > I'm just trying to explain a use case that it would be nice for Redex to > > > support. > > > > > > > > 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? > > > Well, I want to use both. > > > I want to use the closure w.r.t. `(cross t-t)` when reducing `t`s and > > > w.r.t. > > > `(cross t-v)` when reducing `v`s. > > > But that's about right. > > > > > > > (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 think that's an alternative way of viewing it, but the semanticist in > > > me wants > > > to split that hair. > > > Considering it the closure of the `t -> t'` relation w.r.t. to `(cross > > > t-v)` > > > is strange, since closure of the relation actually acts on `v`s instead > > > of `t`s. > > > Said another way, the type of the relations changes between the original > > > relation and its closure w.r.t. `v`. > > > Considering the closure of two mutually defined relations, `t -> t'` and > > > `v -> > > > v'`, is a little nicer---each relation continues to act on `t`s and `v`s, > > > i.e., > > > the types don't change. > > > > > > I think these end up implementing the same relation, though. > > > At least it seems to when I manually write out the 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)). > > > I think this would be a good feature, although that particular name could > > > be > > > confusing: why is it different than `compatible-closure`. > > > But we're getting into bike shed territory. > > > > > > > I'm not sure how to typeset that :) but otherwise adding that seems > > > > straightforward because it is really just about exposing existing > > > > functionality. > > > Personally, I'd like the option to typeset it as the contexts I would > > > write out > > > by hand, but this looks difficult to do in the current implementation. > > > > > > -- > > > 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]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/20190508162114.GC95917%40williamjbowman.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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdONS%2BTc7KzW%2BB%3D%3Dkh-PxQYy%3Df62ubeZ0AZ%2B2doYnXij-jw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
