tag:blogger.com,1999:blog-6918427997759942244.post6203044671557686484..comments2023-05-17T07:01:49.378-04:00Comments on Elegant Coding: Programming and Order Theoryelegantcodinghttp://www.blogger.com/profile/12373582469986942814noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-6918427997759942244.post-24637242650722198102013-03-14T22:18:17.172-04:002013-03-14T22:18:17.172-04:00Decent post. As for the concluding paragraph, if ...Decent post. As for the concluding paragraph, if you want to see order theory applied to computer programming on steroids, check out abstract interpretation: http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/ Abstract interpretation is a powerful generalization of data flow analysis.<br /><br />The basic idea is that each variable in the program lies in some domain, which becomes a lattice when we consider the powerset of all possible values for variables in that domain. Consequently, we can view the operators in the program (such as the integer addition operator) as being operators defined upon lattices. Abstract interpretation is concerned with overapproximating all possible behaviors of a given program. By "overapproximating", we mean that, if "all possible behaviors of a given program" is represented by a lattice element b, then we want to compute some lattice element that is greater than or equal to b. In such a way, we are able to render decisions about the program that are "sound", i.e. that they take into account all possible behaviors of the program, if not "complete", i.e. that they are approximate and hence account for behaviors that are not possible at runtime.<br /><br />We do this by computing an approximation of the program's "collecting semantics", which loosely means "the set of all values that each variable might take on at each program point". The collecting semantics is formulated in a similar way to data flow equations in compiler theory (although dually): that the set of all possible values at any program point p is "at least as big as" (order-theoretically) the values at the locations immediately leading to p. This takes the form of a recursively-defined equation, which uses the aforementioned lattice transformers (i.e. for the addition operator) and the lattice meet/join operators. We seek the least solution to this equation, since the least correct solution describes the smallest set of values, whereas the greatest correct solution would be top (all states are possible at all points) and hence useless. The solution to this equation does exist mathematically (see e.g. Tarski's fixedpoint theorem), although it is not computable. That's where abstract interpretation comes into play.<br /><br />We establish a Galois connection between the powerset lattice representing the concrete values, called the "concrete domain", and some "abstract domain" that overapproximately represents those concrete values. For example, one abstract domain representing an integer variable is the "interval lattice"; it represents the integral lower and upper bound that a variable might assume at that point. Next, we design abstract lattice transformers that mimic the concrete ones: for example, the concrete addition lattice operator must be re-designed for the abstract domain such that it operates on interval values instead of sets of integers. Then, we set up a recursively-defined equation identical to the concrete collecting semantics equation, except using the abstract transformers and abstract meet/join in place of the concrete ones. And this abstract equation not only has a solution (if certain properties are ensured, such as completeness of the abstract lattice), but the solution is computable using chaotic iteration.<br /><br />That's the basic idea. There are more complexities to abstract interpretation, such as how to ensure termination of the fixedpoint computation when dealing with incomplete lattices, designing abstract domains that describe relationships between multiple variables, and other topics.<br /><br />It's serious business; abstract interpretation is used in the static analyzer Astree to prove the absence of runtime errors in safety-critical systems (e.g. flight-control software).Rolf Rolleshttps://www.blogger.com/profile/11281039521454183084noreply@blogger.com