racket - 扩展归约关系

Question

在查看 PLT redex 时，我想尝试简化规则；所以我为 bool 值定义了这种最小语言:

(define-language B0
  (b T F (not b)))

我想简化一个 (not (not ...)) 链，所以我扩展了语言来处理上下文并定义了一个减少关系来简化 not :

(define-extended-language B1 B0
  (C (not C) hole)
  (BV T F))

(define red0
  (reduction-relation
   B1
   (--> (in-hole C (not T)) (in-hole C F))
   (--> (in-hole C (not F)) (in-hole C T))))

现在我想将我的语言扩展到 bool 方程并允许在方程的每一侧进行 not -simplification，所以我定义了:

(define-extended-language B2 B1
  (E (= C b) (= b C)))

希望:

(define red1
  (extend-reduction-relation red0 B2))

会做的事情。
但不行: red1 可以减少 (not (not (not F))))) 但不能减少 (= (not T) F)))我在这里做的事情真的很傻吗？

Answer 1

red1 的问题在于它只包含使用有限上下文 red0 的 C 规则。为了使其按预期工作，您可以添加修改后的旧规则以使用 E 或以某种方式使最终扩展上下文具有名称 C 。一种不太乏味的方法可能是:

(define-language L)

(define R
  (reduction-relation L
    (--> (not T) F)
    (--> (not F) T)))

(define-language LB
  (b T F (not b))
  (C (compatible-closure-context b)))

(define RB (context-closure R LB C))

(define-extended-language LBE LB
  (e (= b b))
  (C .... (compatible-closure-context e #:wrt b)))

(define RBE (extend-reduction-relation RB LBE))

请注意，这在某些旧版本中不起作用。
有用信息的两个来源是 this tutorial ，当然还有 the redex reference 。