Subjects 
--------
     
  * Grammars as set definitions
       - membership proofs
       - concrete and abstract syntax via grammars
       - connection between recursive scheme functions 
         and inductive definitions.
       
  * Evaluation through reduction steps 
    (i.e. substitution-based interpreter from Jan 23 lecture)
															
  * A small dialect of Scheme (as an archetypal functional language)
       - define, cond, let, letrec, lambda, function call,
         define-datatype, cases, begin,
         numbers, booleans, symbols, pairs (and lists), vectors

  * Lexical scope
      - free, binding, and bound occurrences
      - environments
      - let, letrec
      
  * Functions and closures
      - first-order (at top-level) versus higher-order 
        (at expressions)
      - evaluation of `lambda' and function calls
        with an environment

 * Assignment
      - expressed versus denoted values
      - interaction with lexical scope

  * Calling conventions
      - call-by-value
      - call-by-reference
      - call-by-name
      - call-by-need

  * Types and type inference
      - type checking
      - type soundness proof
      - type inference
      - abstract types


Exam Content
------------

In-class, open-book, open-notes.

The exam might...

... ask you to give short answer definitions to some of the terms we've 
    encountered in class.

... ask you to understand a program using "define-datatype" and
    "cases". For example, given:

       (define-datatype
         slithy-tove slithy-tove?
         (wabe-tove ())
         (gyre-tove (st slithy-tove?))
         (gimble-tove (st slithy-tove?)
                      (another slithy-tove?)))

      (define f
		  (lambda (f st)
          (cases slithy-tove st
             (wabe-tove () 0)
             (gyre-tove (inner-st) (+ 1 (f inner-st)))
             (gimble-tove (inner-st another-st) (+ (f inner-st)
                                                   (f another-st))))))

     You should be able to predict the value of

      (f (gyre-tove 
           (gyre-tove 
             (gyre-tove (gimble-tove (wabe-tove) 
                                     (wabe-tove))))))


... ask you about lexical scope. You might have to draw arrows to
    show bindings, or compute bound and free variables.

   Given an expression

     (let ([x 3]
           [y w])
      (let ([x 7]
            [y x])
        (letrec ([f (lambda (z)(f (+ z x)))])
			 (f y))))

   * Draw arrows from bound variable to binding occurrences:

   * List the free vars: w

   * List the bound vars: x y z f

... ask you if two expressions are alpha-equivalent. (i.e. equal up to
    the renaming of *bound* variables).

      (lambda (x) x)
      (lambda (y) y)

      (lambda (x) w)
      (lambda (w) x)

      ((lambda (x) (x y)) z)
      ((lambda (y) (y y)) z)
  
... ask you about the evaluation of a substitution-based interpreter.

    Given the following interpreter (it's a little different from the one 
	 we saw in class):

    (define-datatype expression expression? 
		(lambda-exp (id symbol?)
						(body expression?))
		(app-exp (rator expression?)
					(rand  expression?))
		(lit-exp (datum number?))
		(add-exp (arg1 expression?)
					(arg2 expression?)))

    (define value?
		(lambda (exp)
		  (cases expression exp
			 [lambda-exp (id body) #t]
			 [lit-exp (d) #t]
			 [else #f])))
				 
    (define get-lit
		(lambda (exp)
		  (cases expression exp
			 [lit-exp (i) i]
			 [else (eopl:error 'get-lit "Not a literal expression")])))

    (define eval-one 
		(lambda (exp)
		  (cases expression exp 
			 [lambda-exp (id body) exp]
			 [app-exp (arg1 arg2) 
				 (cond 
				  [(not (value? arg1)) (app-exp (eval-one arg1) arg2)]
				  [(not (value? arg2)) (app-exp arg1 (eval-one arg2))]
				  [else (cases expression arg1
							  [lambda-exp (id body) (subst arg2 id body)]
							  [else (eopl:error 'eval-one
										  "Cannot apply non-function value")])])]
			 [lit-exp (i) exp]
			 [add-exp (arg1 arg2)
				 (cond 
				  [(not (value? arg1)) (app-exp (eval-one arg1) arg2)]
				  [(not (value? arg2)) (app-exp arg1 (eval-one arg2))]
				  [else (lit-exp (+ (get-lit arg1) (get-lit arg2)))])])))

     (define eval-exp
		 (lambda (exp)
			(display (unparse exp))
			(newline)
			(if (value? exp) 
				 exp 
				 (eval-exp (eval-one exp)))))
			 
				  
     * Write the two missing pieces: subst and unparse. (These answers
	    are in the solution to homework 2.)

     * What is printed in the following calls to eval-exp:

     (eval-exp (parse '((lambda (x) (+ x 3)) 4)))

      Answer:
      ((lambda (x) (+ x 3)) 4)
      (+ 4 3)
      7

     (eval-exp (parse '((lambda (y) (y 5))(lambda (x) (+ x 3)))))
              
      Answer:         
      ((lambda (y) (y 5)) (lambda (x) (+ x 3)))
      ((lambda (x) (+ x 3)) 5)
      (+ 5 3)
      8

    * What do we need to change in this interpreter to make it 
      call-by-name instead of call-by-value?

... ask you to rewrite a scheme program as an inductive definition.

    * How can write eval-one (above) as an inductive definition?
      For example, here are some of the rules which state how 
      an expression steps in one step to another expression:

      Functions step to themselves, because they already are values.

      ---------------------------------
      (lambda (x) e) ->1 (lambda (x) e)

       
      There are three cases for application, depending on whether 
      the rator and rand are values or not:

        e1 is not a value
        e2 ->i e2'
      ----------------------
      (e1 e2) ->1 (e1' e2)


        e1 is a value
        e2 ->1  e2'
      -----------------------
      (e1 e2) ->1 (e1 e2')

        e1 is (lambda (x) body)
        e2 is a value
      --------------------------------------
      (e1 e2) ->1 (subst e2 x body)

    What additional rules do we need for literals and addition
    expressions?

... ask about environments and closures at points in an
    evaluation.

    Given the following expression for a call-by-value language
    (denoted values = expressed values):

        (let ([y 2])
           (let ([f (lambda (x)(+ x y))])
             (f 3)))

    * Describe the closure bound to "f" at the
      point where "(f 3)" is the current expression.

          Args: x
          Body: (+ x y)
          Environment: { y = 2 }

    * Describe the environment at the point during evaluation where
      "(+ x y)" is the current expression.

          Environment: { y = 2, x = 3}

... ask you to compute the value of a program using dynamic scoping.
    
    (let ((foo (let ((a 5)) (lambda (x) (- a x)))))
		 (let ((b 3))
         (foo b)))
   
    Result: error because a will not be in the environment
    when foo is called.

... ask you to compute the value of a program using assignment,
    possibly with call-by-reference arguments.
    
    Show the values of the following expressions in a language
    with assignment, sequencing (begin), and both call-by-value and
    call-by-reference(notated with an &) arguments:

        (let ([f (lambda (&x)(begin (set! x (add1 1)) x))])
			(let ([g (lambda (&z) (+ (f z) (f z)))])
			  (let ([y 5])
				 (g y))))

     Result: 13

       (let ([f (lambda (x)(begin (set! x (add1 1)) x))])
			(let ([g (lambda (&z) (+ (f z) (f z)))])
			  (let ([y 5])
				 (g y))))

     Result: 12
     
	  (let ([f (lambda (&x)(begin (set! x (add1 1)) x))])
		 (let ([g (lambda (z) (+ (f z) (f z)))])
			(let ([y 5])
			  (g y))))

     Result: 13

... ask you to compute the value of a program using call-by-value,
    call-by-name, or call-by-need.


    Given the expression

	 (let ([x 0]
			 [f (lambda (y) (set! y (+ y y)))])
		(let ([z (begin
					  (set! x (add1 x))
					  x)])
		  (begin
			 (f z)
			 z)))

    What does the expression produce in the following configurations
    of the interpreter?

     1. All procedure arguments are call-by-value.
       
        Result: 1. Right-hand side of the `z' binding increments
                x once and sets z's result once and for all.

     2. All procedure arguments and let bindings are call-by-name.

        Result: 3. z is used three times, so it's value is
                incremented three times.

     3. All procedure arguments and let bindings are call-by-need.

        Result: 1. z is used three times, but its value is computed
                once and for all on the first use.

... ask you to find and prove the type of an expression.

    Find and prove the type of the following expression:

      (lambda (num x)
         (lambda ((num -> bool) b)
			  (if (b x) x 10)))

    The type is (num -> ((num -> bool) -> num)). Here is the proof:


     E1 |- b : (num -> bool)  E1 |- x : num
     --------------------------------------
              E1 |- (b x) : bool            E1 |- x : num   E1 |- 10 : num
     ---------------------------------------------------------------------
      E1 = { x : num, b : (num -> bool) } |- (if (b x) x 10) : num
     ---------------------------------------------------------------------
      {x : num} |- (lambda ((num -> bool) b) (if (b x) x 10))
                   : ((num -> bool) -> num)
     ---------------------------------------------------------------------
       {} |- (lambda (num x)
				    (lambda ((num -> bool) b)
						(if (b x) x 10)))
             : (num -> ((num -> bool) -> num))

... ask you to infer a type expression so that a larger expression has
    a type, as in Homework 6.

    What must T_1 and T_2 be in the following expression, so that it
    has a type?

      (lambda (T_2 x)
		  (lambda (T_1 b)
			 (if (b x) x 10)))

    T_2 = int
    T_1 = (int -> bool)

    T_2 is int because x must have the same type as 10. T_1 is (int ->
    bool) because b is applied to x, x has type int, and the
    application result is used as a test result.


... ask you to extend the type safety proof to some new forms of
    expressions, in the style of Homework 6.

... ask you questions about the above topics in a different form than the 
    ones given in this review sheet.