Exact Boolean Abstraction of Linear Equation Systems

Abstract

We study the problem of how to compute the boolean abstraction of the solution set of a linear equation system over the positive reals. We call a linear equation system ϕ exact for the boolean abstraction if the abstract interpretation of ϕ over the structure of booleans is equal to the boolean abstraction of the solution set of ϕ over the positive reals. Abstract interpretation over the booleans is thus complete for the boolean abstraction when restricted to exact linear equation systems, while it is not complete more generally. We present a new rewriting algorithm that makes linear equation systems exact for the boolean abstraction while preserving the solutions over the positive reals. The rewriting algorithm is based on the elementary modes of the linear equation system. The computation of the elementary modes may require exponential time in the worst case, but is often feasible in practice with freely available tools. For exact linear equation systems, we can compute the boolean abstraction by finite domain constraint programming. This yields a solution of the initial problem that is often feasible in practice. Our exact rewriting algorithm has two further applications. Firstly, it can be used to compute the sign abstraction of linear equation systems over the reals, as needed for analyzing function programs with linear arithmetics. Secondly, it can be applied to compute the difference abstraction of a linear equation system as used in change prediction algorithms for flux networks in systems biology.

1. Introduction

We develop approaches to remedy the incompleteness of abstract interpretation [1] of linear equation systems over the reals, in the algebra of booleans $\mathbb{B}=\{0,1\}$ and the structure of signs $\mathbb{S}=\{-1,0,1\}$. These abstractions have various applications: in systems biology, the boolean abstraction underlies abstractions of chemical reactions networks into Boolean networks [2,3]. In program analysis, the sign abstraction can be applied to functional programs with arithmetics for analyzing the signs of the possible values of floating-point variables [4,5].

The soundness of abstract interpretations of first-order logic formulas without negation was shown by John [6,7,8,9]. It applies to the interpretation in any concrete structure S, as long as it is connected by a homomorphism $h:S\to \Delta$ to the abstract structure $\Delta$. The concrete interpretation of a first-order formula $\varphi$ is the set of concrete solutions $so{l}^S\left(\varphi \right)$, and its abstract interpretation is the set of its abstract solutions $so{l}^{\Delta }\left(\varphi \right)$. John’s soundness theorem (see Theorem 1 below) states that the set of abstract solutions of overapproximates the abstraction by h of the set of concrete solutions:

$$h\circ so{l}^S\left(\varphi \right)\subseteq so{l}^{\Delta }\left(\varphi \right)$$

When choosing the operators in ${\Sigma }_{bool}=\{+,\ast ,0,1\}$, the class of negation-free first-order formulas with operators in ${\Sigma }_{bool}$ extends on the classes of linear and polynomial equation systems. In this article, we consider the boolean abstraction which is the unique homomorphism $h_{\mathbb{B}}:{\mathbb{R}}_{+}\to \mathbb{B}$, and the sign abstraction which is the unique homomorphism $h_{\mathbb{S}}:\mathbb{R}\to \mathbb{S}$ with respect to the operators in ${\Sigma }_{bool}$. The boolean abstraction maps any strictly positive real to 1 and 0 to 0. The sign abstraction extends on the boolean abstraction while mapping all strictly negative reals to $-1$. We note that the structure of signs $\mathbb{S}$ is not an algebra since the sum of a positive and a negative number may have any sign.

1.1. Problematics

A natural question is whether abstract interpretation is complete [10] for the abstraction of formulas induced by a homomorphisms $h:S\to \Delta$, i.e, whether for all negation-free first-order formulas $\varphi$ with the same operators:

$$h\circ so{l}^S\left(\varphi \right)=so{l}^{\Delta }\left(\varphi \right)$$

We call a formula $\varphi$h-exact if it satisfies this property. A counter example against the completeness of abstraction interpretation for the boolean and the sign abstraction is the linear equation ${\varphi }_0$ equal to $x+y\stackrel{\circ }{=}x+z$. Here, we write $\stackrel{\circ }{=}$ for the equality symbol inside the logic, to point out its difference from equality in the language of mathematics. Formula ${\varphi }_0$ is neither $h_{\mathbb{B}}$-exact nor $h_{\mathbb{S}}$-exact. This can be seen as follows. Over the reals ${\varphi }_0$ is equivalent to $y\stackrel{\circ }{=}z$, so that all assignments $\tau$ that are abstractions of concrete solutions of ${\varphi }_0$ must satisfy $\tau \left(y\right)=\tau \left(z\right)$. When interpreted abstractly over $\mathbb{B}$ or $\mathbb{S}$, however, ${\varphi }_0$ admits the abstract solution $\tau =[x/1,y/1,z/0]$ which is not the abstraction of any concrete solution since $\tau \left(y\right)\ne \tau \left(z\right)$.

To deal with the incompleteness of abstract interpretation, we propose to study the following two questions for homomorphism $h:S\to \Delta$ where h is either the boolean abstraction $h_{\mathbb{B}}$ or the sign abstraction $h_{\mathbb{S}}$.

Exact Rewriting Can we rewrite linear equation systems to h-exact formulas?

Computing Abstractions Can we can compute the abstraction $h\circ so{l}^S\left(\varphi \right)$ exactly for a given system of homogeneous linear equations $\varphi$?

Geometrically speaking, the concrete solution sets $so{l}^{{\mathbb{R}}_{+}}\left(\varphi \right)$ and $so{l}^{\mathbb{R}}\left(\varphi \right)$ of homogeneous linear equation systems $\varphi$ are polytopes—i.e., finite intersections of half-spaces in ${\mathbb{R}}^{\mathit{fv}\left(\varphi \right)}$. The problem of computing boolean abstractions or sign abstraction is thus to compute the $h_{\Delta }$ abstraction of a polytope given by a linear equation system.

For any h-exact formula $\varphi$, the computation of abstractions $h\circ so{l}^S\left(\varphi \right)$ is equivalent to the computation of $so{l}^{\Delta }\left(\varphi \right)$. Since the abstract structure $\Delta$ is finite for the boolean and sign abstraction, we can compute the set of abstract solutions in at most exponential time by a naive generate and test algorithm. Finite domain constraint programming [11] can by used to avoid the naive generation of all variable assignments to $\Delta$ in many practical cases. Therefore, any algorithm for exact rewriting induces an algorithm for computing abstractions that may be feasible in practice.

1.2. Contributions

Our main result is the first algorithm for exact rewriting that applies to linear equation systems for the Boolean abstraction. Based on this algorithm, we present a novel algorithm for computing the sign abstraction of linear equation systems.

Exact Rewriting for the Boolean Abstraction. In the first step, we study exact rewriting of (homogeneous) linear equation systems for boolean abstraction. The counter example ${\varphi }_0$, for instance, can be rewritten to $h_{\mathbb{B}}$-exact formula $y\stackrel{\circ }{=}z$. The idea is to take the system of all linear consequences over ${\mathbb{R}}_{+}$ of the linear equation system. There may be infinitely many such consequences, but all of them are linear combinations of the extreme rays of the cone $so{l}^{{\mathbb{R}}_{+}}\left({\varphi }_0\right)$. Up to normalization, there are only finitely many extreme rays, which are known as the elementary modes of the linear equation system [12,13,14,15]. These can be computed by libraries from computational geometry [16] in at most exponential time. Nevertheless, the computation is often well-behaved in practice.

Based on the elementary modes (Folklore Theorem 2), we can rewrite any (homogeneous) linear equation system into quasi-positive and strongly-triangular linear equation system that is equivalent over ${\mathbb{R}}_{+}$ (Corollary 1), that can be computed in at most exponential time. As we prove, such systems are always $h_{\mathbb{B}}$-exact (Theorem 3). Hence, any system of linear equations can be converted in at most exponential time to some ${\mathbb{R}}_{+}$-equivalent $h_{\mathbb{B}}$-exact formula.

Note that $h_{\mathbb{B}}$-exact formulas may still not be $\mathbb{S}$-exact. A counter example is the strongly-triangular quasi-positive linear system $u+v\stackrel{\circ }{=}x\wedge u+v\stackrel{\circ }{=}y$. It is not $h_{\mathbb{S}}$-exact, since it entails $x\stackrel{\circ }{=}y$ over $\mathbb{R}$ but still has the abstract solution $[u/1,v/-1,x/1,y/-1]$ over $\mathbb{S}$ which maps x and y to distinct signs. Indeed, we don’t have any idea of how to do exact rewriting for the sign abstraction. The problem is that positivity is essential for our approach, and since the addition of positive and negative numbers may have any sign, $\mathbb{S}$ fails to be an algebra, making the analogous argument as in the proof of $\mathbb{B}$-exactness fail.

Extension to $h_{\mathbb{B}}$-Mixed Systems. In the second step, we introduce $h_{\mathbb{B}}$-mixed systems, which by Theorem 4 generalize on systems of 1. linear equations, 2. positive polynomial equations $p\stackrel{\circ }{=}0$, and 3. positive polynomial inequations $p\stackrel{\circ }{\ne }0$, where p is a positive polynomial without constant term. We then show our main result:

Theorem 5 (Main). Any $h_{\mathbb{B}}$-mixed systems can be converted to a $h_{\mathbb{B}}$-exact formula by converting its linear subsystem to an $h_{\mathbb{B}}$-exact formula.

The correctness of the algorithm for $h_{\mathbb{B}}$-mixed systems relies on the notion of $h_{\mathbb{B}}$-invariant formulas that we introduce. The class of $h_{\mathbb{B}}$-invariant formulas subsume systems of positive polynomial equations $p\stackrel{\circ }{=}0$ and inequations $p\stackrel{\circ }{\ne }0$, where p is a positive polynomials without constant terms.

Computing Sign Abstractions. In the third step, we present an algorithm for computing the sign abstraction of (homogeneous) systems of linear equations based on exact rewriting for the boolean abstraction (Theorem 6). For this, we decompose the sign abstraction into the boolean abstraction based on a function that is definable in first-order logic. This function decomposes real numbers into their positive part x and negative part y. At least one of these two parts must be zero, which can be expressed by the polynomial equation $x\ast y\stackrel{\circ }{=}0$. The positivity of x can be expressed by $\exists z.x\stackrel{\circ }{=}z\ast z$ and the positivity of y in analogy. In this way, we can reduce the problem of computing $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left(\varphi \right)$ to the problem of computing $h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left({\varphi }^{\prime }\right)$ for some existentially quantified $h_{\mathbb{B}}$-mixed system ${\varphi }^{\prime }$ that we can make $h_{\mathbb{B}}$-exact based on our main Theorem 5.

Application to Program Analysis. We show how to apply the computation of the sign abstraction of linear equation systems to improve the analysis of functional programs with arithmetics. For finding program errors there it can be useful to know about the possible signs of the values of program variables. We elaborate an example in the final Section 10.

Implementation. We implemented the $h_{\mathbb{B}}$-exact rewriting algorithm for $h_{\mathbb{B}}$-mixed systems from the main Theorem 5 in Python. For this we used a library from computational geometry [16] for computing elementary modes. We also used finite domain constraint programming with Minizinc [17] for computing the set of boolean solutions over logical formulas. Some successful experiments are mentioned in the related work subsection below. We did not yet implemented the algorithm for computing sign abstractions, nor its application to program analysis though.

1.3. Related Work

We start with related work by the authors, and then move to related work by others.

Change Prediction of Reaction Networks. Our main Theorem 5 was recently applied to the change prediction of reaction networks in systems biology [6]. Indeed, the development of the present article was originally motivated by this application. The problem there is to compute the difference abstraction of linear equation systems, expressing the steady state semantics of chemical reaction networks. Two difference abstractions were considered, $h_{{\Delta }_3}:{\mathbb{R}}_{+}^2\to \{△,▽,\approx \}$ and a refinement thereof $h_{{\Delta }_6}:{\mathbb{R}}_{+}^2\to \{\uparrow ,\downarrow ,~,\Uparrow ,\Downarrow ,\approx \}$. In analogy to the approach adopted for computing sign abstractions (step three above), the algorithmic approach presented there is to decompose the difference abstractions $h_{{\Delta }_3}$ and $h_{{\Delta }_6}$ into the boolean abstraction $h_{\mathbb{B}}$ and functions that are definable in first-order logic. The elaboration of this approach, however, is quite different for reflecting the nature of the difference abstractions.

Experimentation. We tested our implementation of the exact rewriting algorithm for the boolean abstraction successfully for computing difference abstractions in the application of change prediction in systems biology. The experimental results are presented in [6] are generally encouraging. They show that $h_{\mathbb{B}}$-exact rewriting based on elementary modes in combination with finite domain constraint programming may indeed avoid naive generate and test in many practical examples. In some of these examples, however, the overall computation time still took some hours.

Abstracting Reaction Networks to Boolean Networks. Independently, the authors proposed an abstraction of chemical reaction networks to boolean networks in [18], whose precision can be improved by using the $h_{\mathbb{B}}$-exact rewriting of $h_{\mathbb{B}}$-mixed equation systems.

Alternative Algorithm for Computing Sign Abstractions. An alternative algorithm for computing the sign abstraction of linear equation systems (and thus also the boolean abstraction) can be obtained by John’s overapproximation Theorem 1. It shows that it is sufficient to generate the finitely many abstract solutions in $\tau \in so{l}^{\mathbb{S}}\left(\varphi \right)$, and then to check for each of them whether there exists a concrete solution $\sigma$ such that $\tau =h_{\mathbb{S}}\circ \sigma$. To perform this latter test, note that $h\Delta \left(x\right)\stackrel{\circ }{=}1$ is equivalent to the strict inequation $x>0$ and $h_{\mathbb{S}}\left(x\right)\stackrel{\circ }{=}0$ by the equation $x\stackrel{\circ }{=}0$. Similarly, $h_{\mathbb{S}}\left(x\right)\stackrel{\circ }{=}-1$ can be defined by the strict inequation $x<0$. Whether there exists a concrete solution $\sigma \in so{l}^{\mathbb{R}}\left(\varphi \right)$ such $\tau =h\circ \sigma$ is thus equivalent to the satisfiability of $\varphi \wedge {\bigwedge }_{x\in \mathit{fv}\left(\varphi \right)}{h}_{\mathbb{S}}\left(x\right)\stackrel{\circ }{=}\tau \left(x\right)$ over $\mathbb{R}$, where $\mathit{fv}\left(\varphi \right)$ is the set of free variables of $\varphi$. The satisfiability of systems of strict linear inequations and homogeneous linear equations without constant terms over $\mathbb{R}$ are known to be decidable since at least 1926 [19]. But still, one has to generate the set of all abstract solutions $so{l}^{\mathbb{S}}\left(\varphi \right)$. The new algorithm presented above avoids generating this set.

Abstract Program Interpretation over Numerical Domains. In abstract interpretation [20], nonrelational domains permit to approximate the set of values of program variables while ignoring the relationship to the values of others. Well-known nonrelational numerical domains include the interval domain [21] describing invariants of the form ${\bigwedge }_{i=1}^m{x}_i\in [r_i,r_i^{\prime }]$ with reals $r_i\le r_i^{\prime }$ and the constant propagation domain for invariants of the form ${\bigwedge }_{i=1}^m{x}_i\stackrel{\circ }{=}{r}_i$ [22].

Abstract interpretation of relational domains may yield better approximations that with nonrelational domains, since relationships between the values of different variables can be taken into account. Well-known relational numerical domains include the polyhedral domain [4]. A polyhedron is the solution set of systems of inhomogeneous linear inequations of the form $n_1{x}_1+\dots +n_m{x}_m\le r$. Alternatively, the linear equality domain [23] was considered. These are defined by system of inhomogeneous linear equations $n_1{x}_1+\dots +n_m{x}_n\stackrel{\circ }{=}r$.

In the present paper, we study the problem of computing the sign abstraction of polytopes represented by homogeneous linear equation systems. The polytopes can be obtained by existing methods for the abstract program interpretation over the polyhedral domain. One weakness of our approach is that we study the homogeneous case only, so that we can only abstract polytope and not more general polyhedrons.

1.4. Outline

In Section 2, we recall preliminaries on homomorphisms between $\Sigma$-structures. In Section 3, the first-order logic is recalled. John’s theorem and its relation to the soundness and completeness of abstract interpretation in the classical framework are discussed in Section 4. We discuss how to make linear equation system quasipositive and strongly triangular based on elementary modes in Section 5. These properties can be used to prove $h_{\mathbb{B}}$-exactness as we show in Section 6, and thus to obtain an $h_{\mathbb{B}}$-exact rewriting of linear equation systems. We introduce the notion of $h_{\mathbb{B}}$-invariance in Section 7 and apply it in Section 8 to lift the $h_{\mathbb{B}}$-exact rewriting algorithm from linear to $h_{\mathbb{B}}$-mixed systems. This allows us to define the sign abstraction of linear equation systems on Section 9. We finally apply this result in Section 10 to the sign analysis of functional programs with arithmetic.

2. Homomorphisms on $\Sigma$-Structures

We need some basic notation from set theory and standard notion of universal algebra such as $\Sigma$-algebras, $\Sigma$-structures, and homomorphism.

For any set A and $n\in \mathbb{N}$, the set of n-tuples of elements in A is denoted by $A^n$. For finite sets A the number of elements of A is denoted by $\left|A\right|$. Furthermore, for any function $f:A\to B$ we define the function $f^2:A^2\to B^2$ such that $f^2(a,a^{\prime })=(f\left(a\right),f\left(a^{\prime }\right)$ for all $a,a^{\prime }\in A$.

2.1. $\Sigma$-Algebras

We next recall the notion of $\Sigma$-algebras. Let $\Sigma ={\cup }_{n\ge 0}{F}^{\left(n\right)}\uplus C$ be a ranked signature. We call the elements of $f\in F^{\left(n\right)}$ are called n-ary function symbols, even though we may also use them as $n+1$-ary relation symbols later on when moving to $\Sigma$-structures. The elements in $c\in C$ are called the constants of $\Sigma$.

Definition 1.

A$\Sigma$-algebra $S=(\mathit{dom}\left(S\right),{.}^S)$ consists of a set $\mathit{dom}\left(S\right)$ and an interpretation ${.}^S$ such that $c^S\in \mathit{dom}\left(S\right)$ for all $c\in C$, and $f^S:\mathit{dom}{\left(S\right)}^n\to \mathit{dom}\left(S\right)$ for all $f\in F^{\left(n\right)}$.

Let $\mathbb{B}=\{0,1\}$ be the set of booleans, $\mathbb{N}$ the set of natural numbers including 0, $\mathbb{Z}$ the set of integers, $\mathbb{R}$ the set of real numbers, and ${\mathbb{R}}_{+}$ the set of positive real numbers including 0. Note that $\mathbb{B}\subseteq \mathbb{N}\subseteq {\mathbb{R}}_{+}\subseteq \mathbb{R}$ and $\mathbb{N}\subseteq \mathbb{Z}\subseteq \mathbb{R}$. Let the addition on the reals be the binary function ${+}^{\mathbb{R}}:{\mathbb{R}}^2\to \mathbb{R}$ and the multiplication the binary function ${\ast }^{\mathbb{R}}:{\mathbb{R}}^2\to \mathbb{R}$. Let the addition on the positive real numbers ${+}^{{\mathbb{R}}_{+}}:{\mathbb{R}}_{+}^2\to {\mathbb{R}}_{+}$ be equal to the restriction ${{+}^{\mathbb{R}}}_{|{\mathbb{R}}_{+}\times {\mathbb{R}}_{+}}$ and the multiplication ${\ast }^{{\mathbb{R}}_{+}}:{\mathbb{R}}_{+}^2\to {\mathbb{R}}_{+}$ be the restriction ${{\ast }^{\mathbb{R}}}_{|{\mathbb{R}}_{+}\times {\mathbb{R}}_{+}}$.

Let ${\Sigma }_{bool}=\{+,\ast \}\cup \{0,1\}$ be the set of boolean operators where + and * are binary function symbols and 0 and 1 constants. Note that constant 0 is freely overloaded with the boolean 0 and the constant 1 with the boolean 1.

Example 1.

The set of positive reals ${\mathbb{R}}_{+}$ can be turned into a ${\Sigma }_{bool}$-algebra, in which the functions symbols are interpreted as binary functions ${+}^{{\mathbb{R}}_{+}}$ and ${\ast }^{{\mathbb{R}}_{+}}$. The constants are interpreted by themselves $0^{{\mathbb{R}}_{+}}=0$ and $1^{{\mathbb{R}}_{+}}=1$.

Example 2.

The set of Booleans $\mathbb{B}=\{0,1\}\subseteq {\mathbb{R}}_{+}$ equally defines a ${\Sigma }_{bool}$-algebra. There, the function symbols are interpreted as a disjunction ${+}^{\mathbb{B}}={\vee }^{\mathbb{B}}$ and conjunction ${\ast }^{\mathbb{B}}={\wedge }^{\mathbb{B}}$ on Booleans. The constants are interpreted by themselves $0^{\mathbb{B}}=0$ and $1^{\mathbb{B}}=1$.

2.2. $\Sigma$-Structures

We next recall the usual generalization of $\Sigma$-algebras to $\Sigma$-structures. The objective is to generalize from functions to relations. For this, we consider n-ary function symbols as $n+1$-ary relation symbols.

Definition 2.

A$\Sigma$-structure $\Delta =(\mathit{dom}(\Delta ),{.}^{\Delta })$ consists of a set $\mathit{dom}(\Delta )$ and an interpretation ${.}^{\Delta }$ such that $c^{\Delta }\in \mathit{dom}(\Delta )$ for all $c\in C$ and $f^{\Delta }\subseteq \mathit{dom}{(\Delta )}^{n+1}$ for all $f\in F^{\left(n\right)}$.

Clearly, any $\Sigma$-algebra is also a $\Sigma$-structure. Note also that symbols in $F^{\left(0\right)}$ are interpreted as monadic relations, i.e., as subsets of the domain, in contrast to constants in C that are interpreted as elements of the domain.

We denote the subtraction on the reals by the binary function ${-}^{\mathbb{R}}:{\mathbb{R}}^2\to \mathbb{R}$ and the division on the reals by the ternary relation ${/}^{\mathbb{R}}\subseteq {\mathbb{R}}^2\times \mathbb{R}$. Note that division by zero is undefined. Note also that subtraction on ${\mathbb{R}}_{+}$ would yield only a partial function.

Let ${\Sigma }_{arith}=\{+,\ast ,-,/\}\cup \{0,1\}$ be the arithmetic signature, where 0 and 1 are constants, and all other operators are binary function symbols. Again, we freely overlead to constant 0 with real number 0 and the constant 1 with the real number 1.

Example 3.

The set of reals $\mathbb{R}$ can be turned into a ${\Sigma }_{arith}$-structure, with the interpretation of the binary functions symbols as the ternary relations ${+}^{\mathbb{R}}$, ${\ast }^{\mathbb{R}}$, ${-}^{\mathbb{R}}$, ${/}^{\mathbb{R}}$. The constants are interpreted by themselves $0^{\mathbb{R}}=0$ and $1^{\mathbb{R}}=1$. Note that ${/}^{\mathbb{R}}$ is a partial but not a total function, since division by 0 is not defined. So we must see ${/}^{\mathbb{R}}$ as a ternary relation, so that $\mathbb{R}$ is not a ${\Sigma }_{arith}$-algebra. It still is a ${\Sigma }_{bool}$-algebra though.

Example 4.

The set of signs $\{-1,0,1\}\subseteq \mathbb{R}$ can be turned into a ${\Sigma }_{arith}$-structure $\mathbb{S}=(\{-1,0,1\},{.}^{\mathbb{S}})$ with the interpretation ${+}^{\mathbb{S}}$, ${-}^{\mathbb{S}}$, ${\ast }^{\mathbb{S}}$ and, ${/}^{\mathbb{S}}$ given in Figure 1. The constants are interpreted by themselves $0^{\mathbb{S}}=0$ and $1^{\mathbb{S}}=1$. Note that all ${+}^{\mathbb{S}}$ contains $(-1,1,-1)$, $(-1,1,1)$ and $(-1,1,0)$ meaning that the sum of a strictly negative and a strictly positive real has a sign in $-1{+}^{\mathbb{S}}1$, so it may either be strictly positive, strictly negative, or zero. So $\mathbb{S}$ is a ${\Sigma }_{arith}$-structure and even when restricting the signature to ${\Sigma }_{bool}$ it remains a ${\Sigma }_{bool}$-structure that is not a ${\Sigma }_{bool}$-algebra.

2.3. Homomorphisms

We recall the standard notion of homomorphism for $\Sigma$-structures which can also be applied to $\Sigma$-algebras.

Definition 3.

A homomorphism between two Σ-structures S and Δ is a function $h:\mathit{dom}\left(S\right)\to \mathit{dom}(\Delta )$ such that for $c\in C$, $n\in \mathbb{N}$, $f\in F^{\left(n\right)}$, and $s_1,\dots ,s_{n+1}\in \mathit{dom}\left(S\right)$:

1

$h\left(c^S\right)=c^{\Delta }$, and

2

if $(s_1,\dots ,s_{n+1})\in f^S$ then $(h\left(s_1\right),\dots ,h\left(s_{n+1}\right))\in f^{\Delta }$.

We can convert any $n+1$-ary relation to a n-ary set valued functions. In this way, any n-function is converted to a n-ary set valued n-functions. In other words, functions of type $D^n\to D$ are converted to functions of type $D^n\to 2^D$ where $D=\mathit{dom}(\Delta )$. In set-valued notation, the second condition on homomorphism can then be rewritten equivalently as $h\left(f^S(s_1,\dots ,s_n)\right)\subseteq f^{\Delta }(h\left(s_1\right),\dots ,h\left(s_n\right))$. A homomorphism for $\Sigma$-algebras thus satisfies $h\left(c^S\right)=c^{\Delta }$ and for all function symbols $f\in F^{\left(n\right)}$ and $s_1,\dots ,s_n\in \mathit{dom}\left(S\right)$ it satisfies $h\left(f^S(s_1,\dots ,s_n)\right)=f^{\Delta }(h\left(s_1\right),\dots ,h\left(s_n\right)).$

The boolean abstraction is the function $h_{\mathbb{B}}:{\mathbb{R}}_{+}\to \mathbb{B}$ with $h_{\mathbb{B}}\left(0\right)=0$ and $h_{\mathbb{B}}\left(r\right)=1$ if $r>0$.

Lemma 1.

The boolean abstraction $h_{\mathbb{B}}$ is a homomorphism between ${\Sigma }_{bool}$-algebras.

Proof. 

For all $r,r^{\prime }\in {\mathbb{R}}_{+}$ we have:

$$\begin{array}{ccccccc}\hfill h_{\mathbb{B}}\left(r{+}^{{\mathbb{R}}_{+}}{r}^{\prime }\right)=1& \iff \hfill & r{+}^{{\mathbb{R}}_{+}}{r}^{\prime }\ne 0\hfill & \iff \hfill & r\ne 0\vee r^{\prime }\ne 0\hfill & \iff \hfill & h_{\mathbb{B}}\left(r\right)=1\vee h_{\mathbb{B}}\left(r^{\prime }\right)=1\hfill \\ \hfill h_{\mathbb{B}}\left(r{\ast }^{{\mathbb{R}}_{+}}{r}^{\prime }\right)=1& \iff \hfill & r{\ast }^{{\mathbb{R}}_{+}}{r}^{\prime }\ne 0\hfill & \iff \hfill & r\ne 0\wedge r^{\prime }\ne 0\hfill & \iff \hfill & h_{\mathbb{B}}\left(r\right)=1\wedge h_{\mathbb{B}}\left(r^{\prime }\right)=1\hfill \end{array}$$

Hence, $h_{\mathbb{B}}\left(r{+}^{{\mathbb{R}}_{+}}{r}^{\prime }\right)=h_{\mathbb{B}}\left(r\right){+}^{\mathbb{B}}{h}_{\mathbb{B}}\left(r^{\prime }\right)$ and $h_{\mathbb{B}}\left(r{\ast }^{{\mathbb{R}}_{+}}{r}^{\prime }\right)=h_{\mathbb{B}}\left(r\right){\ast }^{\mathbb{B}}{h}_{\mathbb{B}}\left(r^{\prime }\right)$. Finally, for both constants $c\in C$ we have that $h_{\mathbb{B}}\left(c^{{\mathbb{R}}_{+}}\right)=h_{\mathbb{B}}\left(c\right)=c=c^{\mathbb{B}}$. □

The sign abstraction is the function $h_{\mathbb{S}}:\mathbb{R}\to \mathbb{S}$ with $h_{\mathbb{S}}\left(0\right)=0$, $h_{\mathbb{S}}\left(r\right)=-1$ for all strictly negative reals $r<0$ and $h_{\mathbb{S}}\left(r\right)=1$ for all strictly positive reals $r>0$.

Lemma 2.

The sign abstraction h_𝕊 is a homomorphism between ${\Sigma }_{arith}$-structures.

Proof. 

Let $r,r^{\prime }\in \mathbb{R}$. For the multiplication we have $h_{\mathbb{S}}\left(r{\ast }^{\mathbb{R}}{r}^{\prime }\right)=h_{\mathbb{S}}\left(r\right){\ast }^{\mathbb{R}}{h}_{\mathbb{S}}\left(r^{\prime }\right)$ and thus $h_{\mathbb{S}}\left(r{\ast }^{\mathbb{R}}{r}^{\prime }\right)\in \left\{h_{\mathbb{S}}\left(r\right){\ast }^{\mathbb{R}}{h}_{\mathbb{S}}\left(r^{\prime }\right)\right\}=h_{\mathbb{S}}\left(r\right){\ast }^{\mathbb{S}}{h}_{\mathbb{S}}\left(r^{\prime }\right)$. For the addition, we have to distinguish cases. If r and $r^{\prime }$ have the same sign, so $r{+}^{\mathbb{R}}{r}^{\prime }$ has the same sign, so that we have $h_{\mathbb{S}}\left(r{+}^{\mathbb{R}}{r}^{\prime }\right)\in h_{\mathbb{S}}\left(r\right){+}^{\mathbb{S}}{h}_{\mathbb{S}}\left(r^{\prime }\right)$. If $r>0$ and $r^{\prime }<0$ or vice versa then we have $h_{\mathbb{S}}\left(r\right){+}^{\mathbb{S}}{h}_{\mathbb{S}}\left(r^{\prime }\right)=\mathbb{S}$ so that $h_{\mathbb{S}}\left(r{+}^{\mathbb{R}}{r}^{\prime }\right)\in \mathbb{S}=h_{\mathbb{S}}\left(r\right){+}^{\mathbb{S}}{h}_{\mathbb{S}}\left(r^{\prime }\right)$. The treatment of ${-}^{\mathbb{S}}$ and ${/}^{\mathbb{S}}$ is similar. For the constants, we have $h_{\mathbb{S}}\left(0^{\mathbb{R}}\right)=0^{\mathbb{S}}$ and $h_{\mathbb{S}}\left(1^{\mathbb{R}}\right)=1^{\mathbb{S}}$. □

3. First-Order Logic

We recall the syntax and semantics of first-order logic with equality. For this, we fix a countably infinite set of variables $\mathcal{V}$ that will be ranged over by $x,y,z$.

3.1. Expressions

Given a ranked signature with constants and function symbols $\Sigma =C\cup {\bigcup }_{n\ge 0}{F}^{\left(n\right)}$, the set of $\Sigma$-expressions contains all terms that can be constructed from constants and variables by using function symbols:

$e_1,\dots ,e_n\in {\mathcal{E}}_{\Sigma }$

::= $x\mid c\mid f(e_1,\dots ,e_n)$

where $c\in C$, $n\ge 0$, $f\in F^{\left(n\right)}$, $x\in \mathcal{V}$

Let $\mathit{fv}\left(e\right)$ be the set of all variables that occur in e. Given a subset $V\subseteq \mathcal{V}$ let ${\mathcal{E}}_{\Sigma }\left(V\right)$ be the subset of expression $e\in {\mathcal{E}}_{\Sigma }$ with $\mathit{fv}\left(e\right)\subseteq V$.

The semantics of $\Sigma$-expressions is defined in Figure 2. For any $\Sigma$-structure S and variable assignment $\sigma :V\to \mathit{dom}\left(S\right)$, any expression $e\in {\mathcal{E}}_{\Sigma }\left(V\right)$ denotes a set of values $〚e{〛}^{\sigma ,S}\subseteq \mathit{dom}\left(S\right)$. This set is defined recursively by set-valued interpretation of the operators of the expressions in the structure S. If S is a $\Sigma$-algebra, then the result will always be a singleton.

3.2. Logic Formulas

The set of first-order formulas is the set of terms constructed with the usual first-order connectives from equations with symbols in $\Sigma$ and variables in $\mathcal{V}$:

$\varphi \in {\mathcal{F}}_{\Sigma }^{}$

::= $e\stackrel{\circ }{=}{e}^{\prime }\mid \exists x.\varphi \mid \varphi \wedge \varphi \mid \neg \varphi$

where $e,e^{\prime }\in {\mathcal{E}}_{\Sigma }$ and $x\in \mathcal{V}$

A $\Sigma$-formula $\varphi \in {\mathcal{F}}_{\Sigma }^{}$ is a term, which either is a $\Sigma$-equation $e\stackrel{\circ }{=}{e}^{\prime }$ with variables in $\mathcal{V}$, an existentially quantified formula $\exists x.\varphi$, a conjunction $\varphi \wedge {\varphi }^{\prime }$, or a negation $\neg \varphi$. A system of $\Sigma$-equations is a conjunction of equations $e_1\stackrel{\circ }{=}{e}_1^{\prime }\wedge \dots \wedge e_n\stackrel{\circ }{=}{e}_n^{\prime }$ where $e_1,e_1^{\prime },\dots ,e_n,e_n^{\prime }\in {\mathcal{E}}_{\Sigma }$.

The set of free variables $\mathit{fv}\left(\varphi \right)$ contains all those variables of $\varphi$ that occur outside the scope of any existential quantifier in $\varphi$. Given a subset $V\subseteq \mathcal{V}$ we write ${\mathcal{F}}_{\Sigma }^{}\left(V\right)$ for the subset of formulas $\varphi \in {\mathcal{F}}_{\Sigma }^{}$ such that $\mathit{fv}\left(\varphi \right)\subseteq V$.

First-order formulas can be defined for providing the missing logical operators. Firstly, we can define disjunctions $\varphi \vee {\varphi }^{\prime }{=}_{\mathrm{def}}\neg (\neg \varphi \wedge \neg {\varphi }^{\prime })$ and implications $\varphi \to {\varphi }^{\prime }{=}_{\mathrm{def}}\neg \varphi \vee {\varphi }^{\prime }$, and secondly, universally quantified formulas $\forall x.\varphi {=}_{\mathrm{def}}\neg \exists x.\neg \varphi$. Note that these formulas are not negation-free (and thus John’s theorem cannot be applied to them). Third, we define the valid formula $\mathit{true}{=}_{\mathrm{def}}\exists x.x\stackrel{\circ }{=}x$. Fourth, we write ${\bigwedge }_{i=1}^n{\varphi }_i$ instead of ${\varphi }_1\wedge \dots \wedge {\varphi }_n$. In the case $n=0$ the conjunction is $\mathit{true}$. Fifth, for any vector of variables $\mathbf{y}=({\mathbf{y}}_1,\dots ,{\mathbf{y}}_n)\in {\mathcal{V}}^n$ we will write $\exists \mathbf{y}.\varphi$ instead of $\exists {\mathbf{y}}_1\dots \exists {\mathbf{y}}_n.\varphi$.

For any $V\subseteq \mathcal{V}$, the semantics of first-order formulas $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ for a $\Sigma$-structure S and a variable assignment $\sigma :V\to \mathit{dom}\left(S\right)$ is the truth value $〚\varphi {〛}^{\sigma ,S}\in \mathbb{B}$ defined in Figure 3.

Note that the equality symbol $\stackrel{\circ }{=}$ is interpreted as nondisjointness, i.e., an equation $e\stackrel{\circ }{=}{e}^{\prime }$ is true if and only if $〚e{〛}^{\sigma ,S}\cap 〚e^{\prime }{〛}^{\sigma ,S}\ne \varnothing$. In the case of $\Sigma$-algebras, the equality symbol $\stackrel{\circ }{=}$ is indeed interpreted as equality of singletons. In the case of more general $\Sigma$-structures, though, it is not interpreted as set equality.

The set of solutions with domain V of a formula $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ over a $\Sigma$-algebra S is:

$$so{l}_V^S\left(\varphi \right)=\{\sigma :V\to \mathit{dom}\left(S\right)\mid 〚\varphi {〛}^{\sigma ,S}=1\}$$

If $V=\mathit{fv}\left(\varphi \right)$ we omit the index V, i.e., $so{l}^S\left(\varphi \right)=so{l}_V^S\left(\varphi \right)$.

Two formulas $\varphi ,{\varphi }^{\prime }\in {\mathcal{F}}_{\Sigma }^{}$ are called S-equivalent if they have the same solution sets over S on $V=\mathit{fv}\left(\varphi \right)\cup \mathit{fv}\left({\varphi }^{\prime }\right)$, that is $so{l}_V^S\left(\varphi \right)=so{l}_V^S\left({\varphi }^{\prime }\right)$. Note that $y\stackrel{\circ }{=}y$ is equivalent to $z\stackrel{\circ }{=}z$ and also to $\mathit{true}$, i.e., to $\exists x.x\stackrel{\circ }{=}x$.

3.3. Examples

Since $\mathbb{B}\subseteq {\mathbb{R}}_{+}$ we can define the boolean abstraction by a formula $y\stackrel{\circ }{=}{h}_{\mathbb{B}}\left(x\right)$ in ${\mathcal{F}}_{{\Sigma }_{bool}}^{}$ over ${\mathbb{R}}_{+}$ with two variables $x,y\in \mathcal{V}$:

$$(x\stackrel{\circ }{=}0\wedge y\stackrel{\circ }{=}0)\vee (\neg x\stackrel{\circ }{=}0\wedge y\stackrel{\circ }{=}1)$$

Since $\mathbb{S}\subseteq \mathbb{R}$ we can define the sign abstraction by a formula $y\stackrel{\circ }{=}{h}_{\mathbb{S}}\left(x\right)$ in ${\mathcal{F}}_{{\Sigma }_{bool}}^{}$ over $\mathbb{R}$ with two variables $x,y\in \mathcal{V}$:

$$\begin{array}{c}\hfill (x\stackrel{\circ }{=}0\wedge y\stackrel{\circ }{=}0)\vee (x>0\wedge y\stackrel{\circ }{=}1)\vee (x<0\wedge y+1\stackrel{\circ }{=}0)\end{array}$$

where:

$$\begin{array}{ccc}\hfill x\ge 0& {=}_{\mathrm{def}}\hfill & \exists z.x\stackrel{\circ }{=}z\ast z\hfill \\ \hfill x>0& {=}_{\mathrm{def}}\hfill & x\ge 0\wedge \neg \left(x\stackrel{\circ }{=}0\right)\hfill \\ \hfill x<0& {=}_{\mathrm{def}}\hfill & \neg x\ge 0\hfill \end{array}$$

These definitions illustrate that both abstraction are closely related to strict inequations $x>0$ and $x<0$. The boolean abstraction is concerned with strict positivity $x>0$, while the sign abstraction is also concerned with strict negativity $x<0$.

3.4. Semantic Properties of Free and Bound Variables

We need the following two standard lemmas on the role of free and bound variables for the solution sets of logic formulas. For any subset of variable assignments R of type $V^{\prime }\to \mathit{dom}\left(S\right)$ and any disjoint sets of variables $V\cap V^{\prime }=\varnothing$ we define ${\mathit{ext}}_V^S\left(R\right)=\{\sigma \cup {\sigma }^{\prime }\mid \sigma :V\to \mathit{dom}\left(S\right),{\sigma }^{\prime }\in R\}$.

Lemma 3

(Cylindrification). If $V\cap \mathit{fv}\left(\varphi \right)=\varnothing$ then $so{l}_{V\cup \mathit{fv}\left(\varphi \right)}^S\left(\varphi \right)={\mathit{ext}}_V^S\left(so{l}^S\left(\varphi \right)\right)$.

Proof. 

We can show that $〚e{〛}^{\sigma ,S}=〚e{〛}^{{\sigma }_{\left|\mathit{fv}\right(e)},S}$ for all expressions $e\in {\mathcal{E}}_{\Sigma }$ with $\mathit{fv}\left(e\right)$ disjoint to V and any variable assignment $\sigma :\mathit{fv}\left(e\right)\cup V\to \mathit{dom}\left(S\right)$ by induction on the structure of expressions. From this, we can prove for all formulas $\varphi \in {\mathcal{F}}_{\Sigma }^{}$ such that $\mathit{fv}\left(\varphi \right)$ is disjoint from V and $\sigma :\mathit{fv}\left(\varphi \right)\cup V\to \mathit{dom}\left(S\right)$ that $〚\varphi {〛}^{\sigma ,S}=〚\varphi {〛}^{{\sigma }_{\left|\mathit{fv}\right(\varphi )},S}$ by induction on the structure of $\Sigma$-formulas. This implies the lemma. □

The projection ${\pi }_a\left(f\right)$ of a function $f:A\to B$ is its restriction $f_{|A\backslash \{a\}}$. The projection of a set F of functions $f:A\to B$ is ${\pi }_a\left(F\right)=\{{\pi }_a\left(f\right)\mid f\in F\}$.

Lemma 4

(Quantification is projection). $so{l}^S(\exists x.\varphi )={\pi }_x\left(so{l}^S\left(\varphi \right)\right)$.

Proof. 

This is follows from the semantics of existential quantified formulas as follows:

$$so{l}^S(\exists x.\varphi )=\{{\sigma }_{\left|\mathit{fv}\right(\varphi )\backslash \{x\}}\mid \sigma \in so{l}^S\left(\varphi \right)\}={\pi }_x\left(so{l}^S\left(\varphi \right)\right)$$

□

4. Abstract Interpretation

We recall the notion of $\Sigma$-abstractions and use them for abstracting sets of concrete solutions of logic formulas within the usual framework of abstract interpretation. Due to John’s theorem, this abstraction can be soundly approximated by the abstract interpretation of logic formulas in the target structure of the $\Sigma$-abstraction. We will argue that John’s overapproximation shows the soundness of abstract interpretation in the classical framework of Cousot & Cousot [1]. We will then introduce the notion of exactness of a logic formula with respect to a $\Sigma$-abstraction and relate it to the completeness of abstract interpretation.

4.1. John’s Overapproximation for $\Sigma$-Abstractions

The notion of $\Sigma$-abstraction from [6] generalizes at the same time over the boolean abstraction and the sign abstraction.

Definition 4.

A Σ-abstraction is a homomorphism $h:S\to \Delta$ between Σ-structures such that $\mathit{dom}(\Delta )\subseteq \mathit{dom}\left(S\right)$.

The boolean abstraction $h_{\mathbb{B}}$ is a ${\Sigma }_{bool}$-abstraction by Lemma 1. The sign abstraction $h_{\mathbb{S}}$ is a ${\Sigma }_{bool}$-abstraction by Lemma 2.

Let $h:S\to \Delta$ be a $\Sigma$-abstraction and $V\subseteq \mathcal{V}$. For any subset of assignments R of type $V\to \mathit{dom}\left(S\right)$, we define the abstraction:

$$h\circ R=\{h\circ \sigma :V\to \mathit{dom}(\Delta )\mid \sigma \in R\}$$

Theorem 1

(John’s Overapproximation [6,8,9]). For any Σ-abstraction $h:S\to \Delta$ between Σ-structures and any negation-free Σ-formula $\varphi \in {\mathcal{F}}_{\Sigma }^{}$:

$$h\circ so{l}^S\left(\varphi \right)\subseteq so{l}^{\Delta }\left(\varphi \right)$$

John’s theorem states that the abstraction with respect to h of the concrete solution set of a first-order formula can be overapproximated by abstract interpretation of the formula in the target structure of h.

We only give a brief sketch of the full proof, which can be found in [6]. Let $V=\mathit{fv}\left(\varphi \right)$ and $\sigma :V\to \mathit{dom}\left(S\right)$. For any expression $e\in {\mathcal{E}}_{\Sigma }\left(V\right)$, we can show $h(〚e{〛}^{\sigma ,S})=〚e{〛}^{h\circ \sigma ,\Delta }$ by induction on the structure of e. It then follows for any negation-free formula $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ that $〚\varphi {〛}^{\sigma ,S}\le 〚\varphi {〛}^{h\circ \sigma ,\Delta }$. This is equivalent to that $\{h\circ \sigma \mid \sigma \in so{l}_V^S\left(\varphi \right)\}\subseteq so{l}_V^{\Delta }\left(\varphi \right)$ and thus $h\circ so{l}_V^S\left(\varphi \right)\subseteq so{l}_V^{\Delta }\left(\varphi \right)$. Since $V=\mathit{fv}\left(\varphi \right)$, it follows that $h\circ so{l}^S\left(\varphi \right)\subseteq so{l}^{\Delta }\left(\varphi \right)$ as required.

4.2. Exactness of $\Sigma$-Formulas for $\Sigma$-Abstractions

As a new contribution, we introduce the notion of exactness of first-order formulas with respect to a $\Sigma$-abstraction.

Definition 5

(h-Exactness). Let $h:S\to \Delta$ be a Σ-abstraction and $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ a formula. We call ϕ h-exact with respect to V if h $\circ so{l}_V^S\left(\varphi \right)=so{l}_V^{\Delta }\left(\varphi \right).$ We call ϕ h-exact if ϕ is h-exact with respect to $\mathit{fv}\left(\varphi \right)$.

For instance, the linear equation system $\varphi$ equal to $x+y\stackrel{\circ }{=}x+z$ is neither $h_{\mathbb{B}}$-exact nor $h_{\mathbb{S}}$-exact. However it is equivalent to $y\stackrel{\circ }{=}z$ which is both $h_{\mathbb{B}}$-exact and $h_{\mathbb{S}}$-exact. To see this note that $\tau =[x/1,y/1,z/0]$ belongs to $so{l}^{\mathbb{B}}\left(\varphi \right)$ but not to $h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\varphi \right)$ since $\tau \left(y\right)\ne \tau \left(z\right)$. The same assignment also belongs to $so{l}^{\mathbb{S}}\left(\varphi \right)$ but not to $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left(\varphi \right)$ since $\tau \left(y\right)\ne \tau \left(z\right)$.

4.3. Soundness and Completeness of Abstract Interpretation

John’s theorem is related to the soundness of abstract interpretation and the notion of exactness to its completeness. To state the precise relationship, we need to embed our setting into the classical framework of abstract interpretation [1,10].

When considering formulas as programs, the usual framework of abstract interpretation of programs applies to the interpretation of the formulas (programs) in the target structure of the $\Sigma$-abstraction. More formally, we fix a finite subset of variables $V\subseteq \mathcal{V}$ and consider the subset of formulas as programs:

$$\mathcal{P}=\{\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)\mid \varphi \mathrm{is}\mathrm{negation}-\mathrm{free}\}$$

The semantics of a program $\varphi \in \mathcal{P}$ over a given $\Sigma$-structure S is the set of its solutions over S:

$$〚\varphi {〛}^{}=so{l}^S\left(\varphi \right)$$

The range of the semantics mapping is the space of concrete values $C=2^{\{\sigma \mid \sigma :V\to \mathit{dom}(S\left)\right\}}$. Note that $(C,\subseteq ,\cap ,\cup )$ is a complete lattice. An abstract interpretation of a program $\varphi \in \mathcal{P}$ maps $\varphi$ to the set of its solutions over $\Delta$:

$$〚\varphi {〛}^{♯}=so{l}^{\Delta }\left(\varphi \right)$$

The range of the abstract interpretation is the abstract domain $A=2^{\{\tau \mid \tau :V\to \mathit{dom}(\Delta \left)\right\}}$. Clearly, $(A,\subseteq ,\cap ,\cup )$ is also a complete lattice. We define the abstraction function ${\alpha }_h:C\to A$ of our Galois connection such that for subsets of concrete assignments $R\subseteq C$:

$${\alpha }_h\left(R\right)=h\circ R$$

Definition 6

(Cousot & Cousot [1], Giacobazzi, Ranzato & Scozzari [10]). An abstract interpretation $〚.{〛}^{♯}:\mathcal{P}\to A$ is sound for an abstraction $\alpha :C\to A$ with respect to the program semantics $〚.{〛}^{}:\mathcal{P}\to C$ if for all programs $\varphi \in \mathcal{P}$ it holds that $\alpha (〚\varphi {〛}^{})\subseteq 〚\varphi {〛}^{♯}$. It is complete if all programs $\varphi \in \mathcal{P}$ satisfy $\alpha (〚\varphi {〛}^{})=〚\varphi {〛}^{♯}$.

John’s theorem states that the abstract interpretation ${\alpha }_h$ of negation free-formulas $\varphi \in \mathcal{P}$ over $\Delta$ is sound for the abstraction of $so{l}^S\left(\varphi \right)$ with respect to the $\Sigma$-abstraction $h:S\to \Delta$. Furthermore, if all formulas of $\mathcal{P}$ are h-exact then abstract interpretation over $\Delta$ is complete for abstraction ${\alpha }_h$. As illustrated above, abstract interpretation over $\mathbb{B}$ fails to be complete for the abstraction ${\alpha }_{h_{\mathbb{B}}}$, and similarly, abstract interpretation over $\mathbb{S}$ fails to be complete for the abstraction ${\alpha }_{h_{\mathbb{S}}}$. Note that the completeness of abstract interpretations was largely studied in the context of program analysis (see e.g., Section 8 of [10] for an overview).

In the present article, we study the problem of exact rewriting for $h_{\mathbb{B}}$. The question is how to rewrite a ${\Sigma }_{bool}$-formula into a $h_{\mathbb{B}}$-exact formula that is ${\mathbb{R}}_{+}$-equivalent. Note that exact rewriting of linear equation system for $h_{\mathbb{B}}$ is a different problem than to decide whether abstract interpretation is complete for ${\alpha }_{h_{\mathbb{B}}}$ on linear equation systems. Still, both notions are closely related: exact rewriting can help to improve the precision of abstract interpretation just in the case where it is not already complete, i.e., maximally precise. Otherwise, exact rewriting is trivial.

In the case of the sign abstraction, we do not have any algorithmic idea of how to do exact rewriting for linear equation systems. Therefore, we study the easier problem of exact rewriting for the boolean abstraction of linear equation systems in the first place. Given an $h_{\mathbb{B}}$-exact formula $\varphi$, we can compute the abstraction $h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\varphi \right)=so{l}^{\mathbb{B}}\left(\varphi \right)$ by finite domain constraints programming. We then use exact rewriting for the boolean abstraction to compute sign abstractions of linear equation systems $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left(\varphi \right)$, rather than relying on exact rewriting for the sign abstraction itself. For this, we use first-order definitions beside of finite domain constraint programming.

4.4. Galois Connection

We finally introduce the concretization operation that corresponds to the abstraction of the solution set of a logic formula with respect to a $\Sigma$-abstraction, and show that the pair of abstraction and concretization forms a Galois connection.

Given a $\Sigma$-abstraction $h:S\to \Delta$, and a set R of variable assignments to $\mathit{dom}(\Delta )$, we define the left-decomposition of R with respect to h as the following set of variable assignments to $\mathit{dom}\left(S\right)$:

$$\begin{array}{cc}\hfill h\circ -R& {=}_{\mathrm{def}}\{\sigma \mid h\circ \sigma \in R\}\hfill \end{array}$$

So let ${\alpha }_h:C\to A$ be the abstraction induced by $\Sigma$-abstraction h. We define the corresponding concretization function ${\gamma }_h:A\to C$ such that for all abstract assignments $R\subseteq A$:

$${\gamma }_h\left(R\right)=h\circ -R{=}_{\mathrm{def}}\{\sigma \in C\mid h\circ \sigma \in R\}$$

Lemma 5.

$(A,C,{\alpha }_h,{\gamma }_h)$ is a Galois connection, i.e., for all $R\in C$ and $T\in A$:

$${\alpha }_h\left(R\right)\subseteq T\mathit{if}\mathit{and}\mathit{only}\mathit{if}R\subseteq {\gamma }_h\left(T\right)$$

Proof. 

If $h\circ R\subseteq T$ then $h\circ -h\circ R\subseteq \circ -T$ and since $R\subseteq h\circ -h\circ R$ we have $R\subseteq h\circ -T$. If conversely $R\subseteq h\circ -T$ then $h\circ R\subseteq h\circ h\circ -T$ and since $h\circ h\circ -T=T$ it follows that $h\circ R\subseteq T$. □

5. Equation Systems, Positivity, and Triangularity

We study systems of ${\Sigma }_{bool}$-equations for positivity and triangularity. These notions will be essential for showing $\mathbb{B}$-exactness. We are not only interested in homogeneous linear equations but also in more general polynomial equations without constant term.

5.1. Classes of Equation Systems

Let $e_1,\dots ,e_n\in {\mathcal{E}}_{{\Sigma }_{bool}}$ be a sequence of expressions and $n\in \mathbb{N}$. If $n\ne 0$ we define ${\sum }_{i=1}^n{e}_i{=}_{\mathrm{def}}{e}_1+\dots +e_n$ and ${\prod }_{i=1}^n{e}_i{=}_{\mathrm{def}}{e}_1\ast \dots \ast e_n$. For $n=0$, we define ${\sum }_{i=1}^n{e}_i=0$ and ${\prod }_{i=1}^n{e}_i=1$. Furthermore, for any expression $e\in {\mathcal{E}}_{{\Sigma }_{bool}}$ we define:

$$ne{=}_{\mathrm{def}}\sum _{i=1}^{n}e\mathrm{and}{e}^n{=}_{\mathrm{def}}\prod _{i=1}^{n}e$$

A polynomial (with natural coefficients) is a ${\Sigma }_{bool}$-expression of the following form:

$$\sum _{j=1}^l{n}_j\prod _{k=1}^{i_j}{x}_{j,k}^{m_{j,k}}$$

where l and $i_j$ are natural numbers, $x_{1,1},\dots ,x_{l,i_l}$ variables, all $n_j\ne 0$ are natural numbers called the coefficients, and all $m_{j,k}\ne 0$ are natural numbers called the exponents. The products ${\prod }_{k=1}^{i_j}{x}_{j,k}^{m_{j,k}}$ are called the monomials of the polynomial.

Definition 7.

A polynomial ${\sum }_{j=1}^l{n}_j{\prod }_{k=1}^{i_j}{x}_{j,k}^{m_{j,k}}$ with natural coefficients $n_j\ne 0$ has no constant term if none of its monomials are equal to 1, i.e., $i_j\ne 0$ for all $1\le j\le l$. It is linear if all its monomials are variables, i.e., $i_j=1$ and $m^{j,1}=\dots =m^{j,i_j}=1$ for all $1\le j\le l$.

A polynomial equation is a ${\Sigma }_{bool}$-equation $p\stackrel{\circ }{=}{p}^{\prime }$ between polynomials. A polynomial equation system is a system of polynomial equations.

Linear polynomials have the form ${\sum }_{j=1}^l{n}_j{x}_{j,1}$ where l and all $n_j\ne 0$ are naturals and all $x_{j,1}$ are variables. In particular, linear polynomials do not have a constant term. Note that the constant 0 is equal to the linear polynomial with $l=0$. A (homogeneous) linear equation is a polynomial equation with linear polynomials, so without constant terms. A (homogeneous) linear equation system is a system of linear equations.

A (homogeneous) integer matrix equation has the form $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$ where A is a $n\times m$ matrix of integers for some naturals $m,n$ such that $\mathbf{y}\in {\mathcal{V}}^m$ and $\mathbf{0}\in {\left\{0\right\}}^n$. Any integer matrix equation can be turned into a linear equation system with natural coefficients, by bringing the negative coefficients positively on the right-hand side. For instance, the linear integer matrix equation:

$$\left(\begin{array}{cc}3\hfill & \hfill 0\\ 2\hfill & \hfill -5\end{array}\right)\left(\begin{array}{c}x\hfill \\ y\hfill \end{array}\right)\stackrel{\circ }{=}\left(\begin{array}{c}0\hfill \\ 0\hfill \end{array}\right)$$

corresponds to the following system of linear ${\Sigma }_{bool}$-equations:

$$3x\stackrel{\circ }{=}0\wedge 2x\stackrel{\circ }{=}5y$$

Therefore, we will sometimes confuse an integer matrix equations with the corresponding system of linear ${\Sigma }_{bool}$-equations. Conversely, any system of linear ${\Sigma }_{bool}$-equations can be converted into a integer matrix equation by moving the positive right-hand sides negatively to the left and factorizing the expressions for the different occurrences of the same variable.

5.2. Positivity and Triangularity

such that $\sigma \left(y\right),\sigma \left(y^{\prime }\right)$ We next define positivity and triangularity properties for equation systems. These are key properties to show $\mathbb{B}$-exactness of linear equation systems.

Definition 8.

A ${\Sigma }_{bool}$-equation is called positive if it has the form $e\stackrel{\circ }{=}0$ and quasi-positive if it has the form $e\stackrel{\circ }{=}ny$, where $n\in \mathbb{N}$, $y\in \mathcal{V}$, and $e\in {\mathcal{E}}_{{\Sigma }_{bool}}$. We call a system of ${\Sigma }_{bool}$-equations positive respectively quasi-positive if all its equations are.

This definition makes sense, since all constants in ${\Sigma }_{bool}$-expressions are positive and all operators of ${\Sigma }_{bool}$-expressions preserve positivity. Note also that any positive equation is quasipositive since the constant 0 is equal to the polynomial $0y$.

This above system of linear equations is quasipositive, but not positive since $5y$ appears on a right-hand side. More generally, the linear equation system for a integer matrix equation $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$ is positive if and only if all integers in A are positive, and quasipositive if each line of A contains at most one negative integer.

Definition 9.

We call a quasipositive system of ${\Sigma }_{bool}$-equations triangular if it has the form ${\bigwedge }_{l=1}^n{e}_l\stackrel{\circ }{=}{n}_l{y}_l$ such that the variables $y_l$ are l-fresh for all $1\le l\le n$, i.e., $y_l\notin \mathit{fv}\left({\bigwedge }_{i=1}^{l-1}{e}_i\stackrel{\circ }{=}{e}_i^{\prime }\right)$ and if $n_l\ne 0$ then $y_l\notin \mathit{fv}\left(e_l\right)$. We call the quasi-positive polynomial system strongly-triangular if it is triangular and satisfies $n_l\ne 0$ for all $1\le l\le n$.

The above linear equation system is triangular, but not strongly triangular since the right-hand side of the first equation is 0. Consider an integer matrix equation $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$. If A is positive and triangular, then the corresponding linear equation system is positive and triangular too. For being quasipositive and strongly-triangular, the integers below the diagonal of A must be negative, those on the diagonal must be strictly negative, and those on the right of the diagonal must be positive.

5.3. Linear Equation Systems and Elementary Modes

We next show that elementary modes [12,13,14,15] can be used to transform systems of linear equations into ${\mathbb{R}}_{+}$-equivalent systems that are quasi-positive and strongly-triangular.

We first recall the necessary definitions and folklore results on elementary modes and the double description method. We limit the presentation to equations with integer coefficients solved in ${\mathbb{R}}_{+}$, since more general definitions and results for elementary modes in $\mathbb{R}$ are not needed for this paper.

Definition 10.

The support of a function $\sigma :V\to \mathbb{R}$ is $\mathit{supp}\left(\sigma \right)=\{y\in V\mid \sigma (y)\ne 0\}$.

Definition 11

(Elementary Modes). An elementary mode of an integer matrix $A\in {\mathbb{Z}}^{n,m}$ is a vector $n\in {\mathbb{N}}^n$ such that for any sequence of pairwise distinct variables $y\in {\mathcal{V}}^n$ the function $\sigma =[y/n]$ is a solution in $so{l}^{{\mathbb{R}}_{+}}\left(Ay\stackrel{\circ }{=}0\right)$ such that:

• $\mathit{supp}\left(\sigma \right)$ is minimal, i.e., there exist no ${\sigma }^{\prime }\in \mathit{s}\mathit{o}{\mathit{l}}^S\left(\varphi \right)$ such that $\mathit{supp}\left({\sigma }^{\prime }\right)⊊\mathit{supp}\left(\sigma \right)$,
• σ is normalized, i.e., there exist variables $y,y^{\prime }$ in $y$ such that $\sigma \left(y\right)$ and $\sigma \left(y^{\prime }\right)$ are coprimes (their greatest common divisor is 1).

The elementary modes of a matrix A are the extreme directions of the polyhedral cone $so{l}^{{\mathbb{R}}_{+}}\left(A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}\right)$. This implies that any solution of the linear system can be expressed as a weighted sum of its elementary modes, where all the weights are non negative. Due to normalization, the number of elementary modes is finite for all integer matrices.

Theorem 2

(Folklore). For any integer matrix $A\in {\mathbb{Z}}^{m,n}$ one can compute a matrix of natural numbers $E\in {\mathbb{N}}^{n,o}$ in at most exponential time, such that the ${\Sigma }_{bool}$-formulas for $A\mathit{y}\stackrel{\circ }{=}\mathbf{0}$ and $\exists \mathit{x}.E\mathit{x}\stackrel{\circ }{=}\mathit{y}$ are ${\mathbb{R}}_{+}$-equivalent for all vectors $\mathit{y}\in {\mathcal{V}}^n$ and $\mathit{x}\in {\mathcal{V}}^o$ of pairwise distince variables. Furthermore, the o columns of E are the elementary modes of A.

We note that Theorem 2 can be lifted to matrices of rational numbers $\mathbb{Q}$, since any rational matrix equation $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$ can be rewritten to a integer matrix equation with the same ${\mathbb{R}}_{+}$-solution set, by multiplying with the natural numbers in the denominators of the rational numbers. The freely available cddlib tool in the rational mode [24] inputs a matrix $A\in {\mathbb{Q}}^{n,m}$, and outputs the list of (integer) elementary modes of A. From this list, we can construct the matrix E for A by aligning the elementary modes of A as the columns of E.

Note that the interface of the cddlib tool is more general, in that it applies to rational matrix inequations interpreted over the reals, rather than to rational matrix equations interpreted over the positive reals: it permits to compute the normalized extreme directions of the polyedral cone $so{l}^{\mathbb{R}}(B\mathbf{y}\ge \mathbf{0})$ for any rational matrix inequation B over the reals. If one wants to compute the elementary modes of a rational matrix A – that is the normalized extreme directions of polyhedral cones of over the positive reals $so{l}^{{\mathbb{R}}_{+}}\left(A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}\right)$ – then one can chose $B=\left(\begin{array}{c}A\hfill \\ -A\hfill \\ Id\hfill \end{array}\right)$ where $Id$ is the identity matrix with as many columns as A.

Corollary 1

(Elementary Mode Rewriting). Given a system of linear equations $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$, one can compute in at most exponential time an ${\mathbb{R}}_{+}$-equivalent formula $\mathit{emr}\left(\varphi \right)$ that has the form $\exists \mathit{x}.{\varphi }^{\prime }$ where ${\varphi }^{\prime }$ is quasi-positive and strongly-triangular system of equations.

Proof. 

Any system of linear equations $\varphi$ can be converted into some integer matrix equation $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$ where $\mathbf{y}$ is a vector that contains all variables in $\mathit{fv}\left(\varphi \right)$ exactly once. Let E be a matrix of elementary modes of A from Theorem 2. This theorem states that $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$ and thus $\varphi$ is ${\mathbb{R}}_{+}$-equivalent to $\exists \mathbf{x}.E\mathbf{x}\stackrel{\circ }{=}\mathbf{y}$ for some vector of fresh variables $\mathbf{x}$. So let $\mathit{emr}\left(\varphi \right)$ be $\exists \mathbf{x}.{\varphi }^{\prime }$ and ${\varphi }^{\prime }$ be $E\mathbf{x}\stackrel{\circ }{=}\mathbf{y}$. Since all entries of E are positive, the variables in $\mathbf{y}$ are pairwise distinct, and the variables in $\mathbf{x}$ are chosen freshly, it follows that ${\varphi }^{\prime }$ is both quasi-positive and strongly-triangular. □

We have implemented the elementary mode rewriting in Python based on the cddlib tool, and plan to make our tool publically available soon. An example input is the system of linear ${\Sigma }_{bool}$-equations ${\varphi }_0$ given in Figure 4. The corresponding integer matrix equation system is given there too. The elementary modes of the matrix of this system are the vectors $(1,0,1,1)$ and $(1,1,0,0)$. When putting these vectors in the columns of a new matrix, our tool returns the elementary mode rewriting $\mathit{emr}\left({\varphi }_0\right)$ in Figure 5.

6. ${\mathit{h}}_{\mathbb{B}}$-Exact Rewriting of Linear Equation Systems

Our next objective is to study the preservation of h-exactness by logical operators. The main difficulty of this paper is the fact that h-exactness is not preserved by conjunction. Nevertheless, as we will show next, it is preserved by disjunction and existential quantification.

To do so we first show that h-exactness is preserved when adding variables. For this, we have to assume that the $\Sigma$-abstraction h is sujective, which will be the case of all $\Sigma$-abstractions of interest.

Lemma 6

(Variable extension preserves exactness). Let $h:S\to \Delta$ be a Σ-abstraction that is surjective and $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ a formula. Then the h-exactness of ϕ implies the h-exactness of ϕ with respect to V.

Proof. 

This follows from that abstractions of solutions of $\varphi$ can be extended arbitrarily to variables that do not appear freely in $\varphi$ as stated by the following claim.

Claim 1.

For all $\sigma :V\to \Delta$: $\sigma \in h\circ so{l}^S\left(\varphi \right)$ iff ${\sigma }_{\left|\mathit{fv}\right(\varphi )}\in h\circ so{l}^S\left(\varphi \right)$.

For the one direction let $\sigma \in h\circ so{l}_V^S\left(\varphi \right)$. Then, there exists $\sigma \in so{l}_V^S\left(\varphi \right)$ such that $\sigma =h\circ \sigma$. Since $V\supseteq \mathit{fv}\left(\varphi \right)$ it follows that ${\sigma }_{\left|\mathit{fv}\right(\varphi )}\in so{l}^S\left(\varphi \right)$. Furthermore ${\sigma }_{\left|\mathit{fv}\right(\varphi )}=h\circ {\sigma }_{\left|\mathit{fv}\right(\varphi )}$ and thus ${\sigma }_{\left|\mathit{fv}\right(\varphi )}\in h\circ so{l}^S\left(\varphi \right)$.

For the other direction let ${\sigma }_{\left|\mathit{fv}\right(\varphi \left)\right)}\in h\circ so{l}^S\left(\varphi \right)$. Then, there exists $\sigma \in so{l}^S\left(\varphi \right)$ such that ${\sigma }_{\left|\mathit{fv}\right(\varphi )}=h\circ \sigma$. For any $y\in V\backslash \mathit{fv}\left(\varphi \right)$ let $s_y\in \mathit{dom}\left(S\right)$ be such that $h\left(s_y\right)=\sigma \left(y\right)$. Such values exists since h is surjective. Now define ${\sigma }^{\prime }=\sigma [y/s_y\mid y\in V\backslash \mathit{fv}\left(\varphi \right)]$. Since $V\supseteq \mathit{fv}\left(\varphi \right)$ it follows that ${\sigma }^{\prime }\in so{l}_V^S\left(\varphi \right)$. Furthermore, $\sigma =h\circ {\sigma }^{\prime }$, so $\sigma \in h\circ so{l}_V^S\left(\varphi \right)$. □

For the case of disjunction, we need a basic property of unions (joins) which fails for intersections (meets).

Lemma 7

(Abstraction ${\alpha }_h$ preserves joins). Let V be a set of variables, $R_1$ and $R_2$ be subsets of assignments of type $V\to \mathit{dom}\left(S\right)$ and $h:S\to \Delta$ be a Σ-abstraction. Then:

$$h\circ (R_1\cup R_2)=h\circ R_1\cup h\circ R_2$$

Proof. 

This lemma follows from the following equivalences:

$$\begin{array}{ccc}\hfill \tau \in h\circ (R_1\cup R_2)& \iff \hfill & \exists \sigma .\sigma \in R_1\cup R_2\wedge \tau =h\circ \sigma \hfill \\ & \iff \hfill & \exists \sigma .(\sigma \in R_1\vee \sigma \in R_2)\wedge \tau =h\circ \sigma \hfill \\ & \iff \hfill & \exists \sigma .(\sigma \in R_1\wedge \tau =h\circ \sigma )\vee (\sigma \in R_2\wedge \tau =h\circ \sigma )\hfill \\ & \iff \hfill & \tau \in h\circ R_1\vee \tau \in h\circ R_2\hfill \\ & \iff \hfill & \tau \in h\circ R_1\cup h\circ R_2\hfill \end{array}$$

□

Proposition 1.

The disjunction of h-exact formulas is h-exact.

Proof. 

Let ${\varphi }_1$ and ${\varphi }_2$ be negation free formulas that are h-exact. Let $V=\mathit{fv}\left({\varphi }_1\right)\cup \mathit{fv}\left({\varphi }_2\right)$. Lemma 6 shows that ${\varphi }_1$ and ${\varphi }_2$ are also h-exact with respect to the extended variable set V, i.e., for both $i\in \{1,2\}$:

$$\begin{array}{ccc}\hfill h\circ so{l}_V^S\left({\varphi }_i\right)& =\hfill & so{l}_V^{\Delta }\left({\varphi }_i\right)\hfill \end{array}$$

The h-exactness of the disjunction ${\varphi }_1\vee {\varphi }_2$ can now be shown as follows:

$$\begin{array}{ccc}\hfill h\circ so{l}^S({\varphi }_1\vee {\varphi }_2)& =\hfill & h\circ (so{l}_V^S\left({\varphi }_1\right)\cup so{l}_V^S\left({\varphi }_2\right))\hfill \\ & =\hfill & h\circ so{l}_V^S\left({\varphi }_1\right)\cup h\circ so{l}_V^S\left({\varphi }_2\right)\hfill & \mathrm{by}\mathrm{Lemma}7\hfill \\ & =\hfill & so{l}_V^{\Delta }\left({\varphi }_1\right)\cup so{l}_V^{\Delta }\left({\varphi }_2\right)\hfill & \mathrm{by}h-\mathrm{exactness}\mathrm{of}{\varphi }_1\mathrm{and}{\varphi }_2\mathrm{wrt}.V\hfill \\ & =\hfill & so{l}^{\Delta }({\varphi }_1\vee {\varphi }_2)\hfill \end{array}$$

□

Lemma 8

(Projection commutes with abstraction). For any Σ-abstraction $h:S\to \Delta$, subset R of assignments of type $V\to S$, and variable $x\in \mathcal{V}$: $\circ {\pi }_x\left(R\right)={\pi }_x(h\circ R)$.

Proof. 

For all $\sigma :V\to \mathit{dom}\left(S\right)$ we have $h\circ {\pi }_x\left(\sigma \right)=h\circ {\sigma }_{|V\backslash \{x\}}={(h\circ \sigma )}_{|V\backslash \{x\}}={\pi }_x(h\circ \sigma )$. □

Proposition 2

(Quantification preserves exactness). For any surjective Σ-abstraction $h:S\to \Delta$ and formula $\exists x.\varphi \in {\mathcal{F}}_{\Sigma }^{}$, if ϕ is h-exact then $\exists x.\varphi$ is h-exact.

Proof. 

Let $\varphi$ be h-exact. By definition $\varphi$ is h-exact with respect to $V=\mathit{fv}\left(\varphi \right)$. Since h is assumed to be surjective, Lemma 6 implies that $\varphi$ is h-exact with respect to $V\cup \left\{x\right\}$ (independently of whether x occurs freely in $\varphi$ or not). Hence:

$$\begin{array}{cccc}\hfill h\left(so{l}^S(\exists x.\varphi )\right)& =\hfill & \left({\pi }_x\left(so{l}^S\left(\varphi \right)\right)\right)\hfill & \mathrm{by}\mathrm{Lemma}4\hfill \\ & =\hfill & {\pi }_{x}h\left(\left(so{l}^S\left(\varphi \right)\right)\right)\hfill & \mathrm{by}\mathrm{Lemma}8\hfill \\ & =\hfill & {\pi }_x\left(so{l}^{\Delta }\left(\varphi \right)\right)\hfill & \sin \mathrm{ce}\varphi \mathrm{is}h-\mathrm{exact}\hfill \\ & =\hfill & so{l}^{\Delta }(\exists x.\varphi )\hfill & \mathrm{by}\mathrm{Lemma}4\hfill \end{array}$$

□

We next study the h-exactness for strongly-triangular systems of ${\Sigma }_{bool}$-equations, under the condition that h is an abstraction between ${\Sigma }_{bool}$-algebras with unique division (see Definition 12).

Lemma 9

(Singleton property). If S is a Σ-algebra, $e\in {\mathcal{E}}_{\Sigma }\left(V\right)$, and $\sigma :V\to S$ a variable assignment, then the set $〚e{〛}^{\sigma ,S}$ is a singleton.

Proof. 

By induction on the structure of expressions $e\in {\mathcal{E}}_{\Sigma }\left(V\right)$:

Case of constants $c\in C$. The set $〚c{〛}^{\sigma ,S}=\left\{c^S\right\}$ is a singleton.

Case of variables $x\in V$. The set $〚x{〛}^{\sigma ,S}=\left\{\sigma \left(x\right)\right\}$ is a singleton.

Case$f(e_1,\dots ,e_n)$ where $e_i\in {\mathcal{E}}_{\Sigma }\left(V\right)$ and $f\in F^{\left(n\right)}$.

$$\begin{array}{ccc}\hfill 〚f(e_1,\dots ,e_n){〛}^{\sigma ,S}& =\hfill & \{f^S(s_1,\dots ,s_n)\mid s_i\in 〚e_i{〛}^{\sigma ,S}\}\hfill \end{array}$$

This set is a singleton since $〚e_i{〛}^{\sigma ,S}$ are singletons by induction hypothesis, meaning that $f^S(〚e_1{〛}^{\sigma ,S},\dots ,〚e_n{〛}^{\sigma ,S})$ is also a singleton since S is a $\Sigma$-algebra. □

A $\Sigma$-algebra is a $\Sigma$-structure with the singleton property. Let $\mathit{ele}$ be the function that maps any singleton to the element that it contains.

Definition 12.

We say that a ${\Sigma }_{bool}$-structure S has unique division if it satisfies the first-order formula $\forall x.{\exists }^{=1}y.ny\stackrel{\circ }{=}x$ for all nonzero natural numbers $n\in \mathbb{N}$.

Clearly, the ${\Sigma }_{bool}$-structures ${\mathbb{R}}_{+}$, $\mathbb{B}$, and $\mathbb{S}$ have unique division. Note, however, that $\mathbb{S}$ is not a ${\Sigma }_{bool}$-algebra, so that the following two Propositions 3 and 4 cannot be applied to $\mathbb{S}$ instead of $\mathbb{B}$.

For any element s of the domain of a ${\Sigma }_{bool}$-structure S with unique division and any nonzero natural number $n\in \mathbb{N}$, we denote by $\frac{s}{n}$ the unique element of $\{\sigma \left(y\right)\mid \sigma \in so{l}^S\left(ny\stackrel{\circ }{=}z\right),\sigma \left(z\right)=s\}$.

Lemma 10.

Let $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$ be a formula and S a ${\Sigma }_{bool}$-algebra with unique division. For nonzero natural number n, variable $y\notin \mathit{fv}\left(\varphi \right)$, and expression $e\in {\mathcal{E}}_{\Sigma }\left(\mathit{fv}\left(\varphi \right)\right)$:

$$so{l}^S(\varphi \wedge ny\stackrel{\circ }{=}e)=\{\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]\mid \sigma \in so{l}^S\left(\varphi \right)\}$$

Proof. 

We fix some $\sigma :\mathit{fv}\left(\varphi \right)\to \mathit{dom}\left(S\right)$ arbitrarily. Since S is a ${\Sigma }_{bool}$-algebra, $〚e{〛}^{\sigma ,S}$ is a singleton and $\mathit{fv}\left(e\right)\subseteq V\left(\varphi \right)$, $\mathit{ele}(〚e{〛}^{\sigma ,S})$ is defined uniquely. Furthermore S has unique division, so that $\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}$ is a well-defined element of $\mathit{dom}\left(S\right)$. Therefore and since $y\notin \mathit{fv}\left(\varphi \right)$, $\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]$ is the unique solution of the equation $ny\stackrel{\circ }{=}e$ that extends on $\sigma$.

Firstly, we prove the inclusion “⊇”. Let $\sigma \in so{l}^S\left(\varphi \right)$, $y\notin \mathit{fv}\left(\varphi \right)$, and $\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]$ is a solution of $ny\stackrel{\circ }{=}e$, it follows that $\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]$ is a solution of $\varphi \wedge ny\stackrel{\circ }{=}e$.

Secondly, we prove the inverse inclusion “⊆”. Let $\sigma \in so{l}^S(\varphi \wedge ny\stackrel{\circ }{=}e)$. Since $\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]$ is the unique solution of the equation $ny\stackrel{\circ }{=}e$ that extends on ${\sigma }^{\prime }={\sigma }_{\left|\mathit{fv}\right(\varphi )}$ it follows that $\sigma \left(y\right)=\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}$ so that $\sigma ={\sigma }^{\prime }[y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]$ while ${\sigma }^{\prime }\in so{l}^S\left(\varphi \right)$. □

Proposition 3.

Let $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}\left(V\right)$ a formula, $n\ne 0$ a natural number, $e\in {\mathcal{E}}_{{\Sigma }_{bool}}\left(V\right)$ an expression, $y\notin V$, and $h:S\to \Delta$ a ${\Sigma }_{bool}$-abstraction between ${\Sigma }_{bool}$-algebras with unique division. Under these conditions, if ϕ is h-exact then $\varphi \wedge e\stackrel{\circ }{=}ny$ is h-exact.

Proof. 

Let $e\in {\mathcal{E}}_{{\Sigma }_{bool}}\left(V\right)$ an expression. □

Claim 2.

For any $\sigma :V\to {\mathbb{R}}_{+}$: $h\left(\mathit{ele}(〚e{〛}^{\sigma ,S})\right)=\mathit{ele}(〚e{〛}^{h\circ \sigma ,\Delta })$.

This can be seen as follows. For any $\sigma :V\to S$ Theorem 1 on homomorphism yields $h(〚e{〛}^{\sigma ,S})\subseteq 〚e{〛}^{h\circ \sigma ,\Delta }$. Since S and $\Delta$ are both $\Sigma$-algebras, the sets $〚e{〛}^{\sigma ,S}$ and $〚e{〛}^{h\circ \sigma ,\Delta }$ are both singletons by Lemma 9, so that $h\left(\mathit{ele}(〚e{〛}^{\sigma ,S})\right)=\mathit{ele}(〚e{〛}^{h\circ \sigma ,\Delta })$.

Claim 3.

For any $s\in \mathit{dom}\left(S\right)$ and $n\ne 0$ a natural number: $h\left(\frac{s}{n}\right)=\frac{h\left(s\right)}{n}$.

Since S is assumed to have unique division $s^{\prime }=\frac{s}{n}$ is well-defined as the unique element of $\mathit{dom}\left(S\right)$ such that $\underset{n}{\underbrace{s^{\prime }{+}^S\dots {+}^S{s}^{\prime }}}=s$. Hence, $h\left(\underset{n}{\underbrace{s^{\prime }{+}^S\dots {+}^S{s}^{\prime }}}\right)=h\left(s\right)$ and since h is a homomorphism, it follows that $\underset{n}{\underbrace{h\left(s^{\prime }\right){+}^{\Delta }\dots {+}^{\Delta }h\left(s^{\prime }\right)}}=h\left(s\right)$. Since $\Delta$ is assumed to have unique division, this implies that $h\left(s^{\prime }\right)=\frac{h\left(s\right)}{n}$.

The Proposition can now be shown based on these two claims. Let $\varphi$ be h-exact, $y\notin V$, and $\mathit{fv}\left(e\right)\subseteq V$. We have to show that $\varphi \wedge ny\stackrel{\circ }{=}e$ is h-exact too:

$$\begin{array}{cccc}\hfill h\circ so{l}^S(\varphi \wedge e\stackrel{\circ }{=}ny)& =\hfill & h\circ \{\sigma [y/\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}]\mid \sigma \in so{l}^S\left(\varphi \right)\}\hfill & \mathrm{by}\mathrm{Lemma}10\hfill \\ & =\hfill & \{(h\circ \sigma )[y/h\left(\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}\right)]\mid \sigma \in so{l}^S\left(\varphi \right)\}\hfill & \mathrm{elementary}\hfill \\ & =\hfill & \{\sigma [y/h\left(\frac{\mathit{ele}(〚e{〛}^{\sigma ,S})}{n}\right)]\mid \sigma \in so{l}^{\Delta }\left(\varphi \right)\}\hfill & h-\mathrm{exactness}\mathrm{of}\varphi \hfill \\ & =\hfill & \{\sigma [y/\frac{h\left(\mathit{ele}(〚e{〛}^{\sigma ,S})\right)}{n}]\mid \sigma \in so{l}^{\Delta }\left(\varphi \right)\}\hfill & \mathrm{by}\mathrm{Claim}3\hfill \\ & =\hfill & \{\sigma [y/\frac{\mathit{ele}(〚e{〛}^{h\circ \sigma ,\Delta })}{n}]\mid \sigma \in so{l}^{\Delta }\left(\varphi \right)\}\hfill & \mathrm{by}\mathrm{Claim}2\hfill \\ & =\hfill & so{l}^{\Delta }(\varphi \wedge e\stackrel{\circ }{=}ny)\hfill & \mathrm{by}\mathrm{Lemma}10\hfill \end{array}$$

Proposition 4.

Let $h:S\to \Delta$ be a ${\Sigma }_{bool}$-abstraction between algebras with unique division. Then any strongly-triangular system of ${\Sigma }_{bool}$-equations is h-exact.

Proof. 

Any strongly-triangular system of equations has the form ${\bigwedge }_{i=1}^n{e}_i\stackrel{\circ }{=}{n}_i{y}_i$ where n and $n_i\ne 0$ are naturals and $y_i$ is i-fresh for all $1\le i\le n$. The proof is by induction on n. In the case $n=0$, the conjunction is equal to $\mathit{true}$ which is h-exact since $h\left(so{l}^S\left(true\right)\right)=$ $so{l}^{\Delta }\left(true\right)$. In the case $n>0$, we have by induction hypothesis that ${\bigwedge }_{j=1}^{i-1}{e}_j\stackrel{\circ }{=}{n}_j{y}_j$ is h-exact. Since $n_i\ne 0$ it follows from Proposition 3 that that $e_i\stackrel{\circ }{=}{n}_i{y}_i\wedge {\bigwedge }_{j=1}^{i-1}{e}_j\stackrel{\circ }{=}{n}_j{y}_j$ is h-exact. □

We notice that Proposition 4 remains true for triangular systems that are not strongly-triangular. This follows from results that we can only present in the next section (Theorem 4 and Proposition 5), since they require an additional argument.

Theorem 3

($h_{\mathbb{B}}$-Exactness). Quasi-positive strongly-triangular polynomial systems are $h_{\mathbb{B}}$-exact.

Proof. 

The ${\Sigma }_{bool}$-algebras ${\mathbb{R}}_{+}$ and $\mathbb{B}$ have unique division, so we can apply Proposition 4 for proving the theorem. □

We note that the analogous statement for $\mathbb{S}$ instead of $\mathbb{B}$ fails, even though $\mathbb{S}$ has unique division. The problem is that $\mathbb{S}$ is not a ${\Sigma }_{bool}$-algebra. As a counter-example, reconsider the strongly-triangular system of quasi-positive system equations:

$$u+v\stackrel{\circ }{=}x\wedge u+v\stackrel{\circ }{=}y$$

This system implies $x\stackrel{\circ }{=}y$ over $\mathbb{R}$ but accept the abstract solution $[u/1,v/-1,x/1,y/-1]$ mapping x and y to distinct signs, so it is not $h_{\mathbb{S}}$-exact. Nevertheless, it is $h_{\mathbb{B}}$-exact by Theorem 3.

Corollary 2

($h_{\mathbb{B}}$-exact rewriting of linear equation systems). For any linear ${\Sigma }_{bool}$-equations ϕ the elementary mode rewriting $\mathit{emr}\left(\varphi \right)\in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$ is ${\mathbb{R}}_{+}$-equivalent, $h_{\mathbb{B}}$-exact, and can be computed in at most exponential time from ϕ.

Proof. 

The elementary modes rewriting Corollary 1 shows that any linear ${\Sigma }_{bool}$-equation system $\varphi$ is ${\mathbb{R}}_{+}$-equivalent a formula $\mathit{emr}\left(\varphi \right)$ of the form $\exists \mathbf{z}.{\varphi }^{\prime }$ such that ${\varphi }^{\prime }$ is a quasi-positive strongly-triangular linear equation system. Theorem 3 shows that any quasi-positive strongly-triangular linear equation system is $h_{\mathbb{B}}$-exact, so is ${\varphi }^{\prime }$. Existential quantification preserves $h_{\mathbb{B}}$-exactness by Proposition 2, so $\mathit{emr}\left(\varphi \right)$ is $h_{\mathbb{B}}$-exact too. □

This $h_{\mathbb{B}}$-exact rewriting permits us to compute the boolean abstraction of any system of linear ${\Sigma }_{bool}$-equations by computing the $\mathbb{B}$-solutions of the ${\mathbb{R}}_{+}$-equivalent $h_{\mathbb{B}}$-exact formula. The latter can be done by finite domain constraint programming.

Our objective to find an algorithm for computing the sign abstraction of a system of linear ${\Sigma }_{bool}$-equations remains open. We finally approach it in Section 9. While the idea is to use the $h_{\mathbb{B}}$-exact rewriting algorithm, we first need to generalize it from linear systems to mixed systems. This is done in Section 8. The generalization relies on the notion of $h_{\mathbb{B}}$-invariance, which we discuss next in Section 7.

7. Invariance

A problem that we need to overcome is that conjunctions of two h-exact formulas may not be h-exact. The situation changes when assuming the following notion of h-invariance for at least one of the two formulas.

Definition 13

(Invariance). Let $h:S\to \Delta$ be a Σ-abstraction and $V\subseteq \mathcal{V}$ a subset of variables. We call a subset R of variable assignments of type $V\to \mathit{dom}\left(S\right)$ h-invariant iff:

$$\forall \sigma ,{\sigma }^{\prime }:V\to \mathit{dom}\left(S\right).(\sigma \in R\wedge h\circ \sigma =h\circ {\sigma }^{\prime }\Rightarrow {\sigma }^{\prime }\in R).$$

We call a Σ-formula ϕ h-invariant if its solution set $so{l}^S\left(\varphi \right)$ is.

The relevance of the notion of invariance for exactness of conjunctions—that we will formalize in Proposition 5—is due to the the following lemma:

Lemma 11.

If either $R_1$ or $R_2$ are h-invariant then: $h\circ (R_1\cap R_2)=h\circ R_1\cap h\circ R_2$.

Proof. 

The one inclusion is straightforward without invariance:

$$\begin{array}{ccc}\hfill h\circ (R_1\cap R_2)& =\hfill & \{h\circ \sigma \mid \sigma \in R_1,\sigma \in R_2\}\hfill \\ & \subseteq \hfill & \{h\circ \sigma \mid \sigma \in R_1\}\cap \{h\circ \sigma \mid \sigma \in R_2\}\hfill \\ & =\hfill & h\circ R_1\cap h\circ R_2\hfill \end{array}$$

For the other inclusion, we can assume without loss of generality that $R_1$ is h-invariant. So let $\tau \in h\circ R_1\cap h\circ R_2$. Then, there exist ${\sigma }_1\in R_1$ and ${\sigma }_2\in R_2$ such that $\tau =h\circ {\sigma }_1=h\circ {\sigma }_2$. By h-invariance of $R_1$ it follows that ${\sigma }_1\in R_2$. So ${\sigma }_1\in R_1\cap R_2$, and hence, $\tau \in h\circ (R_1\cap R_2)$. □

We can now present the algebraic characterization of h-invariance based on the concretization function ${\gamma }_h$ of the Galois connection of h. Recall that $R\subseteq h\circ -(h\circ R)$ for all subsets of concrete variable assignments R. The inverse inclusion characterizes the h-invariance of R.

Lemma 12

(Algebraic characterization). Let $h:S\to \Delta$ be a Σ-abstraction. A subset R of concrete variable assignment $V\to \mathit{dom}\left(S\right)$ is h-invariant for h iff h $\circ -(h\circ R)\subseteq R$.

Proof. 

“⇒”. Let R be h-invariant and $\sigma \in h\circ -(h\circ R)$. Then, there exists ${\sigma }^{\prime }\in R$ such that $h\circ \sigma =h\circ {\sigma }^{\prime }$. The h-invariance of R thus implies that $\sigma \in R$.

“⇐”. Suppose that $h\circ -(h\circ R)\subseteq R$. Let $\sigma ,{\sigma }^{\prime }:V\to \mathit{dom}\left(S\right)$ such that $h\circ \sigma =h\circ {\sigma }^{\prime }$ and $\sigma \in R$. We have to show that ${\sigma }^{\prime }\in R$. From $h\circ \sigma =h\circ {\sigma }^{\prime }$ and $\sigma \in R$ it follows that ${\sigma }^{\prime }\in h\circ -(h\circ R)$ and thus ${\sigma }^{\prime }\in R$ as required. □

Lemma 13

(Variable extension preserves invariance). Let h be a surjective abstraction and R a subset of functions of type $V^{\prime }\to \mathit{dom}\left(S\right)$ and V a subset of variables disjoint from $V^{\prime }$. If R is h-invariant then ${\mathit{ext}}_V^S\left(R\right)$ is h-invariant too.

Proof. 

This follows straightforwardly from the characterization of h-invariance in Lemma 12 and the following two claims:

Claim 4.

If h is surjective then $h\circ {\mathit{ext}}_V^S\left(R\right)={\mathit{ext}}_V^{\Delta }(h\circ R)$.

This follows from $h\circ {\mathit{ext}}_V^S\left(R\right)=\{h\circ \sigma \mid \sigma \in {\mathit{ext}}_V^S\left(R\right)\}={\mathit{ext}}_V^{\Delta }\left(\{h\circ {\sigma }^{\prime }\mid {\sigma }^{\prime }\in R\}\right)$ where we use the surjectivity of h in the last step.

Claim 5.

$h\circ -{\mathit{ext}}_V^{\Delta }\left(R^{\prime }\right)={\mathit{ext}}_V^S(h\circ -R^{\prime })$ for any subset $R^{\prime }$ of functions of type $V^{\prime }\to \mathit{dom}(\Delta )$.

$$\begin{array}{ccc}\hfill h\circ -{\mathit{ext}}_V^{\Delta }\left(R^{\prime }\right)& =\hfill & \{\sigma :V\cup V^{\prime }\to \mathit{dom}\left(S\right)\mid h\circ \sigma \in {\mathit{ext}}_V^{\Delta }\left(R^{\prime }\right)\}\hfill \\ & =\hfill & \{\sigma :V\cup V^{\prime }\to \mathit{dom}\left(S\right)\mid h\circ {\sigma }_{|V^{\prime }}\in R^{\prime }\}\hfill \\ & =\hfill & {\mathit{ext}}_V^S(\{{\sigma }^{\prime }:V^{\prime }\to \mathit{dom}\left(S\right)\mid h\circ {\sigma }^{\prime }\in R^{\prime }\}\hfill \\ & =\hfill & {\mathit{ext}}_V^S(h\circ -R^{\prime })\hfill \end{array}$$

□

Lemma 14.

Let $h:S\to \Delta$ be a surjective Σ-abstraction, ϕ be a Σ-formula, and $V\supseteq \mathit{fv}\left(\varphi \right)$. Then, the h-invariance of ϕ implies the h-invariance of $so{l}_V^S\left(\varphi \right)$.

Proof. 

This follows from the cylindrification Lemma 3 and that extension preserves h-invariance as shown in Lemma 13. □

Proposition 5

(Exactness is preserved by conjunction when assuming invariance). Let h be a surjective Σ-abstraction. If ${\varphi }_1$ and ${\varphi }_2$ are h-exact Σ-formulas and ${\varphi }_1$ or ${\varphi }_2$ are h-invariant then the conjunction ${\varphi }_1\wedge {\varphi }_2$ is h-exact.

Proof. 

Let ${\varphi }_1$ and ${\varphi }_2$ be h-exact $\Sigma$-formulas. We assume without loss of generality that ${\varphi }_1$ is h-invariant. Let $V=\mathit{fv}({\varphi }_1\wedge {\varphi }_2)$. Since $\mathit{fv}\left({\varphi }_2\right)\subseteq V$ the set $so{l}_V^S\left({\varphi }_2\right)$ is h-invariant too by Lemma 14. We can now show that ${\varphi }_1\wedge {\varphi }_2$ is h-exact as follows:

$$\begin{array}{ccc}\hfill h\circ so{l}^S({\varphi }_1\wedge {\varphi }_2)& =\hfill & h\circ (so{l}_V^S\left({\varphi }_1\right)\cap so{l}_V^S\left({\varphi }_2\right))\hfill \\ & =\hfill & h\circ so{l}_V^S\left({\varphi }_1\right)\cap h\circ so{l}_V^S\left({\varphi }_2\right)\hfill & \mathrm{by}\mathrm{Lemma}11\hfill \\ & =\hfill & so{l}_V^{\Delta }\left({\varphi }_1\right)\cap so{l}_V^{\Delta }\left({\varphi }_2\right)\hfill & \mathrm{by}h-\mathrm{exactness}\mathrm{of}{\varphi }_1\mathrm{and}{\varphi }_2\mathrm{wrt}V\hfill \\ & =\hfill & so{l}^{\Delta }({\varphi }_1\wedge {\varphi }_2)\hfill \end{array}$$

□

Our next objective is to show that h-invariant formulas are closed under conjunction, disjunction, and existential quantification. The two former closure properties rely on the following two algebraic properties of abstraction decomposition.

Lemma 15

(Concretization ${\gamma }_h$ preserves join and meet). For any Σ-abstraction $h:S\to \Delta$, any subsets of assignments of type $V\to \mathit{dom}\left(S\right)$ $R_1$ and $R_2$ and V a subset of variables:

• $h\circ -(R_1\cap R_2)=h\circ -R_1\cap h\circ -R_2$.
• $h\circ -(R_1\cup R_2)=h\circ -R_1\cup h\circ -R_2$.

For general Galois connections, concretization is well-known to preserve joins but may not preserve meets. Still, meets are preserved for any Galois connections where the the concrete and abstract domains C and A are powersets as in our setting, so that joins are unions and meets intersections.

Proof. 

The case of unions follows straightforwardly from the definitions:

$$\begin{array}{ccc}\hfill h\circ -(R_1\cup R_2)& =\hfill & \{\sigma \mid h\circ \sigma \in R_1\cup R_2\}\hfill \\ & =\hfill & \{\sigma \mid h\circ \sigma \in R_1\vee h\circ \sigma \in R_2\}\hfill \\ & =\hfill & \{\sigma \mid h\circ \sigma \in R_1\}\cup \{\sigma \mid h\circ \sigma \in R_2\}\hfill \\ & =\hfill & h\circ -R_1\cup h\circ -R_2\hfill \end{array}$$

The case of intersection is symmetric:

$$\begin{array}{ccc}\hfill h\circ -(R_1\cap R_2)& =\hfill & \{\sigma \mid h\circ \sigma \in R_1\cap R_2\}\hfill \\ & =\hfill & \{\sigma \mid h\circ \sigma \in R_1\wedge h\circ \sigma \in R_2\}\hfill \\ & =\hfill & \{\sigma \mid h\circ \sigma \in R_1\}\cap \{\sigma \mid h\circ \sigma \in R_2\}\hfill \\ & =\hfill & h\circ -R_1\cap h\circ -R_2\hfill \end{array}$$

□

Lemma 16

(Intersection and union preserve invariance). Let $h:S\to \Delta$ be a Σ-abstraction. Then, the intersection and union of any two h-invariant subsets $R_1$ and $R_2$ of variables assignments of type $V\to \mathit{dom}\left(S\right)$ is h-invariant.

Proof. 

This follows from the algebraic characterization Lemma 12 for invariance, in combination with the algebraic properties of composition and decomposition given in Lemmas 7, 11, and 15. □

Lemma 17

(Concretization ${\gamma }_h$ commutes with projection). $h\circ -{\pi }_x\left(R\right)={\pi }_x(h\circ -R)$.

Proof. 

For all $\sigma :V\to \mathit{dom}(\Delta )$ we have $h\circ -{\pi }_x\left(\sigma \right)=h\circ -{\sigma }_{|V\backslash \{x\}}={(h\circ -\sigma )}_{|V\backslash \{x\}}={\pi }_x(h\circ -\sigma )$. □

Proposition 6

(Invariance is preserved by conjunction, disjunction, and quantification). If h is a surjective abstraction, then the class of h-invariant FO-formulas is closed under conjunction, disjunction, and existential quantification.

Proof. 

Let $h:S\to \Delta$ be a $\Sigma$-abstraction.

Case of conjunction: Let ${\varphi }_1$ and ${\varphi }_2$ be h-invariant and $V=\mathit{fv}({\varphi }_1\wedge {\varphi }_2)$. By Lemma 14 the sets $so{l}_V^S\left({\varphi }_1\right)$ and $so{l}_V^S\left({\varphi }_2\right)$ are both h-invariant, and so by Lemma 16 is their intersection. Hence:

$$\begin{array}{ccc}& & h\circ -(h\circ so{l}^S({\varphi }_1\wedge {\varphi }_2))\hfill \\ & =\hfill & h\circ -(h\circ (so{l}_V^S\left({\varphi }_1\right)\cap so{l}_V^S\left({\varphi }_2\right)))\hfill \\ & \subseteq \hfill & so{l}_V^S\left({\varphi }_1\right)\cap so{l}_V^S\left({\varphi }_2\right)\hfill & \mathrm{by}h-\mathrm{invariance}\mathrm{and}\mathrm{Lemma}12\hfill \\ & =\hfill & so{l}^S({\varphi }_1\wedge {\varphi }_2)\hfill \end{array}$$

By Lemma 12 in the other direction, this implies that ${\varphi }_1\wedge {\varphi }_2$ is h-invariant.

Case of disjunction: Analogous to the case of conjunction.

Case of existential quantification:

$$\begin{array}{ccc}& & h\circ -(h\circ so{l}^S(\exists x.{\varphi }_1))\hfill \\ & =\hfill & h\circ -(h\circ {\pi }_x\left(so{l}^S\left({\varphi }_1\right)\right))\hfill & \mathrm{by}\mathrm{Lemma}4\hfill \\ & =\hfill & h\circ -\left({\pi }_x(h\circ so{l}^S\left({\varphi }_1\right))\right)\hfill & \mathrm{by}\mathrm{Lemma}8\hfill \\ & =\hfill & {\pi }_x(h\circ -(h\circ so{l}^S\left({\varphi }_1\right)))\hfill & \mathrm{by}\mathrm{Lemma}17\hfill \\ & \subseteq \hfill & {\pi }_x\left(so{l}^S\left({\varphi }_1\right)\right)\hfill & \mathrm{by}\mathrm{h}-\mathrm{invariance}\mathrm{of}{\varphi }_1\mathrm{and}\mathrm{Lemma}12\hfill \\ & =\hfill & so{l}^S(\exists x.{\varphi }_1)\hfill & \mathrm{by}\mathrm{Lemma}4\hfill \end{array}$$

By Lemma 12, this implies that $\exists x.{\varphi }_1$ is h-invariant. □

We do not know whether negation preserves h-invariance in general, but for finite $\Delta$ it can be shown that if $\varphi$ is h-exact and h-invariant, then $\neg \varphi$ is h-exact and h-invariant too.

Proposition 7.

Let h be a surjective Σ-abstraction. Then, the class of h-exact and h-invariant Σ-formulas is closed under conjunction, disjunction, and existential quantification.

Proof. 

Closure under conjunction follows from Propositions 5 and 6, closure under disjunction from Propositions 1 and 6, and closure under existential quantification by Propositions 2 and 6. □

Theorem 4

($h_{\mathbb{B}}$-invariance and $h_{\mathbb{B}}$-exactness of polynomial equations). Any positive polynomial equation $p\stackrel{\circ }{=}0$ such that p has no constant term is $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant.

Proof. 

Consider a positive polynomial equation $p\stackrel{\circ }{=}0$ such that p has no constant term and only positive coefficients. Thus, p has the form ${\sum }_{j=1}^l{n}_j{\prod }_{k=1}^{i_j}{x}_{j,k}^{m_{j,k}}\stackrel{\circ }{=}0$ where $l\ge 0$, and $n_j,i_j,m_{j,k}>0$.

Claim 6.

For both algebras $S\in \{\mathbb{B},{\mathbb{R}}_{+}\}$: $so{l}^S\left(p\stackrel{\circ }{=}0\right)=so{l}^S\left({\bigwedge }_{j=1}^l{\bigvee }_{k=1}^{i_j}{x}_{j,k}\stackrel{\circ }{=}0\right).$

The polynomial has a value of zero if and only if all its monomials do, that is: ${\prod }_{k=1}^{i_j}{x}_{j,k}^{m_{jk}}=0$ for all $1\le j\le l$. Since constant terms are ruled out, we have $i_j\ne 0$. Furthermore, we assumed for all polynomials that $m_{j,k}\ne 0$. So for all $1\le j\le l$ there must exist $1\le k\le i_j$ such that $x_{j,k}=0$.

Claim 7.

The equation $x\stackrel{\circ }{=}0$ is $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant.

This proof of this claim is straightforward from the definitions.

With these two claims, we are now in the position to prove the Theorem 4. Since the class of $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant formulas is closed under conjunction and disjunction by Proposition 7, it follows from by Claim 7 that ${\wedge }_{j=1}^l{\vee }_{k=1}^{i_j}{x}_{j,k}\stackrel{\circ }{=}0$ is both $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant. Since this formula is equivalent over ${\mathbb{R}}_{+}$ to the polynomial equation by Claim 6, the $h_{\mathbb{B}}$-invariance carries over to $p\stackrel{\circ }{=}0$. The $h_{\mathbb{B}}$-exactness also carries over based on the equivalence for both structures ${\mathbb{R}}_{+}$ and $\mathbb{B}$:

$$\begin{array}{cccc}\hfill h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(p\stackrel{\circ }{=}0\right)& =\hfill & h_{\mathbb{B}}\circ so{l}_V^{{\mathbb{R}}_{+}}\left({\wedge }_{j=1}^l{\vee }_{k=1}^{i_j}{x}_{j,k}\stackrel{\circ }{=}0\right)\hfill & \mathrm{by}\mathrm{Claim}6\mathrm{for}{\mathbb{R}}_{+}\hfill \\ & =\hfill & so{l}^{\mathbb{B}}\left({\wedge }_{j=1}^l{\vee }_{k=1}^{i_j}{x}_{j,k}\stackrel{\circ }{=}0\right)\hfill & \mathrm{by}{h}_{\mathbb{B}}\mathrm{exactness}\hfill \\ & =\hfill & so{l}^{\mathbb{B}}\left(p\stackrel{\circ }{=}0\right)\hfill & \mathrm{by}\mathrm{Claim}6\mathrm{for}\mathbb{B}.\hfill \end{array}$$

□

8. ${\mathit{h}}_{\mathbb{B}}$-Exact Rewriting of ${\mathit{h}}_{\mathbb{B}}$-Mixed Systems

In this section, we lift our main result to $h_{\mathbb{B}}$-mixed system, presenting a rewrite algorithm that makes any $h_{\mathbb{B}}$-mixed system $h_{\mathbb{B}}$-exact.

Definition 14.

A $h_{\mathbb{B}}$-mixed system is a formula in ${\mathcal{F}}_{{\Sigma }_{bool}}^{}$ of the form $\exists \mathbf{z}.\varphi \wedge {\varphi }^{\prime }$ where ϕ is a system of linear ${\Sigma }_{bool}$-equations and ${\varphi }^{\prime }$ a $h_{\mathbb{B}}$-invariant and $h_{\mathbb{B}}$-exact first-order formula.

Note that linear equation systems $A\mathbf{y}\stackrel{\circ }{=}\mathbf{0}$, with A an integer matrix and $\mathbf{y}$ a sequence of pairwise distinct variables, need not to be $h_{\mathbb{B}}$-exact, if A is not positive. However, as shown by the elementary mode rewriting Corollary 1 any linear equation systems is ${\mathbb{R}}_{+}$-equivalent to some quasipositive strongly-triangular linear system, that is $h_{\mathbb{B}}$-exact by Theorem 3.

Our next objective is to rewrite formulas to reduce the overapproximation coming with the abstract interpretation over the Booleans by John’s theorem. The idea is to make a linear equation system $h_{\mathbb{B}}$-exact that are used as subformulas as for instance of $h_{\mathbb{B}}$-mixed systems.

We recall from Corollary 1 that the elementary mode rewriting $\mathit{emr}\left(\varphi \right)$ of a linear equation system is an $h_{\mathbb{B}}$-exact formula that is ${\mathbb{R}}_{+}$-equivalent to $\varphi$. We now introduce the boolean rewriting by lifting the elementary mode rewriting to a richer class of formulas. Given a vector $\mathbf{z}\in {\mathcal{V}}^{\ast }$, a linear equation system $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$, and a formula ${\varphi }^{\prime }\in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$, the boolean rewriting is defined by:

$$\mathit{br}(\exists \mathbf{z}.(\varphi \wedge {\varphi }^{\prime })){=}_{\mathrm{def}}\exists \mathbf{z}.(\mathit{emr}\left(\varphi \right)\wedge {\varphi }^{\prime })$$

The boolean rewriting may indeed reduce the overapproximation coming with abstract interpretation of formulas over the booleans, as show by the following proposition.

Proposition 8.

$h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\psi \right)\subseteq so{l}^{\mathbb{B}}\left(\mathit{br}\left(\psi \right)\right)\subseteq so{l}^{\mathbb{B}}\left(\psi \right)$.

Proof. 

Let $\varphi$ be a linear equation system, $\mathbf{z}\in {\mathcal{V}}^{\ast }$, ${\varphi }^{\prime }\in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$ and $\psi {=}_{\mathrm{def}}\exists \mathbf{z}.\varphi \wedge {\varphi }^{\prime }$. Since $\varphi$ is ${\mathbb{R}}_{+}$-equivalent to $\mathit{emr}\left(\varphi \right)$, it follows that $\mathit{br}\left(\psi \right)$ is ${\mathbb{R}}_{+}$-equivalent to $\psi$. Hence, $so{l}^{{\mathbb{R}}_{+}}\left(\psi \right)=so{l}^{{\mathbb{R}}_{+}}\left(\mathit{br}\left(\psi \right)\right)$ so that:

$$h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\psi \right)=h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\mathit{br}\left(\psi \right)\right)$$

By John’s theorem, we have:

$$h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\mathit{br}\left(\psi \right)\right)\subseteq so{l}^{\mathbb{B}}\left(\mathit{br}\left(\psi \right)\right)$$

Furthermore, by $h_{\mathbb{B}}$-exactness, ${\mathbb{R}}_{+}$-equivalence, and again John’s theorem, we have:

$$so{l}^{\mathbb{B}}\left(\mathit{emr}\left(\varphi \right)\right)=h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\mathit{emr}\left(\varphi \right)\right)=h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\varphi \right)\subseteq so{l}^{\mathbb{B}}\left(\varphi \right)$$

Therefore, it follows that:

$$so{l}^{\mathbb{B}}\left(\mathit{br}\left(\psi \right)\right)\subseteq so{l}^{\mathbb{B}}\left(\psi \right)$$

In combination this yields the inclusions of the proposition. □

Theorem 5

(Main). For any $h_{\mathbb{B}}$-mixed system $\psi \in {\mathcal{F}}_{\Sigma }^{}$ the boolean rewriting $\mathit{br}\left(\psi \right)$ is $h_{\mathbb{B}}$-exact, ${\mathbb{R}}_{+}$-equivalent to ψ, and can be computed in at most exponential time.

Proof. 

Let $\psi$ be a $h_{\mathbb{B}}$-mixed system $\exists \mathbf{x}.(\varphi \wedge {\varphi }^{\prime })$. where $\varphi$ is a linear equation system and ${\varphi }^{\prime }$ a first-order formula that is $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant. Based on the elementary modes rewriting Corollary 1, the linear equation system $\varphi$ can be transformed in at most exponential time to the form $\mathit{emr}\left(\psi \right)=\exists \mathbf{z}.{\varphi }^{″}$ where ${\varphi }^{″}$ is a quasipositive strongly-triangular system of linear equations. Such polynomial equation systems are $h_{\mathbb{B}}$-exact by Theorem 3, and so is ${\varphi }^{″}$. The Invariance Proposition 5 shows that the conjunction ${\varphi }^{″}\wedge {\varphi }^{\prime }$ is $h_{\mathbb{B}}$-exact too, since ${\varphi }^{\prime }$ was assumed to be $h_{\mathbb{B}}$-exact and $h_{\mathbb{B}}$-invariant. The $h_{\mathbb{B}}$-exactness is preserved by existential quantification by Proposition 2, so the formula $\mathit{br}\left(\psi \right)=\exists \mathbf{x}.\mathit{emr}\left(\varphi \right)\wedge {\varphi }^{\prime }$ is $h_{\mathbb{B}}$-exact too. □

Corollary 3.

The $h_{\mathbb{B}}$-abstraction of the ${\mathbb{R}}_{+}$-solution set of a $h_{\mathbb{B}}$-mixed system ϕ, that is $h_{\mathbb{B}}\circ so{l}^{{\mathbb{R}}_{+}}\left(\varphi \right)$, can be computed in at most exponential time in the size of the system ϕ.

Proof. 

Given a $h_{\mathbb{B}}$-mixed system $\varphi$, we can apply Theorem 5 to compute in at most exponential time a ${\mathbb{R}}_{+}$-equivalent formula ${\varphi }^{″}$ that is $h_{\mathbb{B}}$-exact. It is then sufficient to compute $so{l}^{\mathbb{B}}\left({\varphi }^{″}\right)$ in exponential time in the size of $\varphi$. This can be done in the naive manner, that is by evaluating the formula ${\varphi }^{″}$—which may be of exponential size—over all possible boolean variable assignments, of which there may be exponentially many. For each assignment, the evaluation can be done in PSpace, and thus in exponential time. The overall time required is thus a product of two exponentials, which remains exponential. □

The algorithm from the proof Corollary 3 can be improved so that it becomes sufficiently efficient for practical use. For this the two steps with exponential worst case complexity must be made polynomial for the particular instances. Firstly, note that the computation of the elementary modes (Corollary 1) is known to be computationally feasible. Various algorithms for this purpose were implemented [16,24,25,26] and applied successfully to problems in systems biology [14]. The second exponential step concerns the enumeration of all boolean variable assignments. This enumeration may be avoided by using constraint programming techniques for computing the solution set $so{l}^{\mathbb{B}}\left({\varphi }^{″}\right)$. For those $h_{\mathbb{B}}$-mixed systems for which both steps can be done in polynomial time, we can compute the boolean abstraction of the ${\mathbb{R}}_{+}$-solution set in polynomial time too. The practical feasibility of this approach was demonstrated recently at an application to knockout prediction in systems biology [6], where previously only over-approximations could be computed.

9. Computing Sign Abstractions

We next show how to compute the sign abstraction $h\mathbb{S}\circ so{l}^{\mathbb{R}}\left(\varphi \right)$ for systems $\varphi$ of linear ${\Sigma }_{bool}$-equations. To apply $h_{\mathbb{B}}$-exact rewriting, we decompose the sign abstraction into the boolean abstraction and functions definable in first-order logic.

9.1. Decomposition

We can decompose any real number $r\in \mathbb{R}$ into a pair of two positive numbers $dec\left(r\right)\in {\mathbb{R}}_{+}^2$—negative and the positive part—as follows:

$$dec\left(r\right){=}_{\mathrm{def}}\left\{\begin{array}{cc}(0,r)\hfill & \mathrm{if}r\ge 0\hfill \\ (-r,0)\hfill & \mathrm{if}r\le 0\hfill \end{array}\right.$$

The image of this surjective function is $\left\{0\right\}\times {\mathbb{R}}_{+})\cup ({\mathbb{R}}_{+}\times \left\{0\right\}$, so it has an inverse $\mathrm{dec}{}^{-1}:(\left\{0\right\}\times {\mathbb{R}}_{+})\cup ({\mathbb{R}}_{+}\times \left\{0\right\})\to \mathbb{R}$, which satisfies for all pairs $(r_1,r_2)$ in the domain:

$$\mathrm{dec}{}^{-1}(r_1,r_2)=r_2{-}^{\mathbb{R}}{r}_1$$

Furthermore, recall that $h_{\mathbb{B}}^2:{\mathbb{R}}_{+}^2\to {\mathbb{B}}^2$ satisfies $h_{\mathbb{B}}^2(r_1,r_2)=(h_{\mathbb{B}}\left(r_1\right),h_{\mathbb{B}}\left(r_2\right))$.

Lemma 18

(Decomposition). $h\mathbb{S}=dec{}^{-1}\circ h_{\mathbb{B}}^2\circ dec$

Proof. 

If r is negative then $\mathrm{dec}{}^{-1}\left(h_{\mathbb{B}}^2\left(\mathrm{dec}\left(r\right)\right)\right)=\mathrm{dec}{}^{-1}\left(h_{\mathbb{B}}^2\left((-r,0)\right)\right)=\mathrm{dec}{}^{-1}\left((h_{\mathbb{B}}(-r),0)\right)$$=-h_{\mathbb{B}}(-r)=h_{\mathbb{S}}\left(r\right)$. Otherwise if r is positive then $\mathrm{dec}{}^{-1}\left(h_{\mathbb{B}}^2\left(\mathrm{dec}\left(r\right)\right)\right)=\mathrm{dec}{}^{-1}\left(h_{\mathbb{B}}^2\left((0,r)\right)\right)$ = $\mathrm{dec}{}^{-1}((0,h_{\mathbb{B}}\left(r\right))$ = $h_{\mathbb{B}}\left(r\right)=h_{\mathbb{S}}\left(r\right)$. □

9.2. Positivity

We show in a first step that first-order formulas over the reals can be rewritten, such that interpretation over the positive reals is enough.

We call a formula $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$ flat if all equations contained in $\varphi$ have the form $x\stackrel{\circ }{=}{x}_1+x_2$, $x\stackrel{\circ }{=}{x}_1\ast x_2$, $x\stackrel{\circ }{=}0$, or $x\stackrel{\circ }{=}1$ for some variables $x,x_1,x_2$. Note that any formula $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$ can be converted to an equivalent flat formula in linear time by introducing fresh existentially quantified variables, so that we can assume flatness without loss of generality.

We fix two generators of fresh variable ${\nu }_{\ominus }$, ${\nu }_{\oplus }:\mathcal{V}\to \mathcal{V}$. For any $x\in \mathcal{V}$, the intention is that ${\nu }_{\oplus }\left(x\right)$ stands for the positive part of x and ${\nu }_{\ominus }\left(x\right)$ for its negative part. We will preserve the invariants $x={\nu }_{\oplus }\left(x\right)-{\nu }_{\ominus }\left(x\right)$ and ${\nu }_{\oplus }\left(x\right)\ast {\nu }_{\ominus }\left(x\right)=0$. Furthermore, we define $\nu :\mathcal{V}\to {\mathcal{V}}^2$ such that for all $x\in \mathcal{V}$:

$$\nu \left(x\right){=}_{\mathrm{def}}({\nu }_{\ominus }\left(x\right),{\nu }_{\oplus }\left(x\right))$$

For any flat formula $\varphi \in {\mathcal{F}}_{\Sigma }^{}\left(V\right)$ we define a formula ${\mathrm{dec}}_{\nu }\left(\varphi \right)\in {\mathcal{F}}_{\Sigma }^{}({\nu }_{\ominus }\left(V\right)\cup {\nu }_{\oplus }\left(V\right))$ with the variables ${\nu }_{\ominus }\left(x\right)$ and ${\nu }_{\oplus }\left(x\right)$ instead of x for all $x\in V$. Otherwise the formula ${\widetilde{\mathrm{dec}}}_{\nu }\left(\varphi \right)$ has the same meaning as over the reals than $\varphi$.

$${\widetilde{\mathrm{dec}}}_{\nu }\left(\varphi \right)={\mathrm{dec}}_{\nu }\left(\varphi \right)\wedge \underset{x\in V}{\bigwedge }{\nu }_{\oplus }\left(x\right)\ast {\nu }_{\ominus }\left(x\right)\stackrel{\circ }{=}0$$

where

$$\begin{array}{ll}{\mathrm{dec}}_{\nu }(x\stackrel{\circ }{=}{x}_1+x_2)=\hfill & {\mathrm{dec}}_{\nu }(x\stackrel{\circ }{=}{x}_1\ast x_2)=\hfill \\ {\nu }_{\oplus }\left(x\right)+{\nu }_{\ominus }\left(x_1\right)+{\nu }_{\ominus }\left(x_2\right)\stackrel{\circ }{=}\hfill & {\nu }_{\oplus }\left(x\right)+{\nu }_{\oplus }\left(x_1\right)\ast {\nu }_{\ominus }\left(x_2\right)+{\nu }_{\ominus }\left(x_1\right)\ast {\nu }_{\oplus }\left(x_2\right)\stackrel{\circ }{=}\hfill \\ {\nu }_{\ominus }\left(x\right)+{\nu }_{\oplus }\left(x_1\right)+{\nu }_{\oplus }\left(x_2\right)\hfill & {\nu }_{\ominus }\left(x\right)+{\nu }_{\oplus }\left(x_1\right)\ast {\nu }_{\oplus }\left(x_2\right)+{\nu }_{\ominus }\left(x_1\right)\ast {\nu }_{\ominus }\left(x_2\right)\hfill \\ {\mathrm{dec}}_{\nu }\left(x\stackrel{\circ }{=}0\right)={\nu }_{\oplus }\left(x\right)\stackrel{\circ }{=}{\nu }_{\ominus }\left(x\right)\hfill & {\mathrm{dec}}_{\nu }\left(x\stackrel{\circ }{=}1\right)={\nu }_{\oplus }\left(x\right)\stackrel{\circ }{=}{\nu }_{\ominus }\left(x\right)+1\hfill \\ {\mathrm{dec}}_{\nu }(\exists x.\varphi )=\exists {\nu }_{\ominus }\left(x\right).\exists {\nu }_{\oplus }\left(x\right).\hfill & {\mathrm{dec}}_{\nu }(\varphi \wedge {\varphi }^{\prime })={\mathrm{dec}}_{\nu }\left(\varphi \right)\wedge {\mathrm{dec}}_{\nu }\left({\varphi }^{\prime }\right)\hfill \\ {\nu }_{\oplus }\left(x\right)\ast {\nu }_{\ominus }\left(x\right)\stackrel{\circ }{=}0\wedge {\mathrm{dec}}_{\nu }\left(\varphi \right)\hfill & {\mathrm{dec}}_{\nu }(\neg \varphi )=\neg {\mathrm{dec}}_{\nu }\left(\varphi \right)\hfill \end{array}$$

Note that the definition in the case of addition, the definition relies on that subtraction ${-}^{\mathbb{R}}$ in the structure of reals is the inverse of addition ${+}^{\mathbb{R}}$. The expressions that are to be subtracted on one side of the equation are added to the other side instead. This is also used in the case of multiplication, in combination with the distributivity law for addition ${+}^{\mathbb{R}}$ and multiplication ${\ast }^{\mathbb{R}}$. Furthermore, ${\widetilde{\mathrm{dec}}}_{\nu }\left(\varphi \right)$ belongs to ${\mathcal{F}}_{{\Sigma }_{bool}}^{}({\nu }_{\ominus }\left(V\right)\cup {\nu }_{\ominus }\left(V\right))$ and can be computed in linear time from $\varphi$.

Proposition 9

(Positivity). For any flat formula $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}\left(V\right)$:

$$\begin{array}{c}dec\circ so{l}_V^{\mathbb{R}}\left(\varphi \right)=\{{\sigma }^2\circ {\nu }_{|V}\mid \sigma \in so{l}^{{\mathbb{R}}_{+}}\left({\widetilde{dec}}_{\nu }\left(\varphi \right)\right)\}\hfill \end{array}$$

Proof. 

By induction on the structure of $\varphi$. In the first case of reals, can use that ${-}^{\mathbb{R}}$ is the inverse of ${+}^{\mathbb{R}}$ and that the distributivity laws holds for ${+}^{\mathbb{R}}$ and ${\ast }^{\mathbb{R}}$. □

Lemma 19.

For any flat linear equation system ϕ, the formula ${\widetilde{dec}}_{\nu }\left(\varphi \right)$ is a $h_{\mathbb{B}}$-mixed system.

Proof. 

If $\varphi$ is a flat linear system, then ${\mathrm{dec}}_{\nu }\left(\varphi \right)$ is a linear system, so that ${\widetilde{\mathrm{dec}}}_{\nu }\left(\varphi \right)$ is a $h_{\mathbb{B}}$-mixed system. □

9.3. Computing Sign Abstractions

We now have developed all the prerequisite for computing the sign abstraction of linear equation systems by using $h_{\mathbb{B}}$-exact boolean rewriting of $h_{\mathbb{B}}$-mixed systems.

Theorem 6.

For any linear equation system $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}\left(V\right)$, the formula $\mathit{br}\left({\widetilde{dec}}_{\nu }\left(\varphi \right)\right)$ can be computed in at most exponential time and satisfies:

$$h_{\mathbb{S}}\circ so{l}_V^{\mathbb{R}}\left(\varphi \right)=\{[y/\tau \left({\nu }_{\oplus }\left(y\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(y\right)\right)\mid y\in V]\mid \tau \in so{l}_{}^{\mathbb{B}}\left(\mathit{br}\left({\widetilde{dec}}_{\nu }\left(\varphi \right)\right)\right)\}$$

Proof. 

Let $\varphi \in {\mathcal{F}}_{{\Sigma }_{bool}}^{}\left(V\right)$ be a system of linear equations. Without loss of generality, we can assume that $\varphi$ is flat. Let: $\tilde{\varphi }{=}_{\mathrm{def}}{\widetilde{dec}}_{\nu }\left(\varphi \right)$. The formula $\tilde{\varphi }$ is a $h_{\mathbb{B}}$-mixed system by Lemma 19 with $\mathit{fv}\left(\tilde{\varphi }\right)={\nu }_{\ominus }\left(V\right)\cup {\nu }_{\oplus }\left(V\right)$ so that we can apply the Main Theorem 5 to it. It shows that boolean rewriting $\mathit{br}\left(\tilde{\varphi }\right)$ is an ${\mathbb{R}}_{+}$-equivalent formula in ${\mathcal{F}}_{\Sigma }^{}({\nu }_{\oplus }\left(V\right)\cup {\nu }_{\ominus }\left(V\right))$ that is $h_{\mathbb{B}}$-exact and can be computed in at most exponential time. We can now conclude as follows:

$$\begin{array}{ccc}{h}_{\mathbb{S}}\hfill & \circ so{l}_V^{\mathbb{R}}\left(\varphi \right)\hfill & \\ & =\mathrm{dec}{}^{-1}\circ h_{\mathbb{B}}^2\circ \mathrm{dec}\circ so{l}_V^{\mathbb{R}}\left(\varphi \right)\hfill & \mathrm{Decomposition}\mathrm{Lemma}18\hfill \\ & =\mathrm{dec}{}^{-1}\circ h_{\mathbb{B}}^2\circ \{{\sigma }^2\circ {\nu }_{|V}\mid \sigma \in so{l}_{}^{{\mathbb{R}}_{+}}\left(\tilde{\varphi }\right)\}\hfill & \mathrm{Positivity}\mathrm{Proposition}9\hfill \\ & =\mathrm{dec}{}^{-1}\circ h_{\mathbb{B}}^2\circ \{{\sigma }^2\circ {\nu }_{|V}\mid \sigma \in so{l}_{}^{{\mathbb{R}}_{+}}\left(\mathit{br}\left(\tilde{\varphi }\right)\right\}\hfill & {\mathbb{R}}_{+}-\mathrm{equivalence}\mathrm{of}\tilde{\varphi }\mathrm{and}\mathit{br}\left(\tilde{\varphi }\right)\hfill \\ & =\{\mathrm{dec}{}^{-1}\circ {\tau }^2\circ {\nu }_{|V}\mid \tau \in so{l}_{}^{\mathbb{B}}\left(\mathit{br}\left(\tilde{\varphi }\right)\right)\}\hfill & h_{\mathbb{B}}-\mathrm{exactness}\mathrm{of}\mathit{br}\left(\tilde{\varphi }\right)\hfill \\ & =\{[y/\tau \left({\nu }_{\oplus }\left(y\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(y\right)\right)\mid y\in V]\hfill & \mathrm{definition}\mathrm{of}\mathrm{dec}{}^{-1}\hfill \\ & \mid \tau \in so{l}_{}^{\mathbb{B}}\left(\mathit{br}\left(\tilde{\varphi }\right)\right)\}\hfill & \end{array}$$

The sign abstraction of a system $\varphi$ of ${\Sigma }_{bool}$-equations with free variables in $V=\mathit{fv}\left(\varphi \right)$ can thus be computed by first computing the $h_{\mathbb{B}}$-exact formula $\mathit{br}\left(\tilde{\varphi }\right)\in {\mathcal{F}}_{\Sigma }^{}({\nu }_{\oplus }\left(V\right)\cup {\nu }_{\ominus }\left(V\right))$ from Theorem 6 by applying the Positivity Proposition 9 and the Main Theorem 5, then computing $so{l}_{}^{\mathbb{B}}\left(\mathit{br}\left(\tilde{\varphi }\right)\right)$ by finite domain constraint programming, and finally inferring $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left(\varphi \right)$ thereof based on the equation of Theorem 6.

Corollary 4.

The sign abstraction $h_{\mathbb{S}}\circ so{l}_V^{\mathbb{R}}\left(\varphi \right)$ can be computed in at most single exponential time in the size of ϕ.

Proof. 

The formula $\mathit{br}\left(\tilde{\varphi }\right)$ is of exponential size but contains only twice as many variables than $\varphi$. Let $n=\left|\mathit{fv}\right(\varphi \left)\right|$. We can then compute $h_{\mathbb{S}}\circ so{l}_V^{\mathbb{R}}\left(\varphi \right)$ by testing $6^{2n}$ variable assignments for membership to $so{l}_{}^{\mathbb{R}}\left(\mathit{br}\left(\tilde{\varphi }\right)\right)$. Each such test is linear in the size of $\mathit{br}\left(\tilde{\varphi }\right)$, and thus in $O\left(2^m\right)$ where m is the size of $\varphi$. So the overall time is in $O\left(6^{2n}{2}^m\right)$ and since $n\le m$ in $O\left(6^{3m}\right)$. □

We finally show that the same algorithm as for computing the sign abstraction for linear equation systems can be lifted to a richer class of formulas to obtain another and possibly more precise overapproximation of the sign abstraction than John’s.

Proposition 10.

Let $\psi =\exists \mathbf{z}.\varphi \wedge {\varphi }^{\prime }$ in ${\mathcal{F}}_{{\Sigma }_{bool}}^{}\left(V\right)$ for some linear equation system ϕ and formula ${\varphi }^{\prime }\in {\mathcal{F}}_{{\Sigma }_{bool}}^{}$. The formula $\mathit{br}\left({\widetilde{dec}}_{\nu }\left(\psi \right)\right)$ then yields an overapproximation of the sign abstraction of ϕ:

$$h_{\mathbb{S}}\circ so{l}_V^{\mathbb{R}}\left(\psi \right)\subseteq \{[y/\tau \left({\nu }_{\oplus }\left(y\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(y\right)\right)\mid y\in V]\mid \tau \in so{l}_{}^{\mathbb{B}}\left(\mathit{br}\left({\widetilde{dec}}_{\nu }\left(\psi \right)\right)\right)\}$$

Proof. 

Along the lines of the proof of Theorem except that $\mathit{br}\left({\widetilde{dec}}_{\nu }\left(\psi \right)\right)$ is not $h_{\mathbb{B}}$-exact. Therefore, the equality where the $h_{\mathbb{B}}$-exactness was used must be weakened to an inclusion. □

10. Application to Program Analysis

We illustrate our results by applying the sign abstraction for program analysis based on abstract interpretation. We consider the Python implementation in Figure 6 of the function $\mathtt{I}:{\mathbb{R}}^2\to \mathbb{R}$. A call $\mathtt{I}(\mathit{a},\mathit{s})$ supposedly computes the approximation of the integral ${\int }_0^{\mathit{a}}\mathtt{f}\left(x\right)dx$ with step width $\mathit{s}$ for some total function $\mathtt{f}:\mathbb{R}\to \mathbb{R}$. Abstract interpretation allows us to find out the conditions that must hold on the input parameters for $\mathtt{I}\left(\right(\mathit{a}:float,\mathit{s}:float)$ to work properly, and in particular to avoid exception throwing.

We can first interpret numeric programs abstractly as a formula of first-order logic with signature ${\Sigma }_{arith}$. We illustrate this in an ad hoc manner on the integral example $\mathtt{I}$:

$${\varphi }_{\mathtt{I}}{=}_{\mathrm{def}}\begin{array}{c}\exists {\mathit{ret}}_{\mathtt{f}}\exists {\mathit{ret}}_{\mathtt{I}}\exists \mathit{result}.\hfill \\ (\mathit{a}<0\iff \mathit{raise}\_\mathit{exception}\stackrel{\circ }{=}1)\wedge \hfill \\ \left(\right(\mathit{s}>\mathit{a}\wedge \mathit{do}\_\mathit{recursion}\stackrel{\circ }{=}0\wedge \mathit{result}\stackrel{\circ }{=}0)\vee \hfill \\ (\neg (\mathit{s}>\mathit{a})\wedge \mathit{do}\_\mathit{recursion}\stackrel{\circ }{=}1\wedge {\mathit{a}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{a}-\mathit{s}\wedge {\mathit{s}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{s}\wedge \hfill \\ \mathit{result}\stackrel{\circ }{=}\mathit{s}·{\mathit{ret}}_{\mathtt{f}}+{\mathit{ret}}_{\mathtt{I}}\left)\right)\hfill \end{array}$$

The variables $\mathit{a}$ and $\mathit{s}$ are the formal parameters in the definition of $\mathtt{I}(\mathit{a}:float,\mathit{s}:float)$. The others are fresh variables introduced to handle exceptions or function calls: the boolean flag $\mathit{raise}\_\mathit{exception}$ represents exception throwing, the boolean flag $\mathit{do}\_\mathit{recursion}$ has a true value only when a recursive call is made to $\mathtt{I}$ with actual parameters represented by the variables ${\mathit{a}}_{rec},{\mathit{s}}_{rec}$ and return value represented by ${\mathit{ret}}_{\mathtt{I}}$, while ${\mathit{ret}}_{\mathtt{f}}$ is the variable for the return value of the call to the function $\mathtt{f}$. The final return value of $\mathtt{I}$ is represented by the variable $\mathit{result}$. In what follows, we are not interested in the signs of the last three variables, so we quantify them existentially.

The sign behavior of function $\mathtt{I}$ is given by the formula’s sign abstraction $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$. Given that ${\varphi }_{\mathtt{I}}$ is not $h_{\mathbb{B}}$-mixed system, we cannot apply the algorithm from Theorem 6 directly to compute this sign abstraction. Nevertheless, it will be beneficial as we will illustrate below.

By John’s theorem, the sign abstraction $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$ can be overapproximated by the abstract interpretation $so{l}^{\mathbb{S}}\left({\varphi }_{\mathtt{I}}\right)$. Since $\mathbb{S}$ is a finite structure, this abstract interpretation can be computed by finite domain constraint programming. For this, we implemented a solver for first-order formulas over the structure $\mathbb{S}$ with Minizinc [17]. When applied to ${\varphi }_{\mathtt{I}}$ it returns the set of abstract solutions $so{l}^{\mathbb{S}}\left({\varphi }_{\mathtt{I}}\right)$ given in

Table 1. Set of abstract solutions in $so{l}^{\mathbb{S}}\left({\varphi }_{\mathtt{I}}\right)$. Six solutions with gray background color are unjustified since outside $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$.

#	$\mathit{raise}\_\mathit{exception}$	$\mathit{do}\_\mathit{recursion}$	$\mathit{a}$	$\mathit{s}$	${\mathit{a}}_{\mathit{rec}}$	${\mathit{s}}_{\mathit{rec}}$
1.	0	0	0	1	−1	1
2.	0	0	1	1	0	1
3.	0	0	1	1	−1	1
4.	0	0	1	1	1	1
5.	0	1	0	0	0	0
6.	0	1	1	0	1	0
7.	0	1	0	−1	1	−1
8.	0	1	1	1	0	1
9.	0	1	1	−1	1	−1
10.	0	1	1	1	−1	1
11.	0	1	1	1	1	1
12.	1	0	−1	0	−1	0
13.	1	0	−1	−1	0	−1
14.	1	0	−1	−1	−1	−1
15.	1	0	−1	−1	1	−1
16.	1	0	−1	1	−1	1
17.	1	1	−1	−1	0	−1
18.	1	1	−1	−1	−1	−1
19.	1	1	−1	−1	1	−1

. This set contains the 6 unjustified abstract solutions $2,4,10,13,15,18$ outside $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$. In the table they are distinguished by gray background color. We also note that the last three solutions $17,18,19$ could be ruled out when using a more precise abstract program interpretation, taking into account that no recursive call is possible when an exception is thrown.

The sets of abstract solutions provide information on possible sign of values of the parameters in a call $\mathtt{I}(\mathit{a}:float,\mathit{s}:float)$. For example, solution 1 in Table 1 states that when called with values of signs $[a/0,s/1]$ the function $\mathtt{I}$ will not raise an exceptions nor make a recursive call. Solution 8 states that when called with values of signs $[a/1,s/1]$ function $\mathtt{I}$ may go into recursion with signs $[a_{rec}/0,s_{rec}/1]$ without raising an exception.

Any set of abstract solutions defines an abstract call graph. The abstract call graphs of $so{l}^{\mathbb{S}}\left({\varphi }_{\mathtt{I}}\right)$ and $h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$ from Table 1 are given in Figure 7. Solution 1 in Table 1 implies a solid edge from the node ${\mathtt{I}}^{\mathbb{S}}(1,1)$ to the node ${\mathtt{I}}^{\mathbb{S}}(0,1)$. The edge is solid since solution 1 is justified. Edges induced by unjustified solutions are dashed. The unjustified solution 10 for instance induces the dashed edge from ${\mathtt{I}}^{\mathbb{S}}(1,1)$ to ${\mathtt{I}}^{\mathbb{S}}(1,-1)$. Solutions with $\mathit{do}\_\mathit{recursion}=0$ and $\mathit{raise}\_\mathit{exception}=0$ do not induce any edge. Instead, they show that the computation may stop, producing final nodes that are surrounded by a double circle. The final nodes are ${\mathtt{I}}^{\mathbb{S}}(1,1)$ and ${\mathtt{I}}^{\mathbb{S}}(0,1)$. Note that for all nonfinal nodes, either an exception is raised or the computation loops endlessly. Solutions with $\mathit{raise}\_\mathit{exception}=1$ induce an edge to the except node.

Given that only 2 unjustified solutions with $\mathit{do}\_\mathit{recursion}=0$ and $\mathit{raise}\_\mathit{exception}=0$ (10 and 18), there are only 2 dashed edges in the graph. Furthermore, the edges induced by the last three solutions 17, 18, 19 are drawn in blue, since these could be removed with a more precise abstract program interpretation than ${\varphi }_{\mathtt{I}}$.

The sign analysis without the unjustified dashed edges yields the following result: the program in state ${\mathtt{I}}^{\mathbb{S}}(1,1)$, where $a>0$ and $s>0$ may either terminate, loop indefinitely, or go to state ${\mathtt{I}}^{\mathbb{S}}(0,1)$ and terminate there immediately. With the unjustified dashed edges, however, it wrongly seems possible that the program may also raise an exception by passing through ${\mathtt{I}}^{\mathbb{S}}(-1,1)$. This overapproximation would be particularly unfortunate since state ${\mathtt{I}}^{\mathbb{S}}(1,1)$ is the only useful state to call $\mathtt{I}$.

We next show how to remove the unjustified solutions by applying the overapproxmation algorithm for the sign abstraction from Proposition 10, that lifts the algorithm for exact sign abstraction from Theorem 6 to a richer class of formulas. The idea is to split the formula ${\varphi }_{\mathtt{I}}$ into its linear part and the rest. Before doing so, we preprocess the inequation $\mathit{s}>\mathit{a}$: We introduce a fresh variable $\mathit{signvar}$, add the equation $\mathit{s}-\mathit{a}\stackrel{\circ }{=}\mathit{signvar}$, and rewrite $\mathit{s}>\mathit{a}$ to $\mathit{signvar}>0$. The linear part of ${\varphi }_{\mathtt{I}}$ then becomes:

$$\mathit{s}-\mathit{a}\stackrel{\circ }{=}\mathit{signvar}\wedge {\mathit{a}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{a}-\mathit{s}\wedge {\mathit{s}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{s}$$

We can then rewrite the linear part into the signature ${\Sigma }_{bool}$ by moving the negative parts positively onto the other side. This yields the following linear equation system:

$$\begin{array}{c}\hfill \mathit{s}\stackrel{\circ }{=}\mathit{signvar}+\mathit{a}\wedge {\mathit{a}}_{\mathit{rec}}+\mathit{s}\stackrel{\circ }{=}\mathit{a}\wedge {\mathit{s}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{s}\end{array}$$

The remainder of ${\varphi }_{\mathtt{I}}$ can be rewritten as follows:

$$\begin{array}{c}\left(\right(\mathit{a}<0\wedge \mathit{raise}\_\mathit{exception}>0)\vee (\mathit{a}\ge 0\wedge \mathit{raise}\_\mathit{exception}\stackrel{\circ }{=}0\left)\right)\hfill \\ \wedge \left(\right(\mathit{signvar}>0\wedge \mathit{do}\_\mathit{recursion}\stackrel{\circ }{=}0\wedge \mathit{result}\stackrel{\circ }{=}0)\vee \hfill \\ (\mathit{signvar}\le 0\wedge \mathit{do}\_\mathit{recursion}>0\wedge \mathit{result}\stackrel{\circ }{=}\mathit{s}\ast {\mathit{ret}}_{\mathtt{f}}+{\mathit{ret}}_{\mathtt{I}}))\hfill \end{array}$$

It is not clear whether the conjunction of both parts is a $h_{\mathbb{B}}$-mixed system, since it is not clear how to show the $h_{\mathbb{B}}$-invariance of the equation $\mathit{result}\stackrel{\circ }{=}\mathit{s}\ast {\mathit{ret}}_{\mathtt{f}}+{\mathit{ret}}_{\mathtt{I}}$. Still, we can apply the overapproximation algorithm of the sign abstraction from Proposition 10. It indeed improves on John’s approximation, ruling out both unjustified solutions. The details are worked out in Appendix A.

In the general case, linear equation systems are not enough, in which case our algorithm from Theorem 6 for computing sign abstractions cannot be applied. But then we can still apply the overapproximation algorithm from Proposition 10 which rewrites a linear part of the formula exactly. As illustrated by the present example, this overapproximation is often way more precise than John’s.

11. Example for the Overapproximation of the Sign Abstraction

We reconsider conjunction of the linear part obtained and the rest of ${\varphi }_{\mathtt{I}}$, that is ${\varphi }_{\mathtt{I}}^{lin}\wedge {\varphi }_{\mathtt{I}}^{rest}$ where:

$${\varphi }_{\mathtt{I}}^{lin}{=}_{\mathrm{def}}\left\{\begin{array}{cc}\hfill & \mathit{s}\stackrel{\circ }{=}\mathit{signvar}+\mathit{a}\hfill \\ \wedge \hfill & {\mathit{a}}_{\mathit{rec}}+\mathit{s}\stackrel{\circ }{=}\mathit{a}\hfill \\ \wedge \hfill & {\mathit{s}}_{\mathit{rec}}\stackrel{\circ }{=}\mathit{s}\hfill \end{array}\right.$$

$${\varphi }_{\mathtt{I}}^{rest}{=}_{\mathrm{def}}\left\{\begin{array}{ccc}\hfill & (\hfill & (\mathit{a}<0\wedge \mathit{raise}\_\mathit{exception}>0)\hfill \\ \hfill & \vee \hfill & (\mathit{a}\ge 0\wedge \mathit{raise}\_\mathit{exception}\stackrel{\circ }{=}0))\hfill \\ \wedge \hfill & (\hfill & (\mathit{signvar}>0\wedge \mathit{do}\_\mathit{recursion}\stackrel{\circ }{=}0\wedge \mathit{result}\stackrel{\circ }{=}0)\hfill \\ \hfill & \vee \hfill & (\mathit{signvar}\le 0\wedge \mathit{do}\_\mathit{recursion}>0\wedge \mathit{result}\stackrel{\circ }{=}\mathit{s}\ast {\mathit{ret}}_{\mathtt{f}}+{\mathit{ret}}_{\mathtt{I}}))\hfill \end{array}\right.$$

The decomposition of the linear subsystem ${dec}_{\nu }\left({\varphi }_{\mathtt{I}}^{lin}\right)$ for interpretation over $\mathbb{B}$ as defined in Section 9 is obtained by splitting each variable x into two fresh variables ${\nu }_{\oplus }\left(x\right)$ and ${\nu }_{\ominus }\left(x\right)$ representing its positive and negative part:

$${dec}_{\nu }\left({\varphi }_{\mathtt{I}}^{lin}\right)=\left\{\begin{array}{cc}\hfill & {\nu }_{\oplus }\left(\mathit{s}\right)+{\nu }_{\ominus }\left(\mathit{a}\right)+{\nu }_{\ominus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}{\nu }_{\ominus }\left(\mathit{s}\right)+{\nu }_{\oplus }\left(\mathit{a}\right)+{\nu }_{\oplus }\left(\mathit{signvar}\right)\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{a}}_{\mathit{rec}}\right)+{\nu }_{\ominus }\left(\mathit{a}\right)+{\nu }_{\oplus }\left(\mathit{s}\right)\stackrel{\circ }{=}{\nu }_{\ominus }\left({\mathit{a}}_{\mathit{rec}}\right)+{\nu }_{\oplus }\left(\mathit{a}\right)+{\nu }_{\ominus }\left(\mathit{s}\right)\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{s}}_{\mathit{rec}}\right)+{\nu }_{\ominus }\left(\mathit{s}\right)\stackrel{\circ }{=}{\nu }_{\ominus }\left({\mathit{s}}_{\mathit{rec}}\right)+{\nu }_{\oplus }\left(\mathit{s}\right)\hfill \end{array}\right.$$

The additional constraints on the decomposition variables are:

$$\begin{array}{cc}\hfill & {\nu }_{\oplus }\left(\mathit{s}\right)\ast {\nu }_{\ominus }\left(\mathit{s}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{a}\right)\ast {\nu }_{\ominus }\left(\mathit{a}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{signvar}\right)\ast {\nu }_{\ominus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{a}}_{\mathit{rec}}\right)\ast {\nu }_{\ominus }\left({\mathit{a}}_{\mathit{rec}}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{s}}_{\mathit{rec}}\right)\ast {\nu }_{\ominus }\left({\mathit{s}}_{\mathit{rec}}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{result}\right)\ast {\nu }_{\ominus }\left(\mathit{result}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{I}}\right)\ast {\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{I}}\right)\stackrel{\circ }{=}0\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{f}}\right)\ast {\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{f}}\right)\stackrel{\circ }{=}0\hfill \end{array}$$

The elementary mode rewriting $\mathit{emr}\left({dec}_{\nu }\left({\varphi }_{\mathtt{I}}^{lin}\right)\right)$ is the following ${\mathbb{R}}_{+}$-equivalent $h_{\mathbb{B}}$-exact ${\Sigma }_{bool}$-formula obtained via Corollary 1:

$$\begin{array}{cc}\hfill & \exists x_0\dots \exists x_{10}.\hfill \\ \wedge \hfill & {\nu }_{\ominus }\left(\mathit{a}\right)\stackrel{\circ }{=}{x}_{10}+x_8+x_9\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{a}\right)\stackrel{\circ }{=}{x}_{10}+x_6+x_7\hfill \\ \wedge \hfill & {\nu }_{\ominus }\left({\mathit{a}}_{\mathit{rec}}\right)\stackrel{\circ }{=}{x}_4+x_5+x_9\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{a}}_{\mathit{rec}}\right)\stackrel{\circ }{=}{x}_3+x_5+x_7\hfill \\ \wedge \hfill & {\nu }_{\ominus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}{x}_2+x_3+x_7\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}{x}_2+x_4+x_9\hfill \\ \wedge \hfill & {\nu }_{\ominus }\left(\mathit{s}\right)\stackrel{\circ }{=}{x}_1+x_3+x_8\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left(\mathit{s}\right)\stackrel{\circ }{=}{x}_1+x_4+x_6\hfill \\ \wedge \hfill & {\nu }_{\ominus }\left({\mathit{s}}_{\mathit{rec}}\right)\stackrel{\circ }{=}{x}_0+x_3+x_8\hfill \\ \wedge \hfill & {\nu }_{\oplus }\left({\mathit{s}}_{\mathit{rec}}\right)\stackrel{\circ }{=}{x}_0+x_4+x_6\hfill \end{array}$$

The nonlinear remainder also needs to be rewritten with the decomposition variables for interpretation over $\mathbb{B}$. The formula below is ${dec}_{\nu }\left({\varphi }_{\mathtt{I}}^{lin}\right)$ except that we simplified the rewriting of inequations a bit.

$$\begin{array}{ccc}\hfill & (\hfill & (\neg {\nu }_{\ominus }\left(\mathit{a}\right)\stackrel{\circ }{=}0\wedge \neg {\nu }_{\oplus }(\mathit{raise}\_\mathit{exception})\stackrel{\circ }{=}0)\hfill \\ \hfill & \vee \hfill & ({\nu }_{\ominus }\left(\mathit{a}\right)\stackrel{\circ }{=}0\wedge {\nu }_{\ominus }(\mathit{raise}\_\mathit{exception})\stackrel{\circ }{=}0\wedge {\nu }_{\oplus }(\mathit{raise}\_\mathit{exception})\stackrel{\circ }{=}0))\hfill \\ \wedge \hfill & (\hfill & (\neg {\nu }_{\oplus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}0\wedge {\nu }_{\ominus }(\mathit{do}\_\mathit{recursion})\stackrel{\circ }{=}0\wedge {\nu }_{\oplus }(\mathit{do}\_\mathit{recursion})\stackrel{\circ }{=}0\hfill \\ \hfill & \hfill & \wedge {\nu }_{\ominus }\left(\mathit{result}\right)\stackrel{\circ }{=}0\wedge {\nu }_{\oplus }\left(\mathit{result}\right)\stackrel{\circ }{=}0)\hfill \\ \hfill & \vee \hfill & ({\nu }_{\oplus }\left(\mathit{signvar}\right)\stackrel{\circ }{=}0\wedge \neg {\nu }_{\oplus }(\mathit{do}\_\mathit{recursion})\stackrel{\circ }{=}0\hfill \\ \hfill & \hfill & \wedge {\nu }_{\oplus }\left(\mathit{result}\right)+{\nu }_{\ominus }\left(\mathit{s}\right)\ast {\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{f}}\right)+{\nu }_{\oplus }\left(\mathit{s}\right)\ast {\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{f}}\right)+{\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{I}}\right))\hfill \\ \hfill & \hfill & \stackrel{\circ }{=}{\nu }_{\ominus }\left(\mathit{result}\right)+{\nu }_{\oplus }\left(\mathit{s}\right)\ast {\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{f}}\right)+{\nu }_{\ominus }\left(\mathit{s}\right)\ast {\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{f}}\right)+{\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{I}}\right)\left)\right)\hfill \end{array}$$

For any solution $\tau$ of the conjunction of the above three blocks of formulas over the algebra of booleans $\mathbb{B}$, we then obtain an assignment $\sigma \in h_{\mathbb{S}}\circ so{l}^{\mathbb{R}}\left({\varphi }_{\mathtt{I}}\right)$ according to Theorem 6:

$$\begin{array}{c}\sigma \left(\mathit{s}\right)=\tau \left({\nu }_{\oplus }\left(\mathit{s}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(\mathit{s}\right)\right)\hfill \\ \sigma \left(\mathit{a}\right)=\tau \left({\nu }_{\oplus }\left(\mathit{a}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(\mathit{a}\right)\right)\hfill \\ \sigma \left(\mathit{signvar}\right)=\tau \left({\nu }_{\oplus }\left(\mathit{signvar}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(\mathit{signvar}\right)\right)\hfill \\ \sigma \left({\mathit{a}}_{\mathit{rec}}\right)=\tau \left({\nu }_{\oplus }\left({\mathit{a}}_{\mathit{rec}}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left({\mathit{a}}_{\mathit{rec}}\right)\right)\hfill \\ \sigma \left({\mathit{s}}_{\mathit{rec}}\right)=\tau \left({\nu }_{\oplus }\left({\mathit{s}}_{\mathit{rec}}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left({\mathit{s}}_{\mathit{rec}}\right)\right)\hfill \\ \sigma \left(\mathit{result}\right)=\tau \left({\nu }_{\oplus }\left(\mathit{result}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left(\mathit{result}\right)\right)\hfill \\ \sigma \left({\mathit{ret}}_{\mathtt{f}}\right)=\tau \left({\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{f}}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{f}}\right)\right)\hfill \\ \sigma \left({\mathit{ret}}_{\mathtt{I}}\right)=\tau \left({\nu }_{\oplus }\left({\mathit{ret}}_{\mathtt{I}}\right)\right){-}^{\mathbb{R}}\tau \left({\nu }_{\ominus }\left({\mathit{ret}}_{\mathtt{I}}\right)\right)\hfill \end{array}$$

12. Conclusions and Future Work

We showed that any $h_{\mathbb{B}}$-mixed system can be rewritten into an $h_{\mathbb{B}}$-exact formula by computing the elementary modes of the linear subsystem. In previous work, $h_{\mathbb{B}}$-exact rewriting $h_{\mathbb{B}}$-mixed systems was applied to compute difference abstractions exactly. In the present paper, we showed that $h_{\mathbb{B}}$-exact rewriting can also be used to compute sign-abstractions exactly.

We have illustrated the usefulness of the computation of sign abstraction for linear formulas for the sign analysis of function programs. Using John’s overapproximation is often not good enough for such applications, since the relationships between the signs of different variables are quickly lost. We saw that elementary mode rewriting yields better a better approximation of the sign abstraction even for nonlinear equation systems, which may preserve these relationships.

The time for computing abstractions exactly strongly depends on the time needed to compute the elementary modes. Some experiments were reported in [6] in the case of the difference abstraction. There, one has to compute the elementary modes for a linear equation system that contains two copies of the linear equation system given with the input. The copying doubles the size and may increase the time for the computation of the elementary modes seriously. In the application of difference abstraction to change prediction of reaction networks, we observed cases where John’s overapproximation of the difference abstraction could be computed in circa 10 min, while the exact computation required circa 10 h.

In the future, it would we of interest to find heuristics for approximating abstractions of linear equation systems that reduce the computation time of the exact algorithm while improving John’s overapproximation in precision. In the case of difference abstractions, the minimal support heuristics was proposed for this purpose [6]. In the example mentioned above, this heuristics could be computed in circa 10 min, like John’s overapproximation, while yielding the exact result. In general, however, the minimal support heuristics is not exact.

Another interesting question for future work is how to compute more quantitative abstractions exactly, as for instance with intervals. In this case however the structure of abstract values is infinite, therefore finite domain constraint programming is no longer sufficient to compute the set of abstract solutions.