Re: [racket-users] Redex compatible closure of mutually defined nonterminals

2019-05-10 Thread Robby Findler
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 

[racket-users] Re: What is the address of the venue for RacketCon ?

2019-05-10 Thread Eric Eide
Brian Adkins  writes:

> Since The City Library has multiple locations, it would be helpful to simply
> list on the website the address of the specific location at which we'll be
> meeting.

RacketCon will be at the Main Library:

210 East 400 South
Salt Lake City, UT 84111

-- 
---
Eric Eide   . University of Utah School of Computing
http://www.cs.utah.edu/~eeide/ . +1 (801) 585-5512 voice, +1 (801) 581-5843 FAX

-- 
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/m1bm0aflfb.fsf%40gris-dmz.flux.utah.edu.
For more options, visit https://groups.google.com/d/optout.