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