Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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 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/20190508162114.GC95917%40williamjbowman.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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 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/CAL3TdOPwwt0%2Bo1s4hZaFRGoV1oOn_pvM-2o4cLV_2Jy9G%3DeDLQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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 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/20190508150511.GY95917%40williamjbowman.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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.) > 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.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
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 racket-users+unsubscr...@googlegroups.com. 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.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
On Mon, May 6, 2019 at 2:11 PM William J. Bowman wrote: > > I took a quick look at the implementation of `cross` and `compatible-closure`, > and couldn't make sense of any of it. > For now, I guess I'll manually write out the contexts, and discuss a feature > request. > > I spoke to Max a bit about what a compatible closure "ought" to be for > mutually > defined syntax. > I think right now, Redex is doing the "wrong" thing. > Suppose I have some relation "->" on my nonterminals `v` and `t`. > Right now, `compatible-closure` is computing something like this: > > t -> t' > v = v' > > t v -> t' v' > > That is, to compute the congruence rule for the `(t v)`, we lift the relation > `->` to apply under `T`, but it appears to compute the simplest possible > relation on `v`: syntactic identity. > This is the reason I don't get reduction of `t`s under a `thunk`. > > Instead, it "ought" to compute these rules: > > (extending t -> t to closure) > t -> t' > v -> v' > > t v -> t' v' 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. > ... > > (generated definition of v -> v) > > t -> t' > > λ x. t -> λx. t' > > This lifts `->` to `v` while computing the closure of `->`. > I think this should be the default behavior of `compatible-closure` on > mutually > defined nonterminals. > > I think in general, we actually want something more: for mutually defined > syntax/judgments, I might want to define `->t` and `->v` (generally, `->ᵢ > ...`), > and compute the closure of `->` w.r.t. `t` and the closure of `->v`. This is basically what redex does, but perhaps not in the way you mean it. What I'm saying is that when redex sees a language with n non-terminals, it computes n^2 new non-terminals, one for each pair. For the pair (x,y), it has a pattern that is internally `(cross x-y)` (or something like that). This non-terminal corresponds with putting a hole at each place in `x` where there is a reference to `y` (which requires duplicating productions in general, repeating each production once for each occurrence of `y` in a given production, allowing the hole to be there). In the earlier example when I wrote out the two non-terminals, TT was `(cross t-t)` and TV was `(cross t-v)`. And when you do compatible closure of `t`, redex uses `(cross t-t)`. (I hope this makes a little bit more sense.) 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/CAL3TdONnd1j%3DDRrQOD6SqoP3doRQHhZb7ex8CxZ04fbz4MUgWw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
I took a quick look at the implementation of `cross` and `compatible-closure`, and couldn't make sense of any of it. For now, I guess I'll manually write out the contexts, and discuss a feature request. I spoke to Max a bit about what a compatible closure "ought" to be for mutually defined syntax. I think right now, Redex is doing the "wrong" thing. Suppose I have some relation "->" on my nonterminals `v` and `t`. Right now, `compatible-closure` is computing something like this: t -> t' v = v' t v -> t' v' That is, to compute the congruence rule for the `(t v)`, we lift the relation `->` to apply under `T`, but it appears to compute the simplest possible relation on `v`: syntactic identity. This is the reason I don't get reduction of `t`s under a `thunk`. Instead, it "ought" to compute these rules: (extending t -> t to closure) t -> t' v -> v' t v -> t' v' ... (generated definition of v -> v) t -> t' λ x. t -> λx. t' This lifts `->` to `v` while computing the closure of `->`. I think this should be the default behavior of `compatible-closure` on mutually defined nonterminals. I think in general, we actually want something more: for mutually defined syntax/judgments, I might want to define `->t` and `->v` (generally, `->ᵢ ...`), and compute the closure of `->` w.r.t. `t` and the closure of `->v`. This would require a lot more changes and different interface, I think. A quick version would give the user access to computed contexts, allowing `(cross t)` (or something) in language definitions. Then, we could implement this easily enough in user libraries. -- William J. Bowman On Fri, May 03, 2019 at 10:09:45PM -0400, William J. Bowman wrote: > I can't seem to use (cross t). > If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently happy. > But alas: > https://github.com/racket/redex/issues/92 > https://github.com/racket/redex/issues/54 > https://github.com/racket/redex/pull/147 > > I'll see about tweaking Redex, but now I'm wondering what to call this > "closure". > To me, it's the obvious compatible closure, but apparently not. > (It's the one the paper I'm reading calls "the congruence closure", as far as > I > can tell; the definition is missing, hence my Redex modeling.) > > -- > William J. Bowman > > On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote: > > There isn't a simple way to do that using the exported stuff currently but > > those nonterminals are hiding inside and one could expose them in the > > pattern language I think. (TT is accessible via (cross t) I think.) > > definitely requires fiddling with intervals but the work would be more > > exposing and documenting and the like, not really deep changes. > > > > But there may be a clever way to make it work with the existing APIs? I am > > not sure. > > > > Robby > > > > On Fri, May 3, 2019 at 8:38 PM William J. Bowman > > wrote: > > > > > Ah, I see. > > > Those are the VT and TT I want, but then I also want to define: > > > > > > (C ::= VT TT) > > > > > > and take the context-closure of C. > > > (see attached) > > > > > > Can I get my hands on the generated VT and TT easily, or would I need to > > > tweak > > > Redex internals to automate this? > > > > > > -- > > > William J. Bowman > > > > > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > > > > (thunk TT) isn't a TT, tho? It will reduce only in a TT. > > > > > > > > Robby > > > > > > > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman > > > > > > > wrote: > > > > > > > > > > That looks like the contexts I want, but it doesn't seem to reduce > > > under a (thunk TT) in my example model. > > > > > > > > > > -- > > > > > Sent from my phoneamajig > > > > > > > > > > > On May 3, 2019, at 20:02, Robby Findler > > > wrote: > > > > > > > > > > > > Redex, when asked to create the compatible closure, creates a > > > > > > context > > > > > > and then uses that. In this case, it will create a context something > > > > > > like this: > > > > > > > > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return > > > > > > VT) > > > > > > VT ::= (thunk TT) > > > > > > > > > > > > If you want something else (I'm not sure of an algorithm to handle > > > > > > this kind of thing without coming with something like that), it > > > > > > might > > > > > > be simplest to write out the contexts that you want directly and use > > > > > > context-closure. > > > > > > > > > > > > Robby > > > > > > > > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman < > > > w...@williamjbowman.com> wrote: > > > > > >> > > > > > >> Hello all, > > > > > >> > > > > > >> I'm trying to define a model in Redex where values and terms are > > > separate > > > > > >> nonterminals, and then define a reduction relation using > > > `compatible-closure` > > > > > >> to lift the small steps to the, well, compatible closure. > > > > > >> Unfortunately, it doesn't do what I expect, pres
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
I just kind of made up the algorithm for what Redex does. It seems to coincide with what one expects for some cases at least. :) Robby On Fri, May 3, 2019 at 9:09 PM William J. Bowman wrote: > I can't seem to use (cross t). > If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently > happy. > But alas: > https://github.com/racket/redex/issues/92 > https://github.com/racket/redex/issues/54 > https://github.com/racket/redex/pull/147 > > I'll see about tweaking Redex, but now I'm wondering what to call this > "closure". > To me, it's the obvious compatible closure, but apparently not. > (It's the one the paper I'm reading calls "the congruence closure", as far > as I > can tell; the definition is missing, hence my Redex modeling.) > > -- > William J. Bowman > > On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote: > > There isn't a simple way to do that using the exported stuff currently > but > > those nonterminals are hiding inside and one could expose them in the > > pattern language I think. (TT is accessible via (cross t) I think.) > > definitely requires fiddling with intervals but the work would be more > > exposing and documenting and the like, not really deep changes. > > > > But there may be a clever way to make it work with the existing APIs? I > am > > not sure. > > > > Robby > > > > On Fri, May 3, 2019 at 8:38 PM William J. Bowman > > > wrote: > > > > > Ah, I see. > > > Those are the VT and TT I want, but then I also want to define: > > > > > > (C ::= VT TT) > > > > > > and take the context-closure of C. > > > (see attached) > > > > > > Can I get my hands on the generated VT and TT easily, or would I need > to > > > tweak > > > Redex internals to automate this? > > > > > > -- > > > William J. Bowman > > > > > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > > > > (thunk TT) isn't a TT, tho? It will reduce only in a TT. > > > > > > > > Robby > > > > > > > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman < > w...@williamjbowman.com> > > > wrote: > > > > > > > > > > That looks like the contexts I want, but it doesn't seem to reduce > > > under a (thunk TT) in my example model. > > > > > > > > > > -- > > > > > Sent from my phoneamajig > > > > > > > > > > > On May 3, 2019, at 20:02, Robby Findler < > ro...@cs.northwestern.edu> > > > wrote: > > > > > > > > > > > > Redex, when asked to create the compatible closure, creates a > context > > > > > > and then uses that. In this case, it will create a context > something > > > > > > like this: > > > > > > > > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | > (return VT) > > > > > > VT ::= (thunk TT) > > > > > > > > > > > > If you want something else (I'm not sure of an algorithm to > handle > > > > > > this kind of thing without coming with something like that), it > might > > > > > > be simplest to write out the contexts that you want directly and > use > > > > > > context-closure. > > > > > > > > > > > > Robby > > > > > > > > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman < > > > w...@williamjbowman.com> wrote: > > > > > >> > > > > > >> Hello all, > > > > > >> > > > > > >> I'm trying to define a model in Redex where values and terms are > > > separate > > > > > >> nonterminals, and then define a reduction relation using > > > `compatible-closure` > > > > > >> to lift the small steps to the, well, compatible closure. > > > > > >> Unfortunately, it doesn't do what I expect, presumably because > the > > > nonterminals > > > > > >> for values and terms are mutually defined, but > `compatible-closure` > > > takes > > > > > >> exactly one nonterminal. > > > > > >> > > > > > >> Is there a way to do what I want? > > > > > >> See attached. > > > > > >> > > > > > >> -- > > > > > >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 t
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
I can't seem to use (cross t). If it were as easy as (C ::= (cross t) (cross v)), I'd be sufficiently happy. But alas: https://github.com/racket/redex/issues/92 https://github.com/racket/redex/issues/54 https://github.com/racket/redex/pull/147 I'll see about tweaking Redex, but now I'm wondering what to call this "closure". To me, it's the obvious compatible closure, but apparently not. (It's the one the paper I'm reading calls "the congruence closure", as far as I can tell; the definition is missing, hence my Redex modeling.) -- William J. Bowman On Fri, May 03, 2019 at 09:00:34PM -0500, Robby Findler wrote: > There isn't a simple way to do that using the exported stuff currently but > those nonterminals are hiding inside and one could expose them in the > pattern language I think. (TT is accessible via (cross t) I think.) > definitely requires fiddling with intervals but the work would be more > exposing and documenting and the like, not really deep changes. > > But there may be a clever way to make it work with the existing APIs? I am > not sure. > > Robby > > On Fri, May 3, 2019 at 8:38 PM William J. Bowman > wrote: > > > Ah, I see. > > Those are the VT and TT I want, but then I also want to define: > > > > (C ::= VT TT) > > > > and take the context-closure of C. > > (see attached) > > > > Can I get my hands on the generated VT and TT easily, or would I need to > > tweak > > Redex internals to automate this? > > > > -- > > William J. Bowman > > > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > > > (thunk TT) isn't a TT, tho? It will reduce only in a TT. > > > > > > Robby > > > > > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman > > wrote: > > > > > > > > That looks like the contexts I want, but it doesn't seem to reduce > > under a (thunk TT) in my example model. > > > > > > > > -- > > > > Sent from my phoneamajig > > > > > > > > > On May 3, 2019, at 20:02, Robby Findler > > wrote: > > > > > > > > > > Redex, when asked to create the compatible closure, creates a context > > > > > and then uses that. In this case, it will create a context something > > > > > like this: > > > > > > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > > > > > VT ::= (thunk TT) > > > > > > > > > > If you want something else (I'm not sure of an algorithm to handle > > > > > this kind of thing without coming with something like that), it might > > > > > be simplest to write out the contexts that you want directly and use > > > > > context-closure. > > > > > > > > > > Robby > > > > > > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman < > > w...@williamjbowman.com> wrote: > > > > >> > > > > >> Hello all, > > > > >> > > > > >> I'm trying to define a model in Redex where values and terms are > > separate > > > > >> nonterminals, and then define a reduction relation using > > `compatible-closure` > > > > >> to lift the small steps to the, well, compatible closure. > > > > >> Unfortunately, it doesn't do what I expect, presumably because the > > nonterminals > > > > >> for values and terms are mutually defined, but `compatible-closure` > > takes > > > > >> exactly one nonterminal. > > > > >> > > > > >> Is there a way to do what I want? > > > > >> See attached. > > > > >> > > > > >> -- > > > > >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subsc
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
There isn't a simple way to do that using the exported stuff currently but those nonterminals are hiding inside and one could expose them in the pattern language I think. (TT is accessible via (cross t) I think.) definitely requires fiddling with intervals but the work would be more exposing and documenting and the like, not really deep changes. But there may be a clever way to make it work with the existing APIs? I am not sure. Robby On Fri, May 3, 2019 at 8:38 PM William J. Bowman wrote: > Ah, I see. > Those are the VT and TT I want, but then I also want to define: > > (C ::= VT TT) > > and take the context-closure of C. > (see attached) > > Can I get my hands on the generated VT and TT easily, or would I need to > tweak > Redex internals to automate this? > > -- > William J. Bowman > > On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > > (thunk TT) isn't a TT, tho? It will reduce only in a TT. > > > > Robby > > > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman > wrote: > > > > > > That looks like the contexts I want, but it doesn't seem to reduce > under a (thunk TT) in my example model. > > > > > > -- > > > Sent from my phoneamajig > > > > > > > On May 3, 2019, at 20:02, Robby Findler > wrote: > > > > > > > > Redex, when asked to create the compatible closure, creates a context > > > > and then uses that. In this case, it will create a context something > > > > like this: > > > > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > > > > VT ::= (thunk TT) > > > > > > > > If you want something else (I'm not sure of an algorithm to handle > > > > this kind of thing without coming with something like that), it might > > > > be simplest to write out the contexts that you want directly and use > > > > context-closure. > > > > > > > > Robby > > > > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman < > w...@williamjbowman.com> wrote: > > > >> > > > >> Hello all, > > > >> > > > >> I'm trying to define a model in Redex where values and terms are > separate > > > >> nonterminals, and then define a reduction relation using > `compatible-closure` > > > >> to lift the small steps to the, well, compatible closure. > > > >> Unfortunately, it doesn't do what I expect, presumably because the > nonterminals > > > >> for values and terms are mutually defined, but `compatible-closure` > takes > > > >> exactly one nonterminal. > > > >> > > > >> Is there a way to do what I want? > > > >> See attached. > > > >> > > > >> -- > > > >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
Ah, I see. Those are the VT and TT I want, but then I also want to define: (C ::= VT TT) and take the context-closure of C. (see attached) Can I get my hands on the generated VT and TT easily, or would I need to tweak Redex internals to automate this? -- William J. Bowman On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote: > (thunk TT) isn't a TT, tho? It will reduce only in a TT. > > Robby > > On Fri, May 3, 2019 at 7:16 PM William J. Bowman > wrote: > > > > That looks like the contexts I want, but it doesn't seem to reduce under a > > (thunk TT) in my example model. > > > > -- > > Sent from my phoneamajig > > > > > On May 3, 2019, at 20:02, Robby Findler wrote: > > > > > > Redex, when asked to create the compatible closure, creates a context > > > and then uses that. In this case, it will create a context something > > > like this: > > > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > > > VT ::= (thunk TT) > > > > > > If you want something else (I'm not sure of an algorithm to handle > > > this kind of thing without coming with something like that), it might > > > be simplest to write out the contexts that you want directly and use > > > context-closure. > > > > > > Robby > > > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman > > >> wrote: > > >> > > >> Hello all, > > >> > > >> I'm trying to define a model in Redex where values and terms are separate > > >> nonterminals, and then define a reduction relation using > > >> `compatible-closure` > > >> to lift the small steps to the, well, compatible closure. > > >> Unfortunately, it doesn't do what I expect, presumably because the > > >> nonterminals > > >> for values and terms are mutually defined, but `compatible-closure` takes > > >> exactly one nonterminal. > > >> > > >> Is there a way to do what I want? > > >> See attached. > > >> > > >> -- > > >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. #lang racket/base (require redex/reduction-semantics) (define-language λvL (x ::= variable-not-otherwise-mentioned) (v w ::= (thunk t) () x) (t u ::= (λ (x) t) (t v) (force v) (return v)) (TT ::= hole (λ (x) TT) (TT v) (t VT) (force VT) (return VT)) (VT ::= (thunk TT)) (C ::= VT TT) ;; How do I tell redex to compatible-close over both v and t? (anyterm ::= v t) #:binding-forms (λ (x) any_1 #:refers-to x)) (define λv--> (reduction-relation λvL (--> ((λ (x) t) v) (substitute t x v) "β") (--> (force (thunk t)) t "force"))) (define λv-->* (context-closure λv--> λvL C)) (test--> λv--> (term ((λ (x) (force (thunk (return x ())) (term (force (thunk (return ()) (test-->> λv-->* (term ((λ (x) (force (thunk (return x ())) (term (return ( (test-->> λv-->* (term (λ (x) (force (thunk (return x) (term (λ (x) (return x ;; Fails, since thunk is a v, not a t. (test-->> λv-->* (term (thunk (λ (x) (force (thunk (return x)) (term (thunk (λ (x) (return x)
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
(thunk TT) isn't a TT, tho? It will reduce only in a TT. Robby On Fri, May 3, 2019 at 7:16 PM William J. Bowman wrote: > > That looks like the contexts I want, but it doesn't seem to reduce under a > (thunk TT) in my example model. > > -- > Sent from my phoneamajig > > > On May 3, 2019, at 20:02, Robby Findler wrote: > > > > Redex, when asked to create the compatible closure, creates a context > > and then uses that. In this case, it will create a context something > > like this: > > > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > > VT ::= (thunk TT) > > > > If you want something else (I'm not sure of an algorithm to handle > > this kind of thing without coming with something like that), it might > > be simplest to write out the contexts that you want directly and use > > context-closure. > > > > Robby > > > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman > >> wrote: > >> > >> Hello all, > >> > >> I'm trying to define a model in Redex where values and terms are separate > >> nonterminals, and then define a reduction relation using > >> `compatible-closure` > >> to lift the small steps to the, well, compatible closure. > >> Unfortunately, it doesn't do what I expect, presumably because the > >> nonterminals > >> for values and terms are mutually defined, but `compatible-closure` takes > >> exactly one nonterminal. > >> > >> Is there a way to do what I want? > >> See attached. > >> > >> -- > >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
That looks like the contexts I want, but it doesn't seem to reduce under a (thunk TT) in my example model. -- Sent from my phoneamajig > On May 3, 2019, at 20:02, Robby Findler wrote: > > Redex, when asked to create the compatible closure, creates a context > and then uses that. In this case, it will create a context something > like this: > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) > VT ::= (thunk TT) > > If you want something else (I'm not sure of an algorithm to handle > this kind of thing without coming with something like that), it might > be simplest to write out the contexts that you want directly and use > context-closure. > > Robby > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman >> wrote: >> >> Hello all, >> >> I'm trying to define a model in Redex where values and terms are separate >> nonterminals, and then define a reduction relation using `compatible-closure` >> to lift the small steps to the, well, compatible closure. >> Unfortunately, it doesn't do what I expect, presumably because the >> nonterminals >> for values and terms are mutually defined, but `compatible-closure` takes >> exactly one nonterminal. >> >> Is there a way to do what I want? >> See attached. >> >> -- >> 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Redex compatible closure of mutually defined nonterminals
Redex, when asked to create the compatible closure, creates a context and then uses that. In this case, it will create a context something like this: TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) VT ::= (thunk TT) If you want something else (I'm not sure of an algorithm to handle this kind of thing without coming with something like that), it might be simplest to write out the contexts that you want directly and use context-closure. Robby On Fri, May 3, 2019 at 6:42 PM William J. Bowman wrote: > > Hello all, > > I'm trying to define a model in Redex where values and terms are separate > nonterminals, and then define a reduction relation using `compatible-closure` > to lift the small steps to the, well, compatible closure. > Unfortunately, it doesn't do what I expect, presumably because the > nonterminals > for values and terms are mutually defined, but `compatible-closure` takes > exactly one nonterminal. > > Is there a way to do what I want? > See attached. > > -- > 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 racket-users+unsubscr...@googlegroups.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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Redex compatible closure of mutually defined nonterminals
Hello all, I'm trying to define a model in Redex where values and terms are separate nonterminals, and then define a reduction relation using `compatible-closure` to lift the small steps to the, well, compatible closure. Unfortunately, it doesn't do what I expect, presumably because the nonterminals for values and terms are mutually defined, but `compatible-closure` takes exactly one nonterminal. Is there a way to do what I want? See attached. -- 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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. #lang racket/base (require redex/reduction-semantics) (define-language λvL (x ::= variable-not-otherwise-mentioned) (v w ::= (thunk t) () x) (t u ::= (λ (x) t) (t v) (force v) (return v)) ;; How do I tell redex to compatible-close over both v and t? (anyterm ::= v t) #:binding-forms (λ (x) any_1 #:refers-to x)) (define λv--> (reduction-relation λvL (--> ((λ (x) t) v) (substitute t x v) "β") (--> (force (thunk t)) t "force"))) ; This ought to reduce under vs, as well ts, since they are mutually defined. ; But it only uses t. (define λv-->* (compatible-closure λv--> λvL t)) ; Doesn't work, but in a different way. #;(define λv-->* (compatible-closure λv--> λvL anyterm)) (test--> λv--> (term ((λ (x) (force (thunk (return x ())) (term (force (thunk (return ()) (test-->> λv-->* (term ((λ (x) (force (thunk (return x ())) (term (return ( (test-->> λv-->* (term (λ (x) (force (thunk (return x) (term (λ (x) (return x ;; Fails, since thunk is a v, not a t. (test-->> λv-->* (term (thunk (λ (x) (force (thunk (return x)) (term (thunk (λ (x) (return x)
