plt-redex:避免捕获免费替换? [英] plt-redex: capture-avoiding substitution for free?
问题描述
每次我在 PLT redex 中定义一种语言时,我都需要手动定义一个(避免捕获)替换函数.例如,这个模型没有完成,因为 subst
没有定义:
Every time I define a language in PLT redex, I need to manually define a (capture-avoiding) substitution function. For example, this model isn't finished because subst
isn't defined:
#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 可以自动处理替换吗?
But the definition of subst
is obvious. Can PLT redex handle substitution automatically?
推荐答案
是的!只需使用 #:binding-forms
声明.
Yes! Just describe your language's binding structure with a #:binding-forms
declaration.
这是一个类似的模型,通过 substitute
函数:
Here's a similar model with capture-avoiding substitution via the substitute
function:
#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?
Alphabetic equivalence comes for free too, see alpha-equivalent?
(谢谢Paul Stansifer!)
这篇关于plt-redex:避免捕获免费替换?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!