Denotational Semantics October 26,2018 4口8，+三，+至+至a0 Denotational Semantics
Denotational Semantics October 26, 2018 Denotational Semantics
Syntax of the Imp Language (intexp)e::=0 11 1... x I -e l e+e l e-e 1... (boolexp)b::=true false I e-e l e<ele<el... b bAb l bvb l .. no quantified terms (comm)c::=x:=e I skip I cjc if b then c else c I while b do c 4口84三，4无+3月a0 Denotational Semantics
Syntax of the Imp Language (intexp) e ::= 0 | 1 | . . . | x | -e | e+e | e-e | . . . (boolexp) b ::= true | false | e=e | e < e | e < e | . . . | ¬b | b ∧ b | b ∨ b | . . . no quantified terms (comm) c ::= x := e | skip | c;c | if b then c else c | while b do c Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σevar→z I-boolexp∈boolexp→∑→B -lcomm E comm→∑→∑1 Σ.鸣ΣU山 x =ellcomm o=x ellintexp or] lx :=x 6llcomm ((x.7) =(X,7)Hx(【x*61meo(x,7) =1(X,7)1x42 =1(X42) IIskipllcamm lc;c.lcomm o if I[cllcomm=L (lic'lcommclcomm)otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σevar→z I-lboolexp∈boolexp→∑→B -lcomm E comm-→∑→∑1 Σ.ΣU山 Ix :=ellcomm=x ellintexp} Ix :=x *6llcomm((x,7)) =((x,7)Hx(Ix 6lintexp((x.7)])} ={(x,7){x42} ={(x,42)} Ilskip llcomm c= IIcic'llcamm if lclcomm c=L =(lc'llconmccomm)cr otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σ№var→z I-boolexp∈boolexp→∑→B -lcomm∈comm→∑→∑1 Σ.粤ΣU山 Ix :ellcomm =x [ellintexp [Ix :=x *6llcomm((x,7)} ={(x,7)Mx→(x*6 intexp(x,7)》 ={(x,7)Hx42} ={(x,42)》 [skiplcomm if I[cllcomm=L cic comm= (IIc'llcomm ollcllcomm)r otherwise Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Denotational Semantics -lintexp∈intexp→∑→Z Σevar→z I-Iboolexp∈boolexp→∑→B -lcomm E comm-→∑→∑1 Σ.ΣU山 Ix :=ellcomm=x ellintexp} Ix :=x *6llcomm((x,7)} =((x,)Hx(Ix 6lintexp((x,7)])} ={(x,7){x42} ={(x,42)》 [skipllcomm IIc;c'llcomm eommcc)otherwise if [Icllcomm=⊥ Denotational Semantics
Denotational Semantics ~−intexp ∈ intexp → Σ → Z Σ def = var → Z ~−boolexp ∈ boolexp → Σ → B ~−comm ∈ comm → Σ → Σ⊥ Σ⊥ def = Σ ∪ {⊥} ~x := ecomm σ = σ{x { ~eintexp σ} ~x := x ∗ 6comm {(x, 7)} = {(x, 7)}{x { (~x ∗ 6intexp{(x, 7)})} = {(x, 7)}{x { 42} = {(x, 42)} ~skipcomm σ = σ ~c;c 0 comm σ = ( ⊥ if ~ccomm σ = ⊥ (~c 0 comm ◦ ~ccomm) σ otherwise Denotational Semantics
Semantics of Sequential Composition Ne extend f S→TL to fr eS,→Ti ifx=⊥ otherwise This defines(-)he(S→Ti)→(S.→T) So llc;c'llcomm=(IIc'lcomm)(IIclcomm ) Denotational Semantics
Semantics of Sequential Composition We extend f ∈ S → T⊥ to fy ∈ S⊥ → T⊥ fy x def = ( ⊥ if x = ⊥ f x otherwise This defines (−)y ∈ (S → T⊥) → (S⊥ → T⊥) So ~c;c 0 comm σ = (~c 0 comm)y (~ccomm σ). Denotational Semantics
Semantics of Conditionals litb then c else Calcommmmifalse Ic1lcomm o if [blboolexp =true Examples: lif x<0 then x=-x else skipllcomm ((x,-3)} =IX =-xllcomm ((x,-3)} since [[x Ollboolexp ((x,-3))=true =((x,-3)Hx-xllintexp ((x,-3)H ={(x,3)} lif x<0 then x =-x else skipllcomm((x,5)) =[Iskipllcomm ((x,5)} since [[x Ollboolexp ((x,5)}=false ={(x,5)} Denotational Semantics
Semantics of Conditionals ~if b then c1 else c2comm σ = ( ~c1comm σ if ~bboolexp σ = true ~c2comm σ if ~bboolexp σ = false Examples: ~if x < 0 then x = −x else skipcomm {(x, −3)} = ~x = −xcomm {(x, −3)} since ~x < 0boolexp {(x, −3)} = true = {(x, −3)}{x { ~−xintexp {(x, −3)}} = {(x, 3)} ~if x < 0 then x = −x else skipcomm {(x, 5)} = ~skipcomm {(x, 5)} since ~x < 0boolexp {(x, 5)} = false = {(x, 5)} Denotational Semantics
Semantics of Loops Idea:define the meaning of while b do c as that of if b then (c;while b do c)else skip That is, Iwhile b do cllcomm =[if b then (c;while b do c)else skipllcomm o (while b do clcomm)a(clcomm if [oolexp=true otherwise However,the semantic function is not syntax directed,as Ilwhile b do cllcomm itself shows as a sub-term on the right side of the equation. Denotational Semantics
Semantics of Loops Idea: define the meaning of while b do c as that of if b then (c ; while b do c) else skip That is, ~while b do ccomm σ = ~if b then (c ; while b do c) else skipcomm σ = ( (~while b do ccomm)y (~ccomm σ) if ~bboolexp σ = true σ otherwise However, the semantic function is not syntax directed, as ~while b do ccomm itself shows as a sub-term on the right side of the equation. Denotational Semantics
Semantics of Loops Actually we can view Iwhile b do clcomm as a solution for this equation: while b do c]lcomm =lif b then (c;while b do c)else skipllcomm (while do com)(commftrue otherwise That is,Iwhile b do cllcomm is a fixed-point of Fsex-zi.oez{&iclameneaeg=twue otherwise However,,not every Fe(E→∑t)→（∑→∑！）has a fixed-point,, and some may have more than one. Example:for any o',o.is a solution for l[while true do x :=x+1]comm- Denotational Semantics
Semantics of Loops Actually we can view ~while b do ccomm as a solution for this equation: ~while b do ccomm σ = ~if b then (c ; while b do c) else skipcomm σ = ( (~while b do ccomm)y (~ccomm σ) if ~bboolexp σ = true σ otherwise That is, ~while b do ccomm is a fixed-point of F def = λf ∈ Σ → Σ⊥. λσ ∈ Σ. ( fy(~ccomm σ) if ~bboolexp σ = true σ otherwise However, not every F ∈ (Σ → Σ⊥) → (Σ → Σ⊥) has a fixed-point, and some may have more than one. Example: for any σ 0 , λσ. σ0 is a solution for ~while true do x := x + 1comm. Denotational Semantics