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 <<a href="mailto:clklein@eecs.northwestern.edu">clklein@eecs.northwestern.edu</a>> wrote: > On Fri, Aug 5, 2011 at 8:13 AM, <<a href="mailto:clklein@racket-lang.org">clklein@racket-lang.org</a>> wrote: >> clklein has updated `master' from 1a65678924 to 576272362b. >> <a href="http://git.racket-lang.org/plt/1a65678924..576272362b">http://git.racket-lang.org/plt/1a65678924..576272362b</a> >> > > 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: > > <a href="https://gist.github.com/1128672">https://gist.github.com/1128672</a> > > 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: > > <a href="https://gist.github.com/1128685">https://gist.github.com/1128685</a> > > 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. > > <a href="https://gist.github.com/1128692">https://gist.github.com/1128692</a> > > 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: > <a href="http://lists.racket-lang.org/listinfo/dev">http://lists.racket-lang.org/listinfo/dev</a>