Redex Does Not Match

Question

A common way of defining semantics is (for example):

return v if [some other condition]
otherwise, return error

For example, consider

(define-language simple-dispatch
   (e ::= v (+ e e))
   (v ::= number string)
   (res ::= e err)
   (E ::= hole (+ E e) (+ v E)))

We could then define the reduction relation

(define s-> (reduction-relation simple-dispatch
  #:domain res
  (--> (in-hole E (+ number_1 number_2))
       (in-hole E ,(+ number_1 number_2)))
  (--> (in-hole E (+ any any))
       err)))

This is the natural way to do this, because it avoids having to write individual matchers for each of the 3 failure cases (number string, string number, string string). However, it then creates the problem that running it like this:

(apply-reduction-relation s-> (term (+ 2 2)))

Shows (correctly) that it lets you reduce both to an error or to the number 4. Is there a way to make an "except" pattern that avoids having to check all of the constituent cases?

Answer 1

What you want to use here is a combination of side-condition and redex-match?. Extending your reduction-relation gives:

(define s-> (reduction-relation simple-dispatch
  #:domain res
  (--> (in-hole E (+ number_1 number_2))
       (in-hole E ,(+ (term number_1) (term number_2))))
  (--> (in-hole E (+ any_1 any_2))
       err
       (side-condition
        (not (redex-match? simple-dispatch
                           (+ number number)
                           (term (+ any_1 any_2))))))))

This just says you can take the second rule so long as the first one is not true, which is what the papers are saying implicitly, and just didn't draw out explicitly in the figure. (Note that you can use side-condition/hidden to get it to not draw the side condition when rendering the figure).

You can use this method to scale up to any number of patterns you want to disallow.