了解 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（上述表达式中的大括号内）中出现的y 替换为x（大括号外）。由于x 中没有y，所以答案应该只是x。然后(λ y x) x y 应该返回x y。但是：

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

为什么它返回一个函数？ 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 上，您可以看到这一点。

为避免这种情况，与其将表达式中的所有xs 简单替换为ys，不如将所有活页夹重命名为新名称，因此您会得到：

(lambda (y«0») y)

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