在查看 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)))
我在这里做的事情真的很傻吗?
最佳答案
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 。
关于racket - 扩展归约关系,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/62517001/