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. 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. This is particularly annoying, since Redex has computed that relation and can use it internally. 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 :(. -- 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/20190508021903.GW95917%40williamjbowman.com. For more options, visit https://groups.google.com/d/optout.
