I. the parameterization and correspondence principles (Schmidt 3)
 A. principles
------------------------------------------
  PARAMTERIZATION AND CORRESPONDENCE
        PRINCIPLES (SCHMIDT 3)

Parameterization:

  Phrases from any syntactic class
  should be 


Correspondence:

  Abstraction and parameterization
  mechanisms should 




Lambda abstraction:
  Allow prameterized phrases,
  i.e., lambda abstractions.

------------------------------------------
	    Why is correspondence a good thing?
------------------------------------------
  TYPE RULES FOR PARAMETERIZATION (3.10)

Syntax (schematic):

 D ::= ... | define I1 (I2: theta1) = U
 U ::= ... | invoke I(V)
 V ::= ... | I

Type attributes:

  theta ::= ... | 

Typing rules:










------------------------------------------
------------------------------------------
  TYPE RULES FOR LAMBDA ABSTRACTION

Syntax:

 D ::= ... | define I = A
 A ::= \I:theta . U
 U ::= ... | invoke I(V)
 v ::= I

Typing rules:






------------------------------------------
------------------------------------------
   PARAMETERIZATION SEMANTICS OVERVIEW

kind of              semantics
parameter      lazy           eager

expression

location

numeral

command

declaration

type struct.		        

function,		        
procedure,...
------------------------------------------
	What do we mean by a lazy or eager semantics for parameters?
	Why should function parameters be lazily evaluated?
II. Expression parameters (Schmidt 3.1-3.3)
 A. syntax
------------------------------------------
 EXPRESSION PARAMETERS TO PROCEDURES (3.1)

Syntax:

 D ::= proc
 C ::= call I(E)

Examples:

  var v: newint;
  proc p(i:intexp) = (v:=i; v:=i)
  in v := 1; call P(@v+1)




------------------------------------------
	What is the type attribute of I1 in the type rule?
 B. semantics (3.2)
------------------------------------------
	EAGER SEMANTICS (3.2)

  [[ tau exp -> comm]] = 


  [[




  [[




  [[



------------------------------------------
	Does this satisfy the correspondence principle?
	What if the actual parameter loops?
------------------------------------------
	LAZY SEMANTICS

  [[ tau exp -> comm]] =



  [[




  [[



  [[


------------------------------------------
	How does this work?
	What would be another way to define this?
III. type equivalence (3.5)
------------------------------------------
	TYPE EQUIVALENCE (3.5)

How to check actual's type vs. formals?

Example:

  class Car = record var age: newint,
                     var weight: newint
              end;
  class Person = record var age: newint,
                        var weight: newint
                 end;
  class Ship = Car;
  var c: Car;
  var p: Person;
  var s: Ship;
  var c2: record var age: newint,
                     var weight: newint
          end;
  var p2: record var age: newint,
                     var weight: newint
          end;

  proc con(r: {age:intloc, weight:intloc})
    = ...

------------------------------------------
	Which of the variables (if any) can be passed to con?
------------------------------------------
	NOTIONS OF TYPE EQUIVALENCE

structural:


occurrence (name):



------------------------------------------
	What kinds of parameter types are useful with
		occurrence equivalence?