Partially Ordered Sets A relation p is reflexive on S iff Vx E S.xpx transitive iff xpyAypz→xPZ antisymmetric iff xpy^ypxx=y symmetric iff xpy=ypx Eis a preorder on S iff is reflexive on S and tansitive is a partial order on S iff is a preorder on S and antisymmetric A poset S S with a partial order on S A discretely ordered S S with Ids as a partial order on S f is monotone from S to T iff f S-T and Vx.yES.x三y=fxg1 y is upper bound of X VxEX.X三y where y e S and X三S 口⊙4三无+ Denotational Semantics
Partially Ordered Sets A relation ρ is reflexive on S iff ∀x ∈ S.x ρ x transitive iff x ρ y ∧ y ρ z ⇒ x ρ z antisymmetric iff x ρ y ∧ y ρ x ⇒ x = y symmetric iff x ρ y ⇒ y ρ x v is a preorder on S iff v is reflexive on S and tansitive v is a partial order on S iff v is a preorder on S and antisymmetric A poset S S with a partial order v on S A discretely ordered S S with IdS as a partial order on S f is monotone from S to T iff f ∈ S → T and ∀x, y ∈ S. x v y ⇒ f x v 0 f y y is upper bound of X ∀x ∈ X. x v y where y ∈ S and X ⊆ S Denotational Semantics
Partially Ordered Sets A relation p is reflexive on S iff Vx E S.xpx transitive iff xpyAypz=xpz antisymmetric iff xpyaypxx=y symmetric iff xpy→ypx Eis a preorder on S iff is reflexive on S and tansitive is a partial order on S iff is a preorder on S and antisymmetric A poset S S with a partial order L on S A discretely ordered S S with Ids as a partial order on S f is monotone from S to T iff f∈S→T and Vx,y∈S.xgy→fxg'fy y is upper bound of X XEX.X三y where yE S and Xc S Denotational Semantics
Partially Ordered Sets A relation ρ is reflexive on S iff ∀x ∈ S.x ρ x transitive iff x ρ y ∧ y ρ z ⇒ x ρ z antisymmetric iff x ρ y ∧ y ρ x ⇒ x = y symmetric iff x ρ y ⇒ y ρ x v is a preorder on S iff v is reflexive on S and tansitive v is a partial order on S iff v is a preorder on S and antisymmetric A poset S S with a partial order v on S A discretely ordered S S with IdS as a partial order on S f is monotone from S to T iff f ∈ S → T and ∀x, y ∈ S. x v y ⇒ f x v 0 f y y is upper bound of X ∀x ∈ X. x v y where y ∈ S and X ⊆ S Denotational Semantics