Redex 不匹配

Question

定义语义的常用方法是（例如）：

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

例如，考虑

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

然后我们可以定义归约关系

(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)))

这是执行此操作的自然方法，因为它避免了为 3 种失败情况（数字字符串、字符串数字、字符串字符串）中的每一个编写单独的匹配器。但是，它会产生这样的问题运行：

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

（正确地）显示它可以让您减少到错误或数字 4。有没有办法制作一个 "except" 模式来避免必须检查所有组成情况？

Answer 1

这里要使用的是side-condition和redex-match?的组合。扩展你的归约关系给出：

(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))))))))

这只是说只要第一个规则不成立就可以采用第二个规则，这是论文中隐含的意思，只是没有在图中明确说明。（注意可以用side-condition/hidden让它在渲染图的时候不画side condition）

您可以使用此方法扩展到您想要禁止的任意数量的模式。

Redex 不匹配

Redex Does Not Match

racket

plt-redex