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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110805/d8c7bfaa/attachment.html>