Order theoryGalois ConnectionsGC and Abstract InterpretationExamplesfsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesOrder Theory, Galois Connections andAbstract InterpretationDavid HenriquesCarnegie Mellon UniversityNovember 7th 2011David Henriques Order Theory 1/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesOrder TheoryDavid Henriques Order Theory 2/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesOrders are everywhereI0 ≤ 1 and 1 ≤ 1023ITwo cousins have a common grandfatherI22/7 is a worse approximation of π than 3.141592654Iaardvark comes before zyzzyvaIa seraphim ranks above an angelIrock beats scissorsIneither {1, 2, 4} or {2, 3, 5} are subsets of one another, butboth are subsets of {1, 2, 3, 4, 5}Actually, there is an intruder in this list. Can you spot it?It’s not easy, we need a formal treatment of order!David Henriques Order Theory 3/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesOrders are everywhereI0 ≤ 1 and 1 ≤ 1023ITwo cousins have a common grandfatherI22/7 is a worse approximation of π than 3.141592654Iaardvark comes before zyzzyvaIa seraphim ranks above an angelIrock beats scissorsIneither {1, 2, 4} or {2, 3, 5} are subsets of one another, butboth are subsets of {1, 2, 3, 4, 5}Actually, there is an intruder in this list. Can you spot it?It’s not easy, we need a formal treatment of order!David Henriques Order Theory 3/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesOrders are everywhereI0 ≤ 1 and 1 ≤ 1023ITwo cousins have a common grandfatherI22/7 is a worse approximation of π than 3.141592654Iaardvark comes before zyzzyvaIa seraphim ranks above an angelIrock beats scissorsIneither {1, 2, 4} or {2, 3, 5} are subsets of one another, butboth are subsets of {1, 2, 3, 4, 5}Actually, there is an intruder in this list. Can you spot it?It’s not easy, we need a formal treatment of order!David Henriques Order Theory 3/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesWhat should we require from an order?Partial OrderLet S be a set. A relation v in S is said to be a partial orderrelation if it has the following propertiesIif a v b and b v a then b = a (anti-symmetry)Iif a v b and b v c then a v c (transitivity)Ia v a (reflexivity)The pair (S, v) is said to be a partial order.Why these properties?Ithey correspond to intuitive notions of orderIstructures that share these properties have a lot of commonbehaviorDavid Henriques Order Theory 4/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesWhat should we require from an order?Partial OrderLet S be a set. A relation v in S is said to be a partial orderrelation if it has the following propertiesIif a v b and b v a then b = a (anti-symmetry)Iif a v b and b v c then a v c (transitivity)Ia v a (reflexivity)The pair (S, v) is said to be a partial order.Why these properties?Ithey correspond to intuitive notions of orderIstructures that share these properties have a lot of commonbehaviorDavid Henriques Order Theory 4/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesWhat should we require from an order?Partial OrderLet S be a set. A relation v in S is said to be a partial orderrelation if it has the following propertiesIif a v b and b v a then b = a (anti-symmetry)Iif a v b and b v c then a v c (transitivity)Ia v a (reflexivity)The pair (S, v) is said to be a partial order.Why these properties?Ithey correspond to intuitive notions of orderIstructures that share these properties have a lot of commonbehaviorDavid Henriques Order Theory 4/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Natural Numbers(N, ≤)Iif a ≤ b and b ≤ a then a = bIif a ≤ b and b ≤ c then a ≤ cIa ≤ aWell... this was not very informativeDavid Henriques Order Theory 5/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Natural Numbers(N, ≤)Iif a ≤ b and b ≤ a then a = bIif a ≤ b and b ≤ c then a ≤ cIa ≤ aWell... this was not very informativeDavid Henriques Order Theory 5/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Natural Numbers(N, ≤)Iif a ≤ b and b ≤ a then a = bIif a ≤ b and b ≤ c then a ≤ cIa ≤ aWell... this was not very informativeDavid Henriques Order Theory 5/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Natural Numbers(N, ≤)Iif a ≤ b and b ≤ a then a = bIif a ≤ b and b ≤ c then a ≤ cIa ≤ aWell... this was not very informativeDavid Henriques Order Theory 5/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Natural Numbers(N, ≤)Iif a ≤ b and b ≤ a then a = bIif a ≤ b and b ≤ c then a ≤ cIa ≤ aWell... this was not very informativeDavid Henriques Order Theory 5/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Rock, paper, scissors({,, }, “beats”)IWe don’t have that beats David Henriques Order Theory 6/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Rock, paper, scissors({,, }, “beats”)IWe don’t have that beats David Henriques Order Theory 6/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Rock, paper, scissorsLet’s try again({,, }, “is not beaten by”)IIt’s reflexive (e.g. is not beaten by )IIt’s antisymmetric (e.g. is not beaten bymeans wecan’t heaveis not beaten by )IIt’s NOT transitive ( is not beaten byis not beaten by . But We don’t have that is not beaten by )David Henriques Order Theory 7/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Rock, paper, scissorsLet’s try again({,, }, “is not beaten by”)IIt’s reflexive (e.g. is not beaten by )IIt’s antisymmetric (e.g. is not beaten bymeans wecan’t heaveis not beaten by )IIt’s NOT transitive ( is not beaten byis not beaten by . But We don’t have that is not beaten by )David Henriques Order Theory 7/ 40fsu-logoOrder theoryGalois ConnectionsGC and Abstract InterpretationExamplesExamples - Rock, paper, scissorsLet’s try again({,, }, “is not beaten
View Full Document