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

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.