K 组合器的绑定变量检查失败

Question

我最近得到了 "Essentials of Programming Languages" 的第二版。在第 29 页，本书介绍了以下用于 lambda 演算的 Scheme 风格语法：

<expression> ::= <identifier>
             ::= (lambda (<identifier>) <expression>)
             ::= (<expression> <expression>)

接着介绍自由变量和绑定变量的定义（定义 1.3.3，第 31 页），内容如下：

A variable x occurs free in a lambda calculus expression E if and only if

1. E is a variable reference and E is the same as x; or
2. E is of the form (lambda (y) E'), where y is different from x and x occurs free in E'; or
3. E is of the form (E1 E2) and x occurs free in E1 or E2.

A variable x occurs bound in a lambda calculus expression E if and only if

1. E is of the form (lambda (y) E'), where x occurs bound in E' or x and y are the same variable and y occurs free in E'; or
2. E is of the form (E1 E2) and x occurs bound in E1 or E2.

这样的定义很容易在两个 Scheme 过程中转换，分别命名为 occurs-free? 和 occurs-bound?:

(define occurs-free?
  (lambda (var exp)
    (cond
      ((symbol? exp) (eqv? exp var))
      ((eqv? (car exp) 'lambda)
       (and (not (eqv? (caadr exp) var))
            (occurs-free? var (caddr exp))))
      (else (or (occurs-free? var (car exp))
                (occurs-free? var (cadr exp)))))))

(define occurs-bound?
  (lambda (var exp)
    (cond
      ((symbol? exp) #f)
      ((eqv? (car exp) 'lambda)
       (or (occurs-bound? var (caddr exp))
           (and (eqv? (caadr exp) var)
                (occurs-free? var (caddr exp)))))
      (else (or (occurs-bound? var (car exp))
                (occurs-bound? var (cadr exp)))))))

当组合器（即仅由绑定变量组成的过程）作为输入时，人们会期望 occurs-bound? 到 return #t。但是，K 组合器的测试失败：

> (occurs-bound? 'x '(lambda (c) (lambda (x) c)))
#f

这是因为在绑定变量的定义中第 1 点指出，对于要绑定的变量，它必须在 lambda 中量化，然后在其主体中出现自由。由于 x 在内部 lambda 的主体中被忽略，因此测试 returns false.

显然，occurs-bound?没有出现在第三版中，因此无法与本书的最新版本进行任何比较。

上面的定义是有缺陷的，还是我遗漏了什么？ Here's a repl for the code.

谢谢

Answer 1

为什么要有瑕疵？你怀疑的根源是什么？

'x 是否出现在 '(lambda (c) (lambda (y) c)) 中？

'x 是否出现在 '(lambda (c) (lambda (z) c)) 中？

你不觉得奇怪吗？我希望不会。那么为什么要考虑在 alpha-equivalent '(lambda (c) (lambda (x) c)) 中发生绑定呢？

不应该。它甚至不存在。

K 组合器的绑定变量检查失败

Check for bound variables fails for K combinator

scheme

grammar

lambda-calculus

combinators