A---calculus with Constants and Let-blocks.ppt

1、A-calculus with Constants and Let-blocks,September 19, 2006,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Outline,Recursion and Y combinator The llet Calculus,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Recursion,fact can be rewritten as: fact = n. Cond (Zero? n) 1 (Mul n (fact (Sub

2、n 1)How to get rid of the fact on the RHS?,fact n = if (n = 0) then 1else n * fact (n-1),Idea: pass fact as an argument to itself,Self application!,H = f.n.Cond (Zero? n) 1 (Mul n (f f (Sub n 1),fact = H H,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Self-application and Paradoxes,Self appli

3、cation, i.e., (x x) is dangerous. Suppose:u y. if (y y) = a then b else a What is (u u) ?,(u u) if (u u) = a then b else aContradiction!Any semantics of -calculus has to make sure that functions such as u have the meaning , i.e. “totally undefined” or “no information”.Self application also violates

4、every type discipline.,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Recursion and Fixed Point Equations,Recursive functions can be thought of as solutions of fixed point equations:fact = n. Cond (Zero? n) 1 (Mul n (fact (Sub n 1),SupposeH = f.n.Cond (Zero? n) 1 (Mul n (f (Sub n 1)thenfact =

5、H factfact is a fixed point of function H!,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Fixed Point Equations,f : D D A fixed point equation has the form f(x) = x,Examples: f: Int Int Solutionsf(x) = x2 2f(x) = x2 + x + 1f(x) = x,x = 2, x = -1,no solutions,infinite number of solutions,Its so

6、lutions are called the fixed points of f because if xp is a solution thenxp = f(xp) = f(f(xp) = f(f(f(xp) = .,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Least Fixed Point,Consider f n = if n=0 then 1else (if n=1 then f 3 else f (n-2) H = f.n.Cond(n=0 , 1, Cond(n=1, f 3, f (n-2) Is there an

7、 fp such that fp = H fp ?,f1 n = 1 if n is even= otherwise,f1 contains no arbitrary information and is called the least fixed point. Unique solution!,f2 n = 1 if n is even= 5 otherwise,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Y : A Fixed Point Operator,Notice Y F x.F (x x) (x.F (x x)F (Y

8、 F) ,Y f.(x. (f (x x) (x.(f (x x),F (x.F (x x) (x.F (x x),F (x.F (x x) (x.F (x x),F (Y F) = Y F (Y F) is a fixed point of FY computes the least fixed point of any function !There are many different fixed point operators.,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Mutual Recursion,odd = H1

9、even even = H2 oddwhere H1 = f.n.Cond(n=0, False, f(n-1)H2 = f.n.Cond(n=0, True, f(n-1),odd n = if n=0 then False else even (n-1) even n = if n=0 then True else odd (n-1),substituting “H2 odd” for even odd = H1 (H2 odd) = H odd where H = odd = Y H,f. H1 (H2 f),Can we expressing odd using Y ?,Septemb

10、er 19, 2006,http:/www.csg.csail.mit.edu/6.827,-calculus with Combinator Y,Recursive programs can be translated into the -calculus with constants and Y combinator. However, Y combinator violates every type disciplinetranslation is messy in case of mutually recursive functions extend the -calculus wit

11、h recursive let blocks.,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Outline,Recursion and Y combinator The llet Calculus ,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,-calculus with Constants & Letrec,E := x | x.E | E E | Cond (E, E, E) | PFk(E1,.,Ek) | CN0 | CNk(E1,.,Ek) | CNk(SE1,

12、.,SEk) | let S in E PF1 := negate | not | . | Prj1| Prj2 | . PF2 := + | . CN0 := Number | Boolean CN2 := cons | .Statements S := | x = E | S; SVariables on the LHS in a let expression must be pairwise distinct,not in initial terms,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Let-block Statem

13、ents,“ ; “ is associative and commutativeS1 ; S2 S2 ; S1 S1 ; (S2 ; S3) (S1 ; S2 ) ; S3 ; S Slet in E E,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Free Variables of an Expression,FV(x) = x FV(E1 E2) = FV(E1) U FV(E2) FV(x.E) = FV(E) - x FV(let S in E) =,FVS(S) U FV(E) BVS(S),FVS() = BVS()

14、= ,BVS(x = E; S) =,FVS(x = E; S) =,FV(E) U FVS(S),x U BVS(S),September 19, 2006,http:/www.csg.csail.mit.edu/6.827,-Renaming (to avoid free variable capture),Assuming t is a new variable, rename x to t : x.e t.(et/x) let x = e ; S in e0 let t = et/x ; St/x in e0t/x where t/x is defined as follows:,xt

15、/x = t yt/x = y if x y (E1 E2 )t/x = (E1t/x E2t/x) (x.E)t/x = x.E (y.E)t/x = y.Et/x if x y (let S in E)t/x ?,= (let S in E) if x FV(let S in E) = (let St/x in Et/x) if x FV(let S in E),(S1; S2)t/x = (y = E)t/x = t/x =,(S1t/x; S2t/x),(y = Et/x),September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Pri

16、mitive Functions and Datastructures,-rules+( n, m) n+m .Cond-rulesCond(True, e1, e2 ) e1Cond(False, e1, e2 ) e2,Data-structures CNk(e1,.,ek ) Prji(CNk(a1,.,ak ) ,let t1 = e1; . ; tk = ek in CNk(t1,.,tk ),ai,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,The -rule,The normal -rule(x.e) ea e ea/

17、xis replaced the following -rule(x.e) ea let t = ea in et/xwhere t is a new variableand the Instantiation rules which are used to refer to the value of a variable,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Values and Simple Expressions,Values V := x.E | CN0 | CNk(SE1,.,SEk)Simple expressio

18、ns SE := x | V,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Contexts for Expressions,A context is an expression (or statement) with a “hole” such that if an expression is plugged in the hole the context becomes a legitimate expression:C := | x.C | C E | E C | let S in C | let SC in E Stateme

19、nt Context for an expressionSC := x = C | SC ; S | S; SC,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,let Instantiation Rules,A free variable in an expression can be instantiated by a simple expression,Instantiation rule 2 (x = a ; SCx) ,Instantiation rule 1 (let x = a ; S in Cx) ,(let x = a

20、 ; S in Ca),Instantiation rule 3 x = a where a = Cx,(x = a ; SCa),x = CCx,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Lifting Rules: Motivation,let f = let S1 in x.e1 y = f a in(let S2 in x.e2) e3) How do we juxtapose (x.e1) a or(x.e2) e3 ?,September 19, 2006,http:/www.csg.csail.mit.edu/6.8

21、27,Lifting Rules,(let S in e) is the -renamed (let S in e) to avoid name conflicts in the following rules:,x = let S in e let S1 in (let S in e) (let S in e) e1 Cond(let S in e), e1, e2) PFk(e1,.(let S in e),.ek),x = e; S,let S1; S in e,let S in e e1,let S in Cond(e, e1, e2),let S in PFk(e1,.e,.ek),

22、September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Confluenence and Letrecs,odd = n.Cond(n=0, False, even (n-1) (M) even = n.Cond(n=0, True, odd (n-1),substitute for even (n-1) in M odd = n.Cond(n=0, False, Cond(n-1 = 0 , True, odd (n-1)-1) (M1) even = n.Cond(n=0, True, odd (n-1),substitute for od

23、d (n-1) in M odd = n.Cond(n=0, False, even (n-1) (M2) even = n.Cond(n=0, True,Cond( n-1 = 0 , False, even (n-1)-1),Can odd in M1 and M2 be reduced to the same expression ?Proposition: let is not confluent. Ariola & Klop 1994,September 19, 2006,http:/www.csg.csail.mit.edu/6.827, versus let Calculus,T

24、erms of the let calculus can be translated into terms of the calculus by systematically eliminating the let blocks. Let T be such a translation.Suppose e e1 in let then does there exist a reduction such that Te Te1 in ?,We need a notion of observable values to compare terms in a meaningful way.,Sept

25、ember 19, 2006,http:/www.csg.csail.mit.edu/6.827,Instantaneous Information,“Instantaneous information” (info) of a term is defined as a (finite) treesTP := | | CN0 | CNk(TP1,.,TPk)Info: E TP,InfoS in E = Info EInfox.E = InfoCN0 = CN0InfoCNk(a1,.,ak) = CNk(Infoa1,.,Infoak)InfoE = otherwise,Notice this procedure always terminates,September 19, 2006,http:/www.csg.csail.mit.edu/6.827,Reduction and Info, t (bottom) t t (reflexive) CNk(v1,.,vi,.,vk) CNk(v1,.,vi,.,vk) if vi vi,Terms can be compared by their Info value,