racket - 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。有没有办法制作一个“异常(exception)”模式，以避免检查所有组成情况？

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

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