12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970 |
- (define (mfilter p l)
- (cond ((null? l) '())
- ((p (car l))
- (cons (car l) (mfilter p (cdr l))))
- (else (mfilter p (cdr l)))))
- (define (mfilter p l)
- (cond ((null? l) '())
- ((p (car l))
- (cons (car l) (mfilter p (cdr l))))
- (else (mfilter p (cdr l)))))
- ;; '(define (reverse l)
- ;; (cond ((null? l) '())
- (define (copy l)
- "copies the list l"
- (if (null? l)
- '()
- (cons (car l) (copy (cdr l)))))
- "
- to copy a list l
- we make a fresh cons that contains the head of l, and the copy of the tail of l.
- if l is empty, the copy of l is '()
- ^- fully describing the algorithm. Except we don't know yet whether `copy` works--since we haven't proven *before* that it works/exists, wer're doing that right now. We need to show that the above description is also complete from a coverage standpoint: does that cover all possible lengths of lists?
- Can we show, that the use of `copy` will be less work, or in other words, *converge* towards a trivially solvable( or defined) case?
- The process that's gonna happen will then only encounter cases that we have defined above.
- So by logical deduction we know that the program will always work and give the right result.
- "
- (define (reverse-append l l2)
- "copies the list l in reverse order, but adds l2 on the right
- (y z) (x) -> (z y x)
- () (x) -> (x)
- (z) (y x) -> (z y x)
- l l2
- "
- (if (null? l)
- l2 ;; (begin (repl) l2)
- (reverse-append (rest l) (cons (first l) l2))))
- "
- reverse-append of the empty l is just l2 (nothing to be done).
- reverse-append of a non-empty l is
- the reverse of the rest of l, prepended to the first of l prepended to l2.
- We cover all the cases:
- - empty l
- - non-empty l: since the recursive call is done with a shorter l it will hit the empty l case and is defined for non-empty case, thus,
- reverse-append is defined for *all* lengths of l.
- And it doesn't matter how long l2 is since we only ever add to it.
- "
- (define (reverse l)
- "copies the list l in reverse order"
- (reverse-append l '())))
- ;; (append (reverse l) l2)
- ;; (append-reverse l l2)
|