CODEWITHSUNDEEP
streamschemeracket
farid99
farid99

Reputation: 712

Streams and the substitution model

I am wondering how the substitution model can be used to show certain things about infinite streams. For example, say you have a stream that puts n in the nth spot and so on inductively. I define it below:

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

(define integers (all-ints 1))

It is pretty clear that this does what it is supposed to, but how would someone go about proving it? I decided to use induction. Specifically, induction on k where

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

provides the last value of the first k values of the stream provided, in this case integers. I define stream-to-list below:

(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)))))))

What I'd like to prove, specifically, is the property that k = (last (stream-to-list integers k)) for all k > 1.

Getting the base case is fairly easy and I can do that, but how would I go about showing the "inductive case" as thoroughly as possible? Since computing the item in the k+1th spot requires that the previous k items also be computed, I don't know how this could be shown. Could someone give me some hints?

In particular, if someone could explain how, exactly, streams are interpreted using the substitution model, I'd really appreciate it. I know they have to be different from the other constructs a regular student would have learned before streams, because they delay computation and I feel like that means they can't be evaluated completely. In turn this would man, I think, the substitution model's apply eval apply etc pattern would not be followed.

Upvotes: 2

Views: 170

Answers (1)

Sylwester
Sylwester

Reputation: 48745

stream-cons is a special form. It equalent to wrapping both arguments in lambdas, making them thunks. like this:

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

These procedures are made with the lexical scopes so here n is the initial value while when forcing the tail would call all-ints again in a new lexical scope giving a new n that is then captured in the the next stream-cons. The procedures steam-first and stream-rest are something like this:

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

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

Now all of this are half truths. The fact is they are not functional since they mutates (memoize) the value so the same value is not computed twice, but this is not a problem for the substitution model since side effects are off limits anyway. To get a feel for how it's really done see the SICP wizards in action. Notice that the original streams only delayed the tail while modern stream libraries delay both head and tail.

Upvotes: 2

Related Questions