了解 Redex 中的 lambda 替换

Question

假设我在 Redex 中定义了以下内容：

(define-language L
    [e ::= (λ x e) (e e) x]
    [x ::= variable-not-otherwise-mentioned]
    #:binding-forms
    (λ x e #:refers-to x))

现在，我认为表达式 (λ y x) x 的意思是：

用x（大括号外）替换x（上述表达式中大括号内）中出现的y。而且由于 x 中没有 y，所以答案应该只是 x。那么(λ y x) x y应该returnx y。但是：

(default-language L)
(term (substitute (λ y x) x y))
'(λ y«0» y)

为什么它 return 是一个函数？ y<<0>> 是什么意思？我是不是误会了term (substitute ..)？

这个结果我也没看懂：

(term (substitute (λ y x) x true))
'(λ y«1» true)

谁能帮我破译一下？我是 Racket/Redex.

的新手

Answer 1

y«0» 和 y«1» 只是意味着虽然变量被命名为 y，但它与传入的 y 不同。#:refers-to标志用于使表单尊重捕获避免替换。

总的来说，思路是这样的，这个程序的结果应该是什么：

((lambda (x) (lambda (y) x))
 y)

这个程序的计算结果应该是 4 还是 3？如果我们使用简单的替换，那么我们可以说程序减少到：

(lambda (y) y)

这是恒等函数。如果我们将 y 绑定到 5 并将结果称为：

，则这一点很明显

(let* ([y 5]
       [f ((lambda (x) (lambda (y) x))
            y)])
  (f 6))

这里，我们期望结果为 5，即使我们将 6 传递给 f。这是因为结果中的 y 指向 let* 中的第一个 y。如果你在 DrRacket 中鼠标 y 就可以看到这个。

为了避免这种情况，它不是简单地将表达式中的所有 x 替换为 y，而是将所有绑定器重命名为新名称，因此您得到：

(lambda (y«0») y)

现在很明显这个表达式中的两个 y 是不同的。

Understanding lambda substitution in Redex