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。有没有办法制作“例外”模式，避免检查所有构成案例？

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 使其在渲染图形时不绘制侧面条件。

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