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