跟踪 lambda 表达式求值

Question

我在使用 Scheme 中一些看起来很棘手的 lambda 表达式时遇到了问题，我想看看解释器是如何评估它们的。

我希望 Scheme 解释器打印所有评估步骤，如 SICP Section 1.1.5, "The Substitution Model for Procedure Application" 所示。

我正在寻找使用任何 Scheme 解释器的解决方案。我已经尝试过Racket's tracing，但它只跟踪过程调用，而不是每个表达式。

激励例子

给定来自SICP Exercise 2.6的教会数字的定义：

(define zero (lambda (f) (lambda (x) x)))

(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

和任务：

直接定义one 和two（不是zero 和add-1）。

我希望根据评估(add-1 zero) 和(add-1 (add-1 zero)) 的结果来检查我对one 和two 的定义。

这是我希望 Scheme 解释器打印出来的内容：

> (add-1 zero)
(add-1 (lambda (f) (lambda (x) x)))
(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) x)) f) x))))
(lambda (f) (lambda (x) (f ((lambda (x) x) x))))
(lambda (f) (lambda (x) (f x)))
>

Answer 1

试试 Racket 的内置步进器，answer 中有一些操作方法。

Answer 2

这很容易使用类似组合器的方程（was once called applicative style I believe）

zero f x = x
add1 n f x = f (n f x)

one f x = add1 zero f x = f (zero f x) = f x         **(1)**
two f x = add1 one f x = f (one f x) = f (f x)       **(2)**

使用组合器，一切都被柯里化了：a b c d 实际上是 (((a b) c) d) 和 a b c = d 等价于 (define a (lambda (b) (lambda (c) d)))。

现在很清楚f和x的本意是什么：x代表“零”数据元素的具体实现，f代表“后继”操作的具体实现，与“零”的给定具体实现兼容。 f 和 x 真的应该用助记符命名：

zero s z = z
add1 n s z = s (n s z)

不再那么难看，语法更方便，对吧？ lambda 本身就是一个印刷事故。现在，

one s z = s z         ; e.g. (1+ 0)
two s z = s (s z)     ; e.g. (1+ (1+ 0))

---

根据SICP 1.1.3 combinations evaluation过程跟踪步骤，

• 要评估组合，请执行以下操作：
  1. 评估组合的子表达式。
  2. 将作为最左边子表达式（运算符）值的过程应用于作为其他子表达式（操作数）值的参数。

还有1.1.5 sustitution model for procedure application

• 要将复合过程应用于参数，请评估过程主体，并将每个形式参数替换为相应的参数。

我们得到

add1 zero = 
  ( n f x => f (n f x) ) ( f x => x ) =
  ( f x => f ( ( f x => x ) f x ) )

这里替换实际上停止了，因为结果是一个简单的 lambda 表达式，即不是组合。只有当再提供两个参数时，才会完整地完成评估：

add1 zero s z = 
  ( n f x => f (n f x) ) ( f x => x ) s z =
  ( f x => f ( ( f x => x ) f x ) ) s z =
  ( x => {s} ( ( f x => x ) {s} x ) ) z =    ; {s} is definition-of s
  {s} ( ( f x => x ) {s} {z} ) =             ; {z} is definition-of z
  ; must find the value of the operand in combination
  {s} ( ( x => x ) {z} ) = 
  {s} {z}

然后根据s和z的实际定义进行计算。这就是上面显示的等式 (1) 以较短的符号表示的内容。