DOC PREVIEW
CMU CS 15414 - Order Theory, Galois Connections and Abstract Interpretation

This preview shows page 1-2-3-4-5-38-39-40-41-42-43-77-78-79-80-81 out of 81 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 81 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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 bymeans wecan’t heaveis not beaten by )IIt’s NOT transitive ( is not beaten byis 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 bymeans wecan’t heaveis not beaten by )IIt’s NOT transitive ( is not beaten byis 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

CMU CS 15414 - Order Theory, Galois Connections and Abstract Interpretation

Download Order Theory, Galois Connections and Abstract Interpretation
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Order Theory, Galois Connections and Abstract Interpretation and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Order Theory, Galois Connections and Abstract Interpretation 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?