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 <
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.)
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