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 <clkl...@eecs.northwestern.edu> wrote: > > On Fri, Aug 5, 2011 at 8:13 AM, <clkl...@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
_________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
