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
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
> > 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
> > > > 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 unsub
