流和替代模型

Question

我想知道如何使用替换模型来显示无限流的某些内容。例如，假设您有一个流，将 n 放在第 n 个位置，依此类推。我定义如下:

(define all-ints
  (lambda ((n <integer>))
    (stream-cons n (all-ints (+ 1 n)))))

(define integers (all-ints 1))

很明显，这确实达到了预期的目的，但是有人会如何证明它呢？我决定使用归纳法。具体来说，对 k 进行归纳，其中

(last (stream-to-list integers k)) 

提供所提供流的前 k 个值中的最后一个值，在本例中为整数。我在下面定义了流到列表:

(define stream-to-list
  (lambda ((s <stream>) (n <integer>))
    (cond ((or (zero? n) (stream-empty? s)) '())
          (else (cons (stream-first s)
                      (stream-to-list (stream-rest s) (- n 1)))))))

具体而言，我想证明的是 k = (last (stream-to-list integers k)) 对于所有 k > 1 的属性。

获得基本案例相当容易，我可以做到这一点，但是我将如何尽可能彻底地展示“归纳案例”？由于计算第 k+1 个位置的项目需要计算前 k 个项目，因此我不知道如何显示这一点。有人可以给我一些提示吗？

特别是，如果有人可以准确地解释如何使用替换模型解释流，我将非常感激。我知道它们必须与普通学生在流之前学习的其他结构不同，因为它们延迟了计算，我觉得这意味着无法完全评估它们。反过来，我认为，替换模型的 apply eval apply 等模式将不会被遵循。

Answer 1

stream-cons 是一种特殊形式。它相当于将两个参数包装在 lambda 中，使它们成为 thunk。像这样:

(stream-cons n (all-ints (+ 1 n))) ; ==>
(cons (lambda () n) (lambda () (all-ints (+ n 1))))

这些过程是使用词法范围进行的，因此这里 n 是初始值，而当强制尾部时，将在新的词法范围中再次调用 all-ints 给出new n 然后在下一个 stream-cons 中捕获。过程steam-first和stream-rest是这样的:

(define (stream-first s)
  (if (null? (car s))
      '()
      ((car s))))

(define (stream-rest s)
  (if (null? (cdr s))
      '()
      ((cdr s))))

现在所有这些都是半真半假的。事实上，它们不起作用，因为它们会改变(内存)值，因此相同的值不会计算两次，但这对于替换模型来说不是问题，因为无论如何副作用都是禁止的。要了解它是如何真正完成的，请参阅 SICP wizards in action 。请注意，原始流仅延迟尾部，而现代流库延迟头部和尾部。