1

假设我在 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意思是：

用（外大括号）替换出现的yin x（上述表达式中的大括号内）。x既然没有yin x，答案应该是 just 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 的新手。

4

1 回答 1

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*。如果您y在 DrRacket 中使用鼠标，您可以看到这一点。

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

(lambda (y«0») y)

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

于 2020-02-25T19:17:12.400 回答