Some subtleties ·formally we should write{π1}U..U{πn}but we write{πi,·,πn} we can replace T191 T2 by T192,T2 whenever 1 and 2 are "equal as sets" P=pu0 p=puip p102=42U1 1U(2U3)=(1U2)U3 P1=P2P2=P3 P1=p1P2=P2 P三p P1=P3 1U2=1U we can replace 71 by 72 if they have the same underlying types and all annotations on corresponding function arrows are "equal as sets'' 1=2=衫p=p 分三子 (行122)=(2) PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 16
Some subtleties • formally we should write {π1} ∪ · · · ∪ {πn} but we write {π1, · · · , πn} • we can replace τ1 ϕ→1 τ2 by τ1 ϕ→2 τ2 whenever ϕ1 and ϕ2 are “equal as sets” ϕ = ϕ ∪ ∅ ϕ = ϕ ∪ ϕ ϕ1 ∪ ϕ2 = ϕ2 ∪ ϕ1 ϕ1 ∪ (ϕ2 ∪ ϕ3) = (ϕ1 ∪ ϕ2) ∪ ϕ3 ϕ = ϕ ϕ1 = ϕ2 ϕ2 = ϕ3 ϕ1 = ϕ3 ϕ1 = ϕ 0 1 ϕ2 = ϕ 0 2 ϕ1 ∪ ϕ2 = ϕ0 1 ∪ ϕ0 2 • we can replace τb1 by τb2 if they have the same underlying types and all annotations on corresponding function arrows are “equal as sets” τb = τb τb1 = τb 0 1 τb2 = τb 0 2 ϕ = ϕ 0 (τb1 →ϕ τb2) = (τb 0 1 ϕ 0 → τb 0 2 ) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 16
One more subtlety The function fny y=>y has type☑デas well as {Y)元 广[x一]上CFAe0:0 f卜CFA fnm a=>e0:U阿 Conservative extension lemma (i)Iff上cFAe:テthen [r.」ruLe:L]: (ii)If rHUL e:T then there exists r and such that f卜cFAe:,Lf」=「andl]=T. If we replaced the above rule by [E一]CFA0:0 fH化A fnx x=>e0:0 then some programs would have no type in the Control Flow Analysis! PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 17
One more subtlety The function fnY y => y has type τb {Y,Z →} τb as well as τb {Y →} τb Γ[ b x 7→ τbx] `CFA e0 : τb0 Γb `CFA fnπ x => e0 : τbx {π}∪ ϕ → τ0 Conservative extension lemma (i) If Γb `CFA e : τb then bΓbc `UL e : bτbc. (ii) If Γ `UL e : τ then there exists Γ and b τb such that Γb `CFA e : τb, bΓbc = Γ and bτbc = τ. If we replaced the above rule by Γ[ b x 7→ τbx] ` 0 CFA e0 : τb0 Γb ` 0 CFA fnπ x => e0 : τbx {π →} τ0 then some programs would have no type in the Control Flow Analysis! PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 17
Operational Semantics Different choices: Structural Operational Semantics ●Natural Semantics with environments -with substitutions Assumption:e is a closed expression;it evaluates to a value v U:=cfnπE=>e0 (closed expressions only) written上e→w PPA Section 5.2 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 18
Operational Semantics Different choices: • Structural Operational Semantics • Natural Semantics – with environments – with substitutions Assumption: e is a closed expression; it evaluates to a value v v ::= c | fnπ x => e0 (closed expressions only) written ` e −→ v PPA Section 5.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 18
Natural Semantics for Fun (1) 卜C→C 上（fnxx=>eo)→(fnrx=>eo) F(funn f x=>eo)→(fnxx=>(eo[f→funn f x=>eo]) 卜e1→(fnπx=>e0)上e2→v2卜eo[x→v2]→v0 e1e2→vo PPA Section 5.2 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 19
Natural Semantics for Fun (1) ` c −→ c ` (fnπ x => e0) −→ (fnπ x => e0) ` (funπ f x => e0) −→ (fnπ x => (e0[f 7→ funπ f x => e0])) ` e1 −→ (fnπ x => e0) ` e2 −→ v2 ` e0[x 7→ v2] −→ v0 ` e1 e2 −→ v0 PPA Section 5.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 19
Natural Semantics for Fun (2) -e0→true-e1→v1 Hif eo then e1 else e2-v1 卜e0→false卜e2→v2 Hif eo then e1 else e2-U2 Fe1→v1卜e2[x-v1]→v2 卜1etx=e1ine2→v2 -e1→v1-e2→v2 if v1 op v2=U -e1ope2→v PPA Section 5.2 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 20
Natural Semantics for Fun (2) ` e0 −→ true ` e1 −→ v1 ` if e0 then e1 else e2 −→ v1 ` e0 −→ false ` e2 −→ v2 ` if e0 then e1 else e2 −→ v2 ` e1 −→ v1 ` e2[x 7→ v1] −→ v2 ` let x = e1 in e2 −→ v2 ` e1 −→ v1 ` e2 −→ v2 ` e1 op e2 −→ v if v1 op v2 = v PPA Section 5.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 20