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功能與捕獲避免替換一個類似的模式：（！謝謝Paul Stansifer）

#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?