![\"lattice002.bmp\"](\"http:\/\/scientopia.org\/img-archive\/goodmath\/img_271.bmp\")
<\/p>\n<\/p>\n
There’s a kind of graph which is very commonly used by people like me for analysis applications, called a lattice. A lattice is a graph with special properties that make it
\nextremely useful for representing information in an analysis system.<\/p>\n
<\/p>\n
I’ve mentioned before that you can use a graph G=(V,E) to describe a partial order over its vertices, where given two vertices a,b∈V, a<b if and only if either (a,b) ∈E, or there exists
\nsome vertex c∈V such that a<c and c<b. If this is true, G is called a partial order graph (POG). <\/p>\n
![\"glb-graph.png\"](\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_272.png?resize=213%2C236\")
<\/p>\n
If we look at POGs, we can create a kind of completion property for describing certain POGs, without Given a POG P, if for any any pair of vertices a and b in P, there is exactly one member in GLB(a,b), then the graph is called a semi-lattice<\/em>. The example graph above is not<\/em> a semi-lattice: the GLB(A,B) contains two elements. The graph to the right is<\/em> a semi-lattice.<\/p>\n There’s a symmetric notion – the least upper bound. You can guess it’s definition. If a graph Why are lattices so important? <\/p>\n A lot of the work that I’ve done has been on program analysis of one kind or another. Program Suppose that you know that statement A and statement B are completely independent. After A, you know some set of facts FA<\/sub>; after statement B, you know some set of facts FB<\/sub>. What For a program analysis to be sound and conservative – which is a fancy way of saying “absolutely sure that its results are correct” – the set of values that can be produced by the analysis must, at least, be a semi-lattice.<\/p>\n To give you a better sense, let’s look at an example.<\/p>\n Suppose we want to see what we can replace with constants in the code above. After the first Now we start the conditional. In the true branch, we end up with: {Const(x,13), Const(y,26×26), After the conditional, what do we have? It’s not just something like set union, or set intersection, This is part of a common, general pattern in all sorts of analysis, from programs, to planning, to What that means for program analysis, in practical terms, is that we can perform optimizations – make changes to the program to make it more efficient – based on information from the analysis: if the analysis says that the optimization won’t change the results of the program, then we can be absolutely sure that it won’t. We call that being conservative: we only do things that we can be absolutely sure There’s a kind of graph which is very commonly used by people like me for analysis applications, called a lattice. A lattice is a graph with special properties that make it extremely useful for representing information in an analysis system.<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[25],"tags":[],"class_list":["post-513","post","type-post","status-publish","format-standard","hentry","category-graph-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-8h","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/513","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=513"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/513\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=513"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=513"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=513"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\ncausing them to become total orders, called a greatest lower bound property. Suppose we’ve got two
\nvertices a and b, where a is not<\/em> less that b, and b is not<\/em> less than a. In a graph with
\nthe GLB property, there is some set of vertices which are the largest<\/em> vertices according to the
\ngraph partial order, and which are less than both a and b. This set, called the greatest lower bound set (GLB set) of a and b will consist of vertices that are not ordered relative to each other in the graph partial order. For example, if you look at the graph to the right, you can J and C are both GLBs of A and B – but J is not less that C, and C is not less than J. They’re not comparable. But they, in turn, have their own GLB – D is the GLB of C and J.<\/p>\n![\"semi-lattice.png\"](\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_273.png?resize=258%2C274\")
<\/p>\n
\nhas both a LUB and a GLB, then it’s called a lattice.<\/p>\n
\nanalysis is pretty typical of how lattices are used. When you’re doing an analysis of some kind on a program, at some location in the program, you have some knowledge about the properties of the program
\nat that point. Then you reach a conditional. At the end of one branch of the conditional, what
\nyou know can be represented as some value T. At the end of the other branch of the conditional, what
\nyou know can be represented as some value F. What do you know after the two branches join<\/em>, at the first statement after the conditional? What you know is the greatest lower bound<\/em> of T and F.<\/p>\n
\ndo you know after both A and B? You know the least upper bound<\/em> of FA<\/sub> and
\nFB<\/sub>.<\/p>\n\ndef foo(a,b):\nx = 13\ny = x*2\nz = x * a\nif (b < z):\nz = y*z\nelse:\nx = sqrt(y)\nq = x\/11\nreturn z\n<\/pre>\n
\nstatement, X is a constant: {Const(x,13)}. After the second statement, we can say that y is a constant,
\ntoo – it’s a constant times a constant. {Const(x,13), Const(y,26)}. After the third statement, we’re x and
\ny are still constant; z isn’t: {Const(x,13), Const(y,26), Var(z)}.<\/p>\n
\nVar(z)}. In the false branch, we wind up with {Const(x,sqrt(26)), Const(y,26), Var(z)}.<\/p>\n
\nor even set difference. It’s something specific to this kind of information – the lower bound of the two
\nbranches. We lose X as a constant – because it could be one of two different constants, based on the value
\nof the parameter b, which we don’t know. What we end up with is {Var(x),Const(y,26),Var(z)} – the lower
\nbound of the two branches in the semi-lattice.<\/p>\n
\nknowledge representation. When we combine two sets of information, we can either know that both are true
\n(in which case we combine them using the upper bound), or we can know that one or<\/em> the other is
\ntrue (in which case we combine them using the lower bound). By making sure that the values form
\na lattice, and using the lower and upper bounds in the lattice to combine information, we know that our results are safe in the sense that we’ll never claim to know something that we don’t. <\/p>\n
\nwon’t change the meaning of the program. That’s obviously a pretty critical thing in a compiler. Proving that the set of values used by the analysis form a lattice is by far the easiest way of showing that the analysis is conservative.<\/p>\n","protected":false},"excerpt":{"rendered":"