I. reasoning about procedures (4.1) (omit)
------------------------------------------
    REASONING ABOUT FUNCTIONAL PROGRAMS

         (define caadr
           (lambda (ls)
             (car (car (cdr ls)))))


  (caadr (list (list 1 2) (list 3 4)))

=>

  ((lambda (ls)
    (car (car (cdr ls))))
   (list (list 1 2) (list 3 4)))

=>

  (car (car
    (cdr (list (list 1 2) (list 3 4)))))
------------------------------------------
	How did we proceed?
------------------------------------------
	  FOR YOU TO DO

	(define square-first
          (lambda (n1 n2)
            (* n1 n1)))

Complete the following simplification:

  (square-first (+ 5 3)
                (/ (* 10567 (+ 93 5)) 7))

=>




------------------------------------------
	Is it better to evaluate the arguments first?
	What strategy does Scheme use?
------------------------------------------
    EVALUATING ARGUMENTS FIRST

          (define caadr
            (lambda (ls)
              (car (car (cdr ls)))))


  (caadr (list (list 1 2) (list 3 4)))

=>

  ((lambda (ls)
    (car (car (cdr ls))))
   (list (list 1 2) (list 3 4)))

=>

  ((lambda (ls)
    (car (car (cdr ls))))
   '((1 2) (3 4)))

=>

  (car (car (cdr '((1 2) (3 4)))))
------------------------------------------
------------------------------------------
	      REDUCTION RULES
      AS A GENERAL SEMANTIC MECHANISM
          (OPERATIONAL SEMANTICS)

1. for procedures

  (define c+
    (lambda (n)
      (lambda (m)
        (+ n m))))

  ((c+ 4) 3)
=> ((lambda (m) (+ 4 m)) 3)
=> (+ 4 3)
=> 7

2. for syntactic sugars

   (let ((x 3)
         (add5 (c+ 5)))
     (add5 x))
=> ((lambda (x add5) (add5 x))
    3
    (c+ 5))
=> ((lambda (x add5) (add5 x))
    3
    (lambda (m) (+ 5 m)))
=>

------------------------------------------
	How is this kind of semantics like an interpreter?
	What happens if the program being reduced is an infinite loop?
II. beta conversion (4.2) (omit)
	What features of other languages are captured by lambda calculus?
 A. beta rule
------------------------------------------
	   THE BETA RULE (4.2)

Syntax of lambda calculus with constants

<exp> ::= <number> | <varref>
	| (lambda (<var>) <exp>)
        | (<exp> <exp>)


Beta rule:



Examples:

  ((lambda (x) 1) 2) = 
  ((lambda (z) z) 2) = 
  ((lambda (z) y) 2) = 

  ((lambda (x) (x (x 2))) f) = 

  ((lambda (f)
     (lambda (g)
       (lambda (x) (f (g x))))) car)
  =
------------------------------------------
------------------------------------------
	   FOR YOU TO DO (IN PAIRS)

Use beta reduction to simplify,
if possible, the following.
Show all steps.

a. ((lambda (x) x) (lambda (x) x))




b. (((lambda (x)
      (lambda (y) (x y)))
     add1) 4)




c. ((lambda (x) (x x)) (lambda (x) (x x)))




------------------------------------------
 B. conversion and reduction
------------------------------------------
	CONVERSION AND REDUCTION

conversion
	((lambda (x) E) M) = E[M/x]

e.g., ((lambda (x) (f x)) 3) = (f 3)

reduction
	((lambda (x) E) M) => E[M/x]

e.g., ((lambda (x) ((lambda (y) y) x)) f)
      => ((lambda (y) y) f)
      => 

anti-reduction
	E[M/x] <= ((lambda (x) E) M)

e.g.,
      ((ccons (car (cdr ls1)))
       (car (cdr ls2)))
      <= ((lambda (cadr)
            ((ccons (cadr ls1))
             (cadr ls2)))

------------------------------------------
	What would that last expression be like using a let?
------------------------------------------
	UTILITY OF BETA REDUCTION

Transforming procedural rep to record rep:

(define seq-repeat
  ; TYPE: (-> (number) sequence)
  (lambda (num)
    (lambda (n) num)))

(define seq-generator
  ; TYPE: (-> ((-> (number) number))
  ;           sequence)
  (lambda (f)
    (lambda (n) (f n))))

(define seq-nth
  ; TYPE: (-> (sequence) number)
  (lambda (seq n)
    (seq n)))

becomes:

(define-record repeated-seq (num))
(define-record generated-seq (f))

(define seq-nth
  ; TYPE: (-> (sequence) number)
  (lambda (seq n)
    (variant-case seq
      (seq-repeat (num)
         ((lambda (n) num) n))
      (seq-generator (f)
         ((lambda (n) (f n)) n)))))

	   FOR YOU TO DO 
Beta-reduce each case of the variant-case
------------------------------------------
	Does that give the original code?
 C. eta conversion (p. 107)
------------------------------------------
	   ETA CONVERSION IDEA

  ((lambda (n) (f n)) y)
=





So:

(define seq-generator
  ; TYPE: (-> ((-> (number) number))
  ;           sequence)
  (lambda (f)
    (lambda (n) (f n))))
=



Similarly:

  ((lambda (f)
      (lambda (n) (f n)))
   g)
= 





------------------------------------------
	Does beta reduction mean both sides are equal?
	When are two functions equal?
	So are f and (lambda (n) (f n)) equal?
------------------------------------------
           FOR YOU TO DO

Reduce the following:

   (lambda (sym val ff)
     (make-extended-ff sym val ff))


Simplify the following code:

(define lambda->formal
  ; TYPE: (-> (exp) exp)
  (lambda (exp)
    (caadr exp)))
------------------------------------------
	Is it possible to make this simplification in C++?
------------------------------------------
	   ETA CONVERSION RULE

conversion:
   if x is not free in E, then
	(lambda (x) (E x)) = E


reduction:
   if x is not free in E, then
	(lambda (x) (E x)) => E


		TERMS

redex, beta-redex, eta-redex

	((lambda (x) (f x)) 3)

------------------------------------------
	What if x is free in E?
	What would eta-anti-reduction (aka eta-expansion) look like?