I. the abstraction principle (Ch. 2) ------------------------------------------ THE ABSTRACTION PRINCIPLE (2) "The phrases of any semantically meaningful syntactic class may be What Named Entity location numeral expression command declaration type structure ------------------------------------------ ------------------------------------------ TERMINOLOGY define pi = 3.14159 define I = V pi I invoke I call I ------------------------------------------ What are the parts of these definitions? ------------------------------------------ SYNTACTIC DOMAINS I \in Identifier D \in Declaration ------------------------------------------ II. Expression abstractions, i.e., functions (2.1) A. abstract syntax ------------------------------------------ CORE IMPERATIVE LANGUAGE WITH NAMES (WhileN) Abstract Syntax: C \in Command P \in Program E \in Expression D \in Declaration L \in Location I \in Identifier N \in Numeral P ::= D ::= C ::= L := E | skip | C1 ; C2 | if E then C1 else C2 fi | while E do C od E ::= N | @L | E1 + E2 | not E | E1 = E2 | L ::= loc i, if i > 0 N ::= n, if n \in Integer Example: ------------------------------------------ What comes next in our description technique? B. type rules 1. type assignments ------------------------------------------ TYPE ASSIGNMENTS Does the following type check? loc 1 := 3 + id def: a *type assignment* is a set of Examples: ------------------------------------------ What information do we need to type check it? How could we model this in Haskell? 2. information flow ------------------------------------------ INFORMATION FLOW IN TYPE RULES I N:int L:int loc I fun id = 4 in loc 1 := id ------------------------------------------ Look at the |- symbols, which way does the information flow on either side of them? 3. actual rules ------------------------------------------ PROGRAM TYPING RULE _________________________________ |- D1 in C: comm DECLARATION TYPING RULES _________________________________ |- fun I = E : {I: }dec _________________________________ \pi |- D1,D2 : _________________________________ \pi |- D1;D2 : where ------------------------------------------ Why use mini-environments as the result of declarations? How could we allow overriding in sequential declarations? how should we revise the rules for expressions? why do we need that because identifiers are expressions? C. semantics (2.2) In the semantics of expressions, how do we find the values of identifiers? ------------------------------------------ ENVIRONMENTS Environment = Set of Examples: OLD SEMANTIC DOMAINS [[C:comm]] \in Store -> Store [[E:t exp]] \in Store -> [[t]] NEW SEMANTIC DOMAINS [[\pi |- C:comm]] \in [[\pi |- E:t exp]] \in ------------------------------------------ How would you model environments in Haskell? ------------------------------------------ SEMANTIC FUNCTIONS For expression: [[ |- E1 + E2: int exp]] e s = [[ |- I: t exp ]] e s = Example calculation: let pi1 = {b:int exp}, e1 = {b = \s -> lookup(1, s)}, s777 = [7,7,7] [[pi1 |- loc 3 := b : comm]] e1 s777 = update([[pi1 |- loc 3 : int loc]] e1, [[pi1 |- b : int exp]] e1 s777, s777) = update(3, = ------------------------------------------ Why don't we get back a new environment? 1. meaning of type attributes (soundness, section 2.3) ------------------------------------------ TYPE ATTRIBUTES theta ::= t exp | int loc | comm | pi dec t ::= int | bool pi ::= {j:theta_j} j \in J, where J finite and J \sub Identifier MEANINGS [[t exp] = Store -> [[t]] [[comm]] = Store -> Store [[bool]] = Bool [[int]] = Int [[int loc]] = Location [[pi dec]] = [[{j:theta_j} ]] = j \in J ------------------------------------------ What would it mean for the type rules to be sound? III. lazy and eager evaluation of abstracts (2.4-2.6) ------------------------------------------ LAZY vs. EAGER EVALUATION OF ABSTRACTS (2.4-2.6) fun F = @loc 1 + 2 in loc 1 := F; loc 2 := F Eager for store [5,4,1], get Lazy for store [5,4,1], get ------------------------------------------ A. lazy evaluation and the copy rule (2.4) ------------------------------------------ WHY LAZY EVALUATION IS BETTER Lazy evaluation allows one to think of an abstract as an Copy rule fun I=E in ... I ... ==> ... ... Example: fun F = @loc 1+2 in loc 1 := F; loc 2 := F ==> ------------------------------------------ 1. formalization ------------------------------------------ FORMALIZING THE COPY RULE Notation: [V1/I1,...,Vn/In]U is simultaneous substitution of the Vi for the Ii. Copy rule for simulataneous declarations D1, D2, ..., Dn define I1 = V1, ..., define In = Vn in U ==> Example: fun two = 2, fun inc1 = @loc 1 + 1 in while not(inc1 = 3) do loc 1 := @loc 1 + two od ==> while not( = 3) do loc 1 := @loc 1 + od ------------------------------------------ How is this like or different from Haskell declarations? How would you formally define simultaneous substitution? what is it for L := E? ------------------------------------------ COPY RULE AND SEQUENTIAL DECLARATIONS Does copy rule work for sequential declarations? fun two = 2; fun inc2 = @loc 1 + two in loc 1 := inc2 ==> loc 1 := ------------------------------------------ How could we fix this? ------------------------------------------ SEQUENTIAL SUBSTITUTION Copy rule for sequential declarations D1; D2; ...; Dn define I1 = V1; ...; define In = Vn in U ==> Example: fun two = 2; fun inc2 = @loc 1 + two in loc 1 := inc2 ==> ------------------------------------------ ------------------------------------------ COPY RULE FOR DECLARATIONS Copy rule for declarations (define I1 = V1, ..., define In = Vn); D ==> Example: fun two = 2; fun inc2 = @loc 1 + two in loc 1 := inc2 ==> ------------------------------------------ What should [Vj/Ij](define I = U) mean? Can we substitute @loc 1 for A in (fun A = @loc 2; fun B = A+1)? 2. debugging Is there anything we could prove about the copy rule that would increase our confidence in it? 3. importance How does the copy rule help us understand the semantics? Is lazy fun declaration any different than a macro define? B. eager evaluation (2.5) Does the copy rule work for eager evaluation? ------------------------------------------ EAGER EVALUATION (2.5) with store [5, 4, 1] fun F = @loc 1+2 in loc 1 := F; loc 2 := F ==> by copy rule fun F = @loc 1+2 in loc 1 := F; loc 2 := F ==> [@loc 1+2/F](loc 1 := F); [@loc 1+2/F](loc 2 := F) ==> [@loc 1+2/F]loc 1 := [@loc 1+2/F](F); [@loc 1+2/F]loc 2 := [@loc 1+2/F](F) ==> loc 1 := @loc 1+2; loc 2 := @loc 1+2 ------------------------------------------ What's an eager evaluation declaration like in C or C++? Might you want to have both kinds, lazy and eager declarations in a language? Why? C. semantics of lazy and eager evaluation (2.6) ------------------------------------------ GENERAL SEMANTICS FOR DECLARATIONS (2.6) Lazy evaluation: [[pi |- define I=U:{I:theta}dec]] e s = [[pi |- invoke I:theta]] e s = Eager evaluation: [[pi |- define I=U:{I:theta}dec]] e s = [[pi |- invoke I:theta]] e s = ------------------------------------------ What's the type of each kind of environment? ------------------------------------------ FOR YOU TO DO Give the semantics of eager evaluation for functions. [[pi |- fun I = E : {I: t exp}dec]] e s = [[pi |- I : t exp]] e s = ------------------------------------------ ------------------------------------------ STRICTNESS CONSIDERATIONS Suppose [[pi |- ohno: bool exp]] e s = _|_ What should the meaning of: [[ |- fun A = ohno in skip: comm]] s ------------------------------------------ How do we get that to happen compositionally? D. summary How would you summarize the advantages and disadvantages of lazy and eager evaluation of declarations (abstracts)? IV. other standard abstractions (2.7) ------------------------------------------ OTHER STANDARD ABSTRACTIONS (2.7) syntax domain define invoke ================================== E fun I = E I C N L Example: ------------------------------------------ What's an alias abstraction like in C++? Is alias abstraction the same as a variable declaration? Does this handle all the syntactic categories? ------------------------------------------ TYPING RULES Pattern: ________________________________ pi |- define I = U:{I:theta} dec pi |- invoke I:theta, if FOR YOU TO DO Give the rules for proc, const, and alias ------------------------------------------ ------------------------------------------ LAZY EVALUATION SEMANTICS [[pi |- proc I = C: {I:comm}dec]]e s = {I = p}, where p(s') = [[pi |- C:comm]]e s' [[pi |- call I:comm]]e s = p(s), where (I = p) \in e [[pi |- const I = N: {I:int}dec]]e s = {I = n}, where n = [[pi |- N:int]]e [[pi |- I:int]]e s = ------------------------------------------ Does it make a difference if we evaluate const abstracts eagerly or lazily? If we have numeral abstracts, do we need eagerly-evaluated function abstracts? Could you do location abstracts? V. recursively defined abstractions (2.8) A. problem Do the typing rules allow recursively-defined abstractions? ------------------------------------------ RECURSION IN ABSTRACTIONS (2.8) Is this legal? proc ohno = call ohno Type proof? |- call ohno: comm, if _________________________________________ |- proc ohno = call ohno:{ohno:comm}dec ------------------------------------------ B. solution ------------------------------------------ FIXING RECURSION IN ABSTRACTIONS Typing rule: |- C: comm __________________________________ pi |- rec-proc I = C : {I:comm}dec Semantics: [[pi |- rec-proc I = C:{I:comm}dec]]e s = ------------------------------------------ can we use the same idea for recursively-defined functions? C. variation of copy rule ------------------------------------------ UNFOLDING RULE FOR RECURSIVE ABSTRACTIONS Recursive syntax binder: rec-proc I = C ==> rec-fun I = E ==> Unfolding Rule: (rec I:comm . C) ==> (rec I:t exp . E) ==> ------------------------------------------ ------------------------------------------ EXAMPLES (alias i = loc 1, alias o = loc 2); rec-proc fact = if @i = 0 then skip else (o := @o * @i; i := @i + -1; call fact) in o := 1; call fact ==> alias i = loc 1, alias o = loc 2, rec-proc fact = if @ = 0 then skip else ( := @ * @ ; := @ + -1; call fact) in loc 2 := 1; call fact ==> alias i = loc 1, alias o = loc 2, proc fact = (rec fact:comm . if @loc 1 = 0 then skip else (loc 2 := @loc 2 * @loc 1; loc 1 := @loc 1 + -1; call fact)) in loc 2 := 1; call fact ==> loc 2 := 1; (rec fact:comm . if @loc 1 = 0 then skip else (loc 2 := @loc 2 * @loc 1; loc 1 := @loc 1 + -1; call fact)) ==> loc 2 := 1; if @loc 1 = 0 then skip else (loc 2 := @loc 2 * @loc 1; loc 1 := @loc 1 + -1; (rec fact:comm . if @loc 1 = 0 then skip else (loc 2 := @loc 2 * @loc 1; loc 1 := @loc 1 + -1; call fact))) ==> ------------------------------------------ VI. Variables (2.9-10) A. declarations (2.9) How is alias abstraction different from a variable declaration in a language like C or C++? What kind of evaluation is used for variable declarations? ------------------------------------------ VARIABLE DECLARATIONS (2.9) Abstract Syntax: D ::= var I | ... C ::= L := E | ... E ::= @L | ... L ::= I Examples: ------------------------------------------ Does the copy rule work for programs like this? B. semantics (2.10) ------------------------------------------ SEMANTICS OF VAR DECLARATIONS (2.10) [[pi |- var I: where and allocate : Store -> (Location x Store) allocate [n1,...,nk] = where init is some arbitrary Integer ------------------------------------------ How does this change the type of the semantic equations for declarations? Do we have to make changes to the other kinds of declarations? any other changes? VII. type structure abstractions (2.11-12) A. separating the parts of a variable declaration (2.11) what's in the semantics that we don't have a way to name yet? ------------------------------------------ TYPE STRUCTURE ABSTRACTIONS (2.11) def: a *type structure* is a Examples: Abstract syntax: D \in Declaration T \in Type-structure D ::= T ::= Example: class N = newint; var x: N, var y: N, var temp: newint; proc swap = (temp := @x; x := @y; y := @temp) in x := 5; y := 4; call swap ------------------------------------------ should x and y be different locations? B. record structures ------------------------------------------ RECORD STRUCTURES Abstract syntax: D \in Declaration C \in Command T \in Type-structure E \in Expression D ::= var I:T | class I=T | D1,D2 | D1;D2 | proc I=C | fun I=E | const I=N T ::= newint | I | Example: class complex = record var x:newint, var y:newint end; var x:complex, var y: complex in ... ------------------------------------------ Are we missing anything in the language? ------------------------------------------ IDENTIFIER EXPRESSIONS Abstract syntax: D \in Declaration C \in Command T \in Type-structure E \in Expression X \in D ::= var I:T | class I=T | D1,D2 | D1;D2 | proc I=C | fun I=E | const I=N T ::= newint | record D end | C ::= L:=E | C1;C2 | if E then C1 else C2 | while E do C od | skip | E ::= N | @L | E1 + E2 | E1 = E2 | not E | L ::= N ::= | n, where n \in Integer X ::= I | Example: var arg: newint; class point = record var x:newint, var y:newint; proc set_x = (x := @arg), proc set_y = (y := @arg), proc north = (x := @x + 1), proc south = (y := @x + -1) end; var p1:point in arg := 0; p1.set_x; arg := 1; p1.set_y; p1.north ------------------------------------------ ------------------------------------------ TYPE ATTRIBUTES (2.12) Attributes: pi ::= {i : theta_i} , J finite i \in J theta ::= t | t exp | comm | pi dec | delta ::= t ::= int | bool Meaning for type structure attributes: [[delta class ]] = ------------------------------------------ What other things can be bound to names? What kinds of classes are there? ------------------------------------------ TYPING RULES theta ::= t | t exp | comm | pi dec | delta | delta class delta ::= int loc | pi FOR YOU TO DO Finish the typing rules below... |- newint : int loc class _________________________________ |- record D end : _________________________________ |- (var I: T) : _________________________________ |- class I = T : |- I : theta, if (I:theta) \in ______________, if |- X.I:theta ------------------------------------------ C. semantics (2.12) ------------------------------------------ SEMANTICS OF TYPE STRUCTURES (2.12) For Declaration: [[pi|-(var I:T):{I:delta}dec]] e s = For Type-structure [[pi|- newint:int loc class]] e s = [[pi|- record D end: pi1 class]] e s = [[pi|- X: delta class]]e s = For Identifier-expr: [[pi|-I:theta]]e = v, where (I=v) \in e [[pi|-X.I:theta]]e = v, where ------------------------------------------ what programming language is this like now? VIII. modules (2.13) What's another kind of "." in C++? How is a module like a record? What syntactic domain haven't we allowed to be named yet? ------------------------------------------ MODULES (2.13) Modules are Abstract syntax: D ::= ... | Example: module LineM = { class Point = record x:newint, y:newint end; var p1:Point, var p2:Point; var arg:newint, var result:newint; proc set_p1_x = p1.x := @arg, proc set_p1_y = p1.y := @arg, proc set_p2_x = p2.x := @arg, proc set_p2_y = p2.y := @arg, proc x_length = result:= p1.x - p2.y }; class Line = record import LineM end; var x:Line, p1:LineM.Point in x.arg := 3; x.set_p1_x; p1.x := 4; LineM.arg := 2 ------------------------------------------ Why is the invocation form a declaration? ------------------------------------------ TYPING RULES FOR MODULES ___________________________________ pi |- module I={D}:{I:pi_1 dec} dec pi |- import I:pi_1 dec, if SEMANTICS FOR MODULES Should it be lazy or eager? [[pi|-module I={D}:{I:pi_1 dec} dec]]e s = [[pi |- import I:pi_1 dec]]e s = ------------------------------------------ Should we give a module declaration lazy or eager evaluation semantics? For which declarations inside a module will it make a difference? ------------------------------------------ DISCUSSION Eager evaluation allows sharing: module S = {var A:newint}; module M = {import S; proc INIT=A:=0}; module N = {import S; proc SUCC=A:=@A+1} in call M.INIT; call N.SUCC Let D be the declaration above. Let piS = {S={A:int loc}dec} piM = {M={A:int loc,INIT:comm}dec} piN = {N={A:int loc,SUCC:comm}dec} piSM = piS U piM pi = piSM U piN [[0 |- D:pi dec]]0 s = {by sample calculation...} ({S={A=l}, M={A=l,INIT=p}, N={A=l,SUCC=p'}}, s1) where (l,s1)= allocate(s) and p s' = [[piS U {A:int loc}|-A:=0:comm ]]({S={A=l},A=l}) s' and p' s' =[[piSM U{A:int loc}|-A:=@A+1 :comm ]]({S={A=l},M={A=l,INIT=p}, A=l}) s' ------------------------------------------ ------------------------------------------ Redeclaration: -- is the following okay? module S = {var A:newint}; module M = {import S; proc INIT=A:=0}; module N = {import S; proc SUCC=A:=@A+1}; import M; import N in call INIT; call SUCC ------------------------------------------ What should the language do? What's the difference between a module and a class? IX. records (2.14) ------------------------------------------ ABSTRACTION = RECORD INTRODUCTION (2.14) The abstraction principle: if pi |- U : theta then allow pi |- (define I=U) : {I:theta}dec Semantics: [[pi |- define I=U:{I:theta}dec]]e s = ({I=f}, s), where f s' = [[pi|-U:theta}]]e s' ------------------------------------------ ------------------------------------------ DISCUSSION ON RECORDS What are the operations on records? ------------------------------------------