plt-redex：避免捕获免费替换？

Question

每次我在 PLT redex 中定义一种语言时，我都需要手动定义一个（避免捕获）替换函数。例如，这个模型没有完成，因为subst没有定义：

#lang racket/base
(require redex/reduction-semantics)

(define-language ?
  [V ::= x (? x M)]
  [M ::= (M M) V]
  [C ::= hole (V C) (C M)]
  [x ::= variable-not-otherwise-mentioned])

(define -->?
  (reduction-relation ?
    [--> (in-hole C ((? x M) V))
         (in-hole C (subst M x V))]))

但定义subst是显而易见的。PLT redex 可以自动处理替换吗？

Answer 1

是的！只需用#:binding-forms声明描述您的语言的绑定结构。

这是一个类似的模型，通过substitute函数避免捕获替换：

#lang racket/base
(require redex/reduction-semantics)

(define-language ?
  [V ::= x (? x M)]
  [M ::= (M M) V]
  [C ::= hole (V C) (C M)]
  [x ::= variable-not-otherwise-mentioned]
  #:binding-forms
  (? x M #:refers-to x)) ;; "term M refers to the variable x"

(define -->?
  (reduction-relation ?
    [--> (in-hole C ((? x M) V))
         (in-hole C (substitute M x V))]))

(apply-reduction-relation -->?
  (term ((? x (? y x)) y)))
;; '((? y«2» y))

字母等效也是免费的，请参阅 alpha-equivalent?

（谢谢保罗·斯坦西弗！）