Section 2/25

Today:
	quote function
	read function
	Induction on lists
		"non-structural"
		structural
	"trees"

------------------------------------------------------------------------

quote:

' is a short-hand notation for quote.

'x --> (quote x)

'(+ 4 5) --> (quote (+ 4 5))  --> (+ 4 5)


quote takes 1 argument, an expression or symbol, and returns that 
expression or symbol unevaluated.


read:

(read)
After evaluating (read), NOODLE waits for 1 expression/symbol, returns
 that expression as an unevaluated list/symbol

ex:
	? (define x (read)
		waits for input  e.g. (+ 1 2)
		note: you must click the eval button!  Don't use Ctrl E.
	=> x
	? x
	=> (+ 1 2)
	? (head x)
	=> +  <-- this is a symbol, not a function

ex:
	? (define add (read))
		input +
	=> add
	? (add 1 2)
	=> error

------------------------------------------------------------------------

One way to think about lists and recursive list manipulation is using
induction and the substitution model.

How could we go about showing that, for all lists l, (copy l) = l?

But it's a different kind of induction.  
 * We've been doing induction on *integers*. 
 * We can recast our problem as an induction on the *length* of the
   list - that's an integer for sure.

The length of () is 0
The length of (x) is 1
etc.

copy:
(define (copy <function>)
	(method ((l <list>))
		(if (null? l)
		    '()
		    (cons (head l)
			    (copy (tail l))))))


Proof by induction:

INDUCTION ON: n, length of l
STATEMENT: (copy l) = l for any list l of length n

BASE n=0:
  * l must be ()
  * (copy ()) = () by the substitution model.
    
    because (null? ()) ==> #t

INDUCTION: 
  Assume that for any list l of length n, (copy l) = l
  We must show that for any list l' of length n+1, (copy l') = l'.

  Using the substitution model, we know that:
   (null? l') --> #f    because the length of l' is n+1 > 0

  The length (tail l') is length l' - 1, which is n

  So, (copy (tail l')) = (tail l') *by the induction hypothesis* 
                                 [CLEARLY STATED]

  Thus 
   (copy l') = (cons (head l') (copy (tail l')))
             = (cons (head l') (tail l'))          <<< by above reasoning
             = l'                                <<< contract for cons



----------------------------------------------------------------------

However, the induction on (length l) was a bit of a kludge.
  * We don't *need* to do it.

Recall that induction was supposed to be usable on any 
*inductively* *defined* *set*:
  Nat was defined by {0} and succ(x)=x+1

The set of lists is defined by '() and (cons x l) for any
expression x and list l.

The corresponding inductive proofs 
   * INDUCTION ON: a list l
   * STATEMENT: some claim about l
   * BASE CASE: '()
   * INDUCTIVE STEP: prove for all l' that P(l') ==> P(cons s l'), all s
       - Assume that the hypothesis holds for l' 
       - Show that it holds for (cons s l') for every s

This is called *STRUCTURAL* *INDUCTION*:
  - Induct on the *structure* of lists.

----------------------------------------------------------------------

Let's revisit our proof of copy by induction on lists:

INDUCTION ON: l
STATEMENT: (copy l) = l
BASIS:  l = ().
  (copy ()) = () by the substitution model, because (null? ()) = #t

INDUCTION:  Assume (copy l') = l'
            Must show (copy (cons s l')) = (cons s l') for all s.

  (null? (cons s l')) = #f by definition, it contains at least s.

  (copy (cons s l')) = (cons (head (cons s l')) 
				     (copy (tail (cons s l'))))  <<< subst model
              = (cons s (copy l'))                   <<< list contract
              = (cons s l')                          <<< induction 
                                                         hypothesis!
              

----------------------------------------------------------------------

(define (atom? <function>)
	(method ((x <object>))
		(not (id? (object-class x) <pair>))))

(atom? 1) --> #t
(atom? '()) --> #f


(define (count-prim <function>)
	(method ((l <object>))
		(cond
			((null? l) 0)
			((atom? l) 1)
			(else:
				(+ (count-prim (head l))
				   (count-prim (tail l)))))))

(define (tree-map <function>)
	(method ((f <function>) (t <object>))
		(cond 
			((null? t) '())
			((atom? t) (f t))
			(else:
				(cons (tree-map f (head l))
				      (tree-map f (tail l)))))))