plt-redex: замена, избегающая захвата, бесплатно?

Question

Каждый раз, когда я определяю язык в переопределении PLT, мне нужно вручную определять (исключая захват) функцию подстановки. Например, эта модель не закончена, потому что 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?

(Спасибо, Пол Стансифер!)