对 let 到 lambda 的转换感到困惑

Question

我目前正在阅读Mike Vanier撰写的关于 Y-combinator的这篇很棒的文章。在解释中删除了以下行：

事实证明，任何 let 表达式都可以使用以下等式转换为等效的 lambda 表达式：

(let ((x <expr1>)) <expr2>) ==> ((lambda (x) <expr2>) <expr1>)

文章通过转换来说明这个语句：

(define (part-factorial self)
  (let ((f (self self)))
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1)))))))

到：

(define (part-factorial self)
  ((lambda (f)
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1))))))
  (self self)))

现在，我明白了上面两个代码片段是如何以及为什么是相同的，尽管我无法理解转换let为的一般方程lambda是：

(let ((x <expr1>)) <expr2>)
==> ((lambda (x) <expr2>) <expr1>)

我很感激详细的解释。

Answer 1

我最终自己弄清楚了=）。

我缺少的一点是：

(let ((x <expr1>)) <expr2>)
==> ((lambda (x) <expr2>) <expr1>)

x存在，某处， inside <expr2>，所以它更像是：

(let ((x <expr1>)) <expr-containing-x>)
==> ((lambda (x) <expr-containing-x>) <expr1>)

话虽如此，如果我们将替换x为f：

(define (part-factorial self)
  (let ((f (self self)))
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1)))))))

以及：

(define (part-factorial self)
  ((lambda (f)
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1))))))
  (self self)))

并且将突出显示x，<expr1>并且<expr2>使用不同的颜色，转换公式应该变得清晰：

Answer 2

你应该想象有一个非常小的 lisp 语言，它有lambda但没有let. 你想做：

(let ((nsq (square n)))
  (+ nsq nsq))

您知道这nsq是一个新变量，并且 的主体let可以成为一个函数：

(lambda (nsq) (+ nsq nsq))

然后你需要使用它来获得相同的值：

((lambda (nsq) (+ nsq nsq)) (square n))

想象一下，您的简单方案具有宏，因此您实现为let：

(define-syntax let
  (syntax-rules ()
    [(let ((binding value) ...)
       body ...)
     ((lambda (binding ...)
        body ...)
      value ...)]))

请注意，在许多实现中，这实际上正是以这种方式发生的。