SIGPLwinterschool2012

1994

1992 2001 2008

2002

Semantics Engineering with PLT Redex Matthias Felleisen, Robert Bruce Findler and Matthew Flatt 2009 Text

David A. Schmidt

EXPRESSION E ::= N ( E1 O E2 ) OPERATOR O ::= + - NUMERAL N ::= D D N DIGIT D ::= 0 1 2 3 4 5 6 7 8 9 : ((2 + 1) - (3-4)) ETREE ::= NUM [ OP, ETREE, ETREE ] OP ::= + - NUM ::= <string of digits> : ["-", ["+", "2", "1"], ["-", "3", "4"]]

def interpetree(t): # pre: t == ETREE # where ETREE ::= NUM [ OP, ETREE, ETREE ] # OP ::= + - # NUM ::= <string of digits> # post: ans == t ( ) # returns: ans if isinstance(t, str): if t.isdigit(): ans = int(t) else: raise Exception else: if t[0] == + : ans = interpetree(t[1]) + interpetree(t[2]) elif t[0] == - : ans = interpetree(t[1]) - interpetree(t[2]) else: print( interpetree error:,t, is illegal. ) raise Exception return ans

interpetree( ["-", ["+", "2", "1"], ["-", "3", "4"]]) => ans = interpetree(["+", "2", "1"]) - interpetree(["-", "3", "4"]) => ans = interpetree("2") + interpetree("1") => ans = 2 = 2 + interpetree("1") => ans = 1 = 2 + 1 = 3 = 3 - interpetree(["-", "3", "4"]) => ans = interpetree("3") - interpetree("4") => ans = 3 = 3 - interpetree("4") = 3 - => ans = 4 = 3-4 = -1 = 3 - (-1) = 4 = 4

Program P ::= CL CommandList CL ::= C C ; CL Command C ::= I = E print I while E : CL end Expression E ::= N I ( E O E ) Operator O ::= + - Numeral N ::= <strings of digits> Variable I := <strings> PTREE ::= CLIST CLIST ::= [ CTREE+ ] CTREE ::= ["=", ID, ETREE] ["print", ID] ["while", ETREE, CLIST] ETREE ::= NUM ID [OP, ETREE, ETREE]

x = 3 ; while x : x = x - 1 end ; print x [["=", "x", "3"], ["while", "x", [["=", "x", ["-", "x", "1"]]]], ["print", "x"] ]

x = 3 ; while x : x = x - 1 end ; print x program [["=", "x", "3"], ["while", "x", [["=", "x", ["-", "x", "1"]]]], ["print", "x"] ] interpptree interpctree interpetree namespace x 3 def interpptree(program): # pre: program == PTREE ::= CLIST # CLIST ::= [ CTREE+ ] # post: namespace == program ( ) global namespace namespace = {} # for command in program: interpctree(command) print( final namespace =, namespace)

def interpctree(c): # pre: c == CTREE ::= [ =, ID, ETREE] [ print, ID] [ while, ETREE, CLIST] # post: namespace == c ( ) op = c[0] if op == = : var = c[1] expr = c[2] exprval = interpetree(expr) namespace[var] = exprval elif op == print : var = c[1] if var in namespace: val = namespace[var] print(val) else: crash( variable name undefined ) elif op == while : expr = c[1] body = c[2] while (interpetree(expr)!= 0) interpclist(body) else: crash( invalid command )

def interpetree(e): # pre: e == ETREE ::= NUM ID [OP, ETREE, ETREE] OP ::= + - # post: val == e ( ) # returns: val if isinstance(e,str) and e.isdigit(): val = int(e) elif isinstance(e,str) and len(e)>0 and e[0].isalpha(): if e in namespace: val = namespace[e] else: crash( variable name undefined ) else: op = e[0] val1 = interpetree(e[1]) val2 = interpetree(e[2]) if op == + : val = val1 + val2 elif op == - : val = val1 - val2 else: crash( illegal arithmetic operator ) return val

interpptree([["=", "x", "3"], ["while", "x", [["=", "x", ["-", "x", "1"]]]], ["print", "x"] ])

Program P ::= CL CommandList CL ::= C C ; CL Command C ::= L = E while E : CL end print L Expression E ::= N L &L ( E + E ) LefthandSide L ::= I *L Numeral N ::= <strings of digits> Variable I ::= <strings> PTREE ::= CLIST CLIST ::= [ CTREE+ ] CTREE ::= ["=", LTREE, ETREE] ["while", ETREE, CLIST] ["print", LTREE] ETREE ::= NUM LTREE [ &, LTREE] [ +, ETREE, ETREE] LTREE ::= ID [ *, LTREE]

y = 5; z = 0; x = (6 + y) [["=", "y", "5"], ["=", "z", "0"], ["=", "x", [ +, 6, y ]] ] program interpptree interpctree interpetree interpltree namespace 0 1 2... memory

y = 5; z = 0; x = (6 + y) [["=", "y", "5"], ["=", "z", "0"], ["=", "x", [ +, 6, y ]] ] program interpptree interpctree interpetree interpltree y 0 namespace 0 1 2 5... memory

y = 5; z = 0; x = (6 + y) [["=", "y", "5"], ["=", "z", "0"], ["=", "x", [ +, 6, y ]] ] program interpptree interpctree interpetree interpltree y 0 z 1 namespace 0 1 2 5 0... memory

y = 5; z = 0; x = (6 + y) [["=", "y", "5"], ["=", "z", "0"], ["=", "x", [ +, 6, y ]] ] program interpptree interpctree interpetree interpltree y 0 z 1 x 2 namespace 0 1 2 5 0 11... memory

y = 5; z = &y; x = (6 + *z) program [["=", "y", "5"], ["=", "z", ["&", "y"]], ["=", "x", [ +, 6, [ *, z ]]] ] interpptree interpctree interpetree interpltree namespace 0 1 2... memory

y = 5; z = &y; x = (6 + *z) program [["=", "y", "5"], ["=", "z", ["&", "y"]], ["=", "x", [ +, 6, [ *, z ]]] ] interpptree interpctree interpetree interpltree y 0 namespace 0 1 2 5... memory

y = 5; z = &y; x = (6 + *z) program [["=", "y", "5"], ["=", "z", ["&", "y"]], ["=", "x", [ +, 6, [ *, z ]]] ] interpptree interpctree interpetree interpltree y 0 z 1 namespace 0 1 2 5 0... memory

y = 5; z = &y; x = (6 + *z) program [["=", "y", "5"], ["=", "z", ["&", "y"]], ["=", "x", [ +, 6, [ *, z ]]] ] interpptree interpctree interpetree interpltree y 0 z 1 x 2 namespace 0 1 2 5 0 11... memory

memory = [] # memory = [5,0,11] namespace = {} # namespace = { y =0, z =1, x =2} def interpc(program): # pre: program == PTREE ::= [ CTREE+ ] # post: memory == program ( ) global namespace, memory namespace = {} memory = [] for command in program: interpctree(command) print( final namespace =, namespace) print( final memory =, memory)

def interpltree(x): # pre: x == LTREE ::= ID [ *, LTREE] # post: loc == x # returns: loc if isinstance(x,str): if x in namespace: loc = namespace[x] else: memory.append( err ) namespace[x] = len(memory) - 1 loc = namespace[x] else: y = interpltree(x[1]) loc = memory[y] return loc

def interpctree(c): # pre: c == CTREE ::= [ =, LTREE, ETREE] [ while, ETREE, CLIST] [ print, LTREE] # post: memory == c ( ) op = c[0] if op == = : lval = interpltree(c[1]) rval = interpetree(c[2]) memory[lval] = rval elif op == while : expr = c[1] body = c[2] while (interpetree(expr)!= 0) interpclist(body) elif op == print : print(interpltree(c[1])) else: crash( invalid command )

def interpetree(e): # pre: e == ETREE ::= NUM LTREE [ &, LTREE] [ +, ETREE, ETREE] # post: val == e ( ) # returns: val if isinstance(e,str) and e.isdigit(): val = int(e) elif isinstance(e,list) and e[0] == + :: val1 = interpetree(e[1]) val2 = interpetree(e[2]) val = val1 + val2 elif isinstance(e,list) and e[0] == & : val = interpltree(e[1]) else: x = interpltree(e) val = memory[x] return val

declare y : int; declare z : *int; y = 5; z = &y; declare x : int; x = (6 + *z) declare x : int; x = 0; declare y : int; y = (6 + &x) declare x : int; x = 0; *x = 999

Program CommandList Command P ::= CL CL ::= C C ; CL C ::= L = E while E : CL end print L declare I : T Type T ::= int *T Expression E ::= N L &L ( E1 + E2 ) LefthandSide L ::= I *L Numeral Variable N ::= <strings of digits> I ::= <strings> PTREE ::= CLIST CLIST ::= [ CTREE+ ] CTREE ::= ["=", LTREE, ETREE] ["while", ETREE, CLIST] ["print", LTREE] [ dec, ID, TYPE] TYPE ::= [ ptr *, int ] ETREE ::= NUM LTREE [ &, LTREE] [ +, ETREE, ETREE] LTREE ::= ID [ *, LTREE]

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 z [ ptr, int ], 1 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 z [ ptr, int ], 1 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2 5... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 z [ ptr, int ], 1 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2 5 0... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 z [ ptr, int ], 1 x [ int ], 2 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2 5 0... memory

declare y : int; declare z : *int; y = 5; z = &y; declare x; x = (6 + *z) program interpptree interpctree interpetree interpltree y [ int ], 0 z [ ptr, int ], 1 x [ int ], 2 namespace [[ dec, y, [ int ]], [ dec, z, [ ptr, int ]], ["=", "y", "5"], ["=", "z", ["&", "y"]], [ dec, x, [ int ]], ["=", "x", [ +, 6, [ *, z ]]] ] 0 1 2 5 0 11... memory

memory = [] # memory = [5,0,11] namespace = {} # namespace = { y =([ int ],0), # z =([ ptr, int ],1), # x =([ int ],2)} def interpct(program): # pre: program == PTREE ::= [ CTREE+ ] # post: memory == program ( ) global namespace, memory namespace = {} memory = [] for command in program: interpctree(command) print( final namespace =, namespace) print( final memory =, memory)

def interpltree(x): # pre: x == LTREE ::= ID [ *, LTREE] # post: ans == x (, ) # returns: ans if isinstance(x,str): if x in namespace: ans = namespace[x] else: crash( variable,x, undeclared ) else: type, loc = interpltree(x[1]) if type[0] == ptr : ans = (type[1:],memory[loc]) else: crash( variable not a pointer ) return ans

def interpctree(c): # pre: c == CTREE ::= [ =, LTREE, ETREE] [ while, ETREE, CLIST] [ print, LTREE] [ dec, ID, TYPE] TYPE ::= [ ptr *, int ] # post: memory == c ( ) op = c[0] if op == = : type1,lval = interpltree(c[1]) type2,rval = interpetree(c[2]) if type1 == type2: memory[lval] = rval else: crash( incompatible types for assignment ) elif op == while : expr = c[1] body = c[2] type,val = interpetree(expr) while (val!= 0) interpclist(body) type,val = interpetree(expr) elif op == print : type,num = interpltree(c[1]) print(num) elif op == dec : x = c[1] if x in namespace: crash( variable,x, redeclared ) else: memory.append( err ) namespace[x] = (c[2],len(memory)-1) else: crash( invalid command )

def interpetree(e): # pre: e == ETREE ::= NUM LTREE [ &, LTREE] [ +, ETREE, ETREE] # post: ans == e (, ) # returns: ans if isinstance(e,str) and e.isdigit(): ans = ([ int ],int(e)) elif isinstance(e,list) and e[0] == + :: type1,val1 = interpetree(e[1]) type2,val2 = interpetree(e[2]) if type1 == [ int ] and type2 == [ int ]: ans = ([ int ],val1 + val2) elif isinstance(e,list) and e[0] == & : type,val = interpltree(e[1]) ans = ([ ptr ]+type,val) else: type,loc = interpltree(e) ans = (type,memory[loc]) return ans

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α heap

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α x 7 heap

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α x 7 y β heap β f g

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α x 7 y β heap β f 7 g

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α x 7 y β heap β f 7 g ɣ ɣ r

x = 7; y = new {f, g}; y.f = x; y.g = new {r}; y.g.r = y.f program interpptree interpctree interpetree interpltree α namespace α x 7 y β heap β f 7 g ɣ ɣ r 7

Program CommandList Command Expression LefthandSide FieldNames Numeral Variable P ::= CL CL ::= C C ; CL C ::= L = E if E : CL1 else CL2 end print L E ::= N L ( E + E ) new { F } L ::= I L. I F ::= I I, F N ::= <strings of digits> I ::= <strings> PTREE ::= CLIST CLIST ::= [ CTREE+ ] CTREE ::= ["=", LTREE, ETREE] ["if", ETREE, CLIST, CLIST] ["print", LTREE] ETREE ::= NUM [ deref, LTREE] [ +, ETREE, ETREE] [ new, OBJ] LTREE ::= [ ID+ ] OBJ ::= [ ID+ ] a = new { f,g }; a.f = 3; a.g = (1 + a.f) [ ["=", ["a"], ["new", ["f","g"]]], ["=", ["a", "f"], "3"], ["=", ["a", "g"], ["+", "1", ["deref", ["a", "f"]]]] ]

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 namespace 0

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 namespace 0

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 y 1 namespace 0 1 f g

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 y 1 namespace 0 1 f g 5

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 y 1 z 2 namespace 0 1 f g 5 2 r

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 y 1 z 2 namespace 0 1 f g 5 2 r 12

heap = {} # { ( = )+ } heap_count = 0 # x = 7; y = new {f,g}; y.g = 5; z = new {r}; z.r = (y.g + x) heap 0 x 7 y 1 z 2 namespace 0 heap = { "0": {"x":7, "y":"1", "z":"2"}, "1": {"f":"nil", "g":5}, "2": {"r":12} } heap_count = 3 1 2 f g 5 r 12

def cleartheheap(): global heap_count, heap heap_count = 0 heap = {} def allocatens(): global heap_count newloc = str(heap_count) heap[newloc] = {} heap_count = heap_count + 1 return newloc def dereference(lval): ans = nil loc,f = lval if isinstance(loc,str) and loc.isdigit(): ans = heap[loc][f] else: crash( dereference error: lval =,str(lval)) return ans def store(lval,rval): loc, qual = lval if isinstance(loc,str) and loc.isdigit(): heap[loc][qual] = rval else: crash( store error: lval =,str(lval))

def interpct(program): # pre: program == PTREE ::= [ CTREE+ ] # post: memory == program ( ) global namespace, heap cleartheheap() namespace = allocatens() for command in program: interpctree(command) print( final namespace =,namespace) print( final heap =,heap)

def interpctree(c): # pre: c == CTREE ::= [ =, LTREE, ETREE] [ if, ETREE, CLIST, CLIST] [ print, LTREE] # post: heap == c ( ) op = c[0] if op == = : lval = interpltree(c[1]) rval = interpetree(c[2]) store(lval,rval) elif op == if : test = interpetree(c[1]) if test!= 0: interpclist(c[2]) else: interpclist(c[3]) elif op == print : val = dereference(interpltree(c[1])) print(val) else: crash( invalid command )

def interpetree(e): # pre: e == ETREE ::= NUM [ deref, LTREE] [ +, ETREE, ETREE] [ new OBJ] OBJ ::= [ ID+ ] # post: ans == or or nil (+ ) # returns: ans ans = nil if isinstance(e,str) and e.isdigit(): ans = int(e) elif e[0] == + :: val1 = interpetree(e[1]) val2 = interpetree(e[2]) if isinstance(val1,int) and isinstance(val2,int): ans = val1 + val2 else: crash( addition error - non-int value used ) elif e[0] == deref : ans = dereference(interpltree(e[1])) elif e[0] == new : handle = allocatens() fields = e[1] for f in fields: store((handle,f), nil ) ans = handle else: crash( invalid expression ) return ans

def interpltree(x): # pre: x == LTREE ::= [ ID+ ] # post: lval == (, ) # returns: ans lval = (namespace,x[0]) indexlist = x[1:] while indexlist!= []: fieldname = indexlist[0] indexlist = indexlist[1:] handle = dereference(lval) lval = (handle, fieldname) return lval

x y.f y.g.h ["x"] ["y", "f"] ["y", "g", h ] ( 0, x ) ( 1, f ) crash! heap namespace 0 x 7 y 1 z 2 0 1 f g 5 2 r 12

Peter J. Landin, "Correspondence between ALGOL 60 and Church's Lambda-notation: part I & II". Communications of the ACM, (February 1965).

Program Declaration Command Expression Numeral Variable P ::= D ; C D ::= int I D1 ; D2 C ::= I = E C1 ; C2 while E : C print E E ::= N E1 + E2 E1 == E2 @I N ::= <strings of digits> I ::= <alphanumeric strings>

Program Declaration Command Expression Numeral Variable P ::= D ; C D ::= int I D1 ; D2 proc I = C C ::= I = E C1 ; C2 while E : C print E call I E ::= N E1 + E2 E1 == E2 @I N ::= <strings of digits> I ::= <alphanumeric strings>

Program Declaration Command Expression Numeral Variable P ::= D ; C D ::= int I D1 ; D2 proc I = C fun I = E C ::= I = E C1 ; C2 while E : C print E call I E ::= N E1 + E2 E1 == E2 @I I() N ::= <strings of digits> I ::= <alphanumeric strings>

int i; i = 0; fun f = (i + i) + 1; i = i + 1; i = f() + f() - i int i; i = 0; fun f = 1; i = i + 1; i = f() + f() - i int i; i = 0; fun f = 1; i = i + 1; i = 1 + 1 - i

int i; i = 0; fun f = (i + i) + 1; i = i + 1; i = f() + f() - i int i; i = 0; fun f = (i + i) + 1; i = i + 1; i = (i + i) + 1 + (i + i) + 1 - i

Program Declaration Command Expression Numeral Variable P ::= D ; C D ::= int I D1 ; D2 proc I = C fun I = { C ; return E} C ::= I = E C1 ; C2 while E : C print E call I E ::= N E1 + E2 E1 == E2 @I I() N ::= <strings of digits> I ::= <alphanumeric strings>

Program Declaration Command P ::= D ; C D ::= int I D1 ; D2 proc I(I *) = C C ::= I = E C1 ; C2 while E : C print E I(E*) Program Declaration Command P ::= D ; C D ::= int I D1 ; D2 proc I(I ) = C C ::= I = E C1 ; C2 while E : C print E I(C)

(a) int x; int[3] y; proc p(x, z) { z = x + y[1]; y[x] = z }; x = 1; y[1] = 5; p(x + x, 0); print x; (a) namespace heap α α β x 1 y β p ɣ nil 0 1 2 0 5 0 ɣ codeptr α

int x; int[3] y; proc p(x, z) { (b) α δ z = x + y[1]; y[x] = z }; x = 1; y[1] = 5; p(x + x, 0); print x; (b) namespace α β heap x 1 y p β ɣ nil 0 1 2 0 5 0 δ x 2 z 0 α ɣ codeptr α

(c) int x; int[3] y; proc p(x, z) { z = x + y[1]; y[x] = z }; x = 1; y[1] = 5; p(x + x, 0); print x; (c) namespace heap α δ α β x 1 y β p ɣ nil 0 1 2 0 5 7 δ x 2 z 7 α ɣ codeptr α

(d) int x; int[3] y; proc p(x, z) { z = x + y[1]; y[x] = z }; x = 1; y[1] = 5; p(x + x, 0); print x; (d) namespace heap α α β x 1 y β p ɣ nil 0 1 2 0 5 7 δ x 2 z 7 α ɣ codeptr α

(a) (a) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) namespace α heap α x 1 f β nil β codeptr α

(b) (b) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) namespace α ɣ heap α x 1 f β ɣ n 4 α nil β codeptr α

(c) (c) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) namespace α ɣ heap α x 4 f β ɣ n 4 α nil β codeptr α

(d) (d) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) namespace α ɣ δ heap α x 4 f β ɣ n 4 α δ n 3 α nil β codeptr α

(e) (e) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) namespace α ɣ δ heap α x 12 f β ɣ n 4 α δ n 3 α nil β codeptr α

(f) int x; x = 1; proc f(n) { if n > 0 { x = x * n; f(n - 1) } }; f(4) (f) namespace α ɣ δ ε heap α ɣ δ ε x 12 n 4 n 3 n 2 f β nil β codeptr α α α α

define I = U define F(I) =... F(U)

Declaration D ::= int I D1 ; D2 proc I(I ) { C } Command C ::= I = E C1 ; C2 while E : C print E I(E) begin D in C end int x = 0; # begin int y # in y = x + 1; x = y + y end; # y print x # 2 int x = 0; # int y = 9; # begin int y # in y = x + 1; x = y + y print y end; print y # 1 # 9

int i = 0; proc p() { i = i + 1 }; begin int i = 9 in p(); print i # 9? 10? end; p(); print i # 1? 2?

(a) proc f(n) { begin int i; proc g(m) { print m + n + i } in i = 1; return g end }; int i = 9; h = f(2); h(3) (a) namespace α heap α f β i 9 nil β codeptr α

(b) proc f(n) { begin int i; proc g(m) { print m + n + i } in i = 1; return g end }; int i = 9; h = f(2); h(3) (b) namespace α ɣ heap α ɣ f β i 9 nil β codeptr α n 2 i 1 g δ α δ codeptr ɣ

(c) proc f(n) { begin int i; proc g(m) { print m + n + i } in i = 1; return g end }; int i = 9; h = f(2); h(3) (c) namespace α heap α f i β 9 ɣ n i 2 1 h δ g δ nil α β codeptr α δ codeptr ɣ

(d) proc f(n) { begin int i; proc g(m) { print m + n + i } in i = 1; return g end }; int i = 9; h = f(2); h(3) (d) namespace α ε heap α f β ɣ n 2 ε i 9 i 1 h δ g δ nil α m 3 ɣ β δ codeptr codeptr α ɣ

(d) proc f(n) { begin int i; proc g(m) { print m + n + i } in i = 1; return g end }; int i = 9; h = f(2); h(3) (d) namespace α ε heap α f β ɣ n 2 ε i 9 i 1 h δ g δ nil α m 3 ɣ β δ codeptr codeptr α ɣ