流和替换模型

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>1，k＝（last（列出整数k的流））的性质。

获取基本情况相当容易，我可以做到，但我该如何尽可能彻底地展示"归纳情况"？由于计算第k+1个点中的项目需要计算之前的k个项目，我不知道如何显示这一点。有人能给我一些提示吗？

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

Answer 1

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

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

这些过程是用词法作用域进行的，因此这里n是初始值，而当强制尾部时，将在新的词法作用域中再次调用all-ints，给出新的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向导的操作。请注意，原始流只延迟尾部，而现代流库同时延迟头部和尾部。