Расширение редукционного отношения

Question

Когда я смотрел на 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))

сделаю вещь. Но нет: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))

Обратите внимание, что это не работает в некоторых старых версиях.

Два источника полезной информации - это этот учебник и, конечно же, справочник по редексам.