3/2 Monday Section

Our Data Abstraction:

We're going to have the following TYPES of expressions:
[CONSTANTS]:   
Type: <const>  
Predicate: constant?
  
>> represented concretely as <number>s -- this costs us flexibility,
     no abstraction, but means we can directly use Dylan arithmetic ops

[VARIABLES]:  
Type: <var>  
Predicate: variable?  
(same-variable? v1 v2)

[SUM]:   
Type: <sum>  
Predicate: sum?  
Accessors:  addend, augend
Constructor: make-sum  
Contract:
  If x = (make-sum a b) then (addend x) + (augend x) = a+b
  Note: this contract allows sums to be manipulated as long as
        maintain mathematical equality to summation.

[PRODUCT]: (* a b)
Type: <prod>  
Predicate: product?  
Accessors:  multiplier, multiplicand
Constructor: make-prod  
Contract:  
If x = (make-prod a b) then (multiplier x) * (multiplicand x) = a*b  

[EXPONENT]: (^ a b)  
Type: <expt>  
Predicate: exponent?  
Accessors: base, power
Constructor: make-expt   
Contract:
  If x = (make-expt a b) then (base x) ^ (power x) = a^b



Take a look at how one of the underlying types is implemented

(define-class <sum> (<object>) (addend <object>) (augend <object>))

(define (make-sum <function>)  
  (method ((a1 <object>) (a2 <object>))
    (make <sum> addend: a1 augend: a2)))

(define (sum? <function>)
  (method ((e <object>))    
          (instance? e <sum>)))

(define (addend <function>)
  (method ((s <sum>))    
          (get-slot addend: s)))

(define (augend <function>)
  (method ((s <sum>))   
          (get-slot augend: s)))

New special form define-class, three new procedures, make, instance? and
get-slot (define-class NAME SUPERS slot1 ... slotn)defines a new CLASS
where sloti is (SLOTNAME TYPE [INITVAL])

Note: SUPERS is for now always (<object>), used for building a type hierarchy
(make CLASS [KEY1: VAL1 ... KEYN: VALN])
creates an INSTANCE of the named CLASS (note, must be user defined class)

The keywords optionally specify slot names and the initial values to
use for each named slot.


(instance? VAL TYPE)

tests whether VAL is an instance of the given TYPE

(get-slot SLOT: VAL)
returns the value of the named SLOT: for the given instance

INDUCTION to prove DERIV works

Now, let's look at proving that this procedure works correctly:
SHOW: (deriv e v) = de/dvby 
induction on ... depth of expressions.

BASE CASE: depth of e is zero  
* e is a number    (deriv e v) = 0 = de/dv
* e is a variable    
 * e is v      (deriv e v) = 1 = de/dv
 * e is some other variable,      (deriv e v) = 0 = de/dvINDUCTION CASE:
 
ASSUME (deriv e v) = de/dv for any expression e of depth <= n.
SHOW (deriv f v) = df/dv for f of depth n+1There are three cases
(1) f is the sum of f1 and f2    
(deriv f v)   
   = (make-sum (deriv (addend f) v)
               (deriv (augend f) v))  <<< substitution
   = (make-sum (deriv f1 v)           <<< Contract               
               (deriv f2 v))
   = (make-sum df1/dv df2/dv)         <<< by IH
   = df1/dv + df2/dv                  <<< by rules for sums   = df/dv


(2) f is the product of f1 and f2      
(deriv f v)
  = (make-sum (make-prod f1 (deriv f2 v))
              (make-prod f2 (deriv f1 v)))  
  = (make-sum (make-prod f1 df2/dv)
              (make-prod f2 df1/dv))  
  = f1 df2/dv + f2 df1/dv  = df/dv

(3) f is f1 to the f2, where f2 is a number >= 0   
(deriv f v)  
  = (make-prod
     (make-prod f2      
                (make-expt f1 (- f2 1)))     
     (deriv f1 v))
  = f2 * (f1^(f2-1)) * df1/dv  = df/dv