2

在查看 PLT redex 时，我想玩简化规则；所以我为布尔值定义了这个最小的语言：

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

现在我想将我的语言扩展到布尔方程并允许not在方程的每一边进行简化，所以我定义了：

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

希望：

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

会做的事情。but no：red1可以减少(not (not (not F)))))但不能减少(= (not T) F)))

我在这里做了什么很傻的事情吗？

4

1 回答 1

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

请注意，这在某些旧版本中不起作用。

本教程和redex 参考是两个有用信息的来源。

于 2020-07-14T17:02:11.057 回答