[racket-dev] [plt] Push #23181: master branch updated

1. I like Robby's mode suggestion. 

2. I prefer shorter keywords, e.g., define-judgment. 

3. Why is this in github and not in the docs? 


On Aug 5, 2011, at 9:56 PM, Robby Findler wrote:

> How about 
> 
>  #:mode (sum I I O)
> 
> for the mode spec where the #:mode keyword is optional but, if present must be followed by what looks like a use of the relation but with a
> Mode?
> 
> Robby
> 
> On Friday, August 5, 2011, Casey Klein <clklein at eecs.northwestern.edu> wrote:
> > On Fri, Aug 5, 2011 at 8:13 AM,  <clklein at racket-lang.org> wrote:
> >> clklein has updated `master' from 1a65678924 to 576272362b.
> >>  http://git.racket-lang.org/plt/1a65678924..576272362b
> >>
> >
> > This push adds a more general way to define relations in Redex,
> > currently under the name define-judgment-form. For those of you
> > familiar with the existing define-relation form, this new form lifts
> > the restriction that relations have no outputs when executed. In
> > particular, it lets you specify which positions are inputs and which
> > are outputs, and it statically checks that the outputs can be computed
> > from the inputs without "guessing" any intermediate values.
> >
> > Here's a simple example:
> >
> > (define-language nats
> >  (n z (s n)))
> >
> > (define-judgment-form nats
> >  mode : O O I
> >  sum ⊆ n × n × n
> >  [(sum z n n)]
> >  [(sum (s n_1) n_2 (s n_3))
> >   (sum n_1 n_2 n_3)])
> >
> >> (judgment-holds (sum (s (s z)) (s z) (s (s (s z)))))
> > true
> >> (judgment-holds (sum (s (s z)) (s z) (s (s z))))
> > false
> >> (judgment-holds (sum (s z) n (s (s z))) n)
> > `((s z))
> >> (judgment-holds (sum n_1 n_2 (s (s z))) (n_1 n_2))
> > `(((s (s z)) z) ((s z) (s z)) (z (s (s z))))
> >
> > I see three use cases:
> >
> > 1. Defining type systems in a way that supports mechanized
> > typesetting. Here's an example:
> >
> > https://gist.github.com/1128672
> >
> > There are still plenty of type systems Redex can't express, but the
> > new form gets a lot of low-hanging fruit.
> >
> > 2. Defining structural operational semantics in a way that supports
> > mechanized typesetting. Here's an example:
> >
> > https://gist.github.com/1128685
> >
> > Relations defined in this way don't work directly with traces. You can
> > embed them in reduction-relation, as the example demonstrates, but you
> > lose out on edge labels. It shouldn't be too difficult to rig up
> > something better, if this turns out to be important.
> >
> > 3. Defining relations using something like multi-valued metafunctions.
> > Here's an example in which (add1 e) may reduce to 0.
> >
> > https://gist.github.com/1128692
> >
> > Any feedback is welcome, but I'm especially interested in opinions on
> > two points:
> >
> > 1. Is there a better name than define-judgment-form? I would have
> > liked the name define-relation, if it weren't already taken. Is it OK
> > to overload it?
> >
> > 2. Should mode declarations use a different syntax? I tried to do
> > something in the paren-free style of define-relation contracts, but I
> > don't like the result -- partially because I personally like parens,
> > partially because it makes it harder to give good error messages.
> >
> > _________________________________________________
> >  For list-related administrative tasks:
> >  http://lists.racket-lang.org/listinfo/dev _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110806/65f50fe8/attachment.html>