racket - 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 描述您的语言的绑定(bind)结构即可。声明。

这是一个类似的模型，通过 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?

(谢谢Paul Stansifer!)