了解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表示：

用y（外部括号）替换x（上面表达式中的内部括号）中x的出现。并且由于y中没有x，因此答案应该只是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指向y中的第一个let*。如果在DrRacket中单击y，则可以看到此内容。

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

(lambda (y«0») y)
现在很明显，此表达式中的两个y不同。