Quantifier Elimination For Imperative Programs

The Background When people want to write mathematical statments formally, they make use of the quantifier symbols $\exists$ and $\forall$. Of course, many formally distinct mathematical statements are actually logically equivalent. For example, the following two logical formulas are equivalent (if $x$ is a real number): $$ \exists x: a x^2 + b x + c = 0 $$ $$ b^2 - 4ac \geq 0 $$ It is worth noting briefly that the two formulas are only equivalent when $x$ is restricted to be a real number. If we allowed $x$ to be any complex number (or further restricted $x$ to be an integer!) the two formulas would no longer be equivalent. We say that the formulas are equivalent in the theory of real numbers. For our purposes, a theory is a formal language together with some axioms defining which formulas constructed from that language are true. When a formula can be written with and without quantifiers, the quantifier-free version has some advantages from a computational perspective. The main advantage in the context of formal mathematical statements is that in most theories we care about, it is possible to describe an algorithm that decides the truth of any quantifier-free formula in that theory. This is not generally true of quantifier-ful formulas. If we squint and pretend our two formulas are computer programs, the quantifier-free version looks like a few arithmetic operations while the quantifier-ful version looks an awful lot like a loop that might never halt! This suggests an algorithm for deciding the truth of a formula. First convert the formula to a quantifier-free form, then apply the universal-quantifier-free-deciding algorithm to the result. This is possible in some theories which have known procedures for removing quantifiers from any formula in that theory and, in fact, the Z3 SMT solver has a quantifier elimination tactic which attempts to apply such procedures. Of course, quantifier elimination is not performing any decidability magic. Theories which admit quantifier elimination are fully decidable even by algorithms that do not perform quantifier elimination. So one reason Z3 has a quantifier elimination tactic (and not some other deciding algorithm) is because it can make the deciding cheaper. Even if our “loopy” pseudo-program above eventually terminates, it might take a long time. It would be easier to do the arithmetic instead. The Project This brings us to the task at hand. If quantifier elimination can speed up SMT solving, maybe it can speed up regular old computer programs. As we saw above, true quantifiers generally translate to loops that may never terminate. In most programming circles, writing loops that you know ahead of time might never terminate is generally frowned upon, so we will need more limited substitutes. We will use the commonly available any and all functions as our restricted quantifiers. any returns true if and only if any of its inputs is true while all returns true if and only if all of its inputs are true (get it?). This makes any an existential quantifier ($\exists$) and all a universal quantifier ($\forall$). We will also restrict ourselves to a single theory: Presburger Integer Arithmetic. Formulas in Presburger Arithmetic are built from the following language: $[ \neg, \wedge, \vee, \exists, \forall ] \cup \mathbb{N} \cup [ +,-,<,= ]$. Where the first three symbols are the standard first order predicate logic not, and, and or. We will operate on Python programs because Python has a few nice properties: