Abstract Interpretation: prove that the sign subtraction is increasing in each of its parameters

I need to prove that the binary operator $$-_\pm: \mathbb{P}^\pm\times\mathbb{P}^\pm\rightarrow\mathbb{P}^\pm$$ is increasing in each of its arguments, where

$$\mathbb{P}^\pm = \{\top_\pm, \leq0,\neq0, \geq0,<0,=0,>0,\bot_\pm\}$$

are the abstract properties it operates on. They represent the "signs" of values in $$\mathbb Z$$.

Their concretizations are, resp.,

$$\mathcal{P}^\pm = \{ \mathbb Z, \{z \in \mathbb Z \mid z \leq0\}, \{z \in \mathbb Z \mid z \neq0\}, \{z \in \mathbb Z \mid z \geq0\}, \ldots, \emptyset \}$$

The concretization of a sign property $$s$$ is given by $$\gamma(s)$$, where $$\gamma$$ is an isomorphism between the posets $$(\mathcal{P}^\pm, \subseteq)$$ and $$(\mathbb{P}^\pm, \sqsubseteq)$$, and

$$\forall s_1,s_2\in\mathbb{P}^\pm . s_1 \sqsubseteq s_2 \iff \gamma(s_1)\subseteq\gamma(s_2).$$

I couldn't find any smart way to prove the monotonicity of $$-_\pm$$, so I just built an $$8\times8$$ "subtraction table" with $$s_1-_\pm s_2$$ for every possible pair of signs. For each valid $$i$$, let $$r_i$$ be the $$i$$-th row, and $$s_i$$ the property associated with $$r_i$$. I simply verified that if $$s_i \sqsubseteq s_j$$ then, for all valid $$k$$, $$r_{ik}\sqsubseteq r_{jk}$$. I did the same for the columns.

This is quite bruteforc-y, although it didn't take long thanks to the table. I'd just like to know whether this is the correct way to solve this exercise or not.

• Abstract Interpretation is a formal method for statically analyzing the behavior of programs. My question is about an exercise from the book "Principles of Abstract Interpretation". Oct 5, 2023 at 21:40

If $$P$$ is a property, let $$\alpha(P)$$ be its best sound abstraction. "Sound" means that $$P\subseteq \gamma(\alpha(P))$$, that is, $$\alpha(P)$$ overapproximates $$P$$. "Best" means that if $$p$$ is another sound abstraction of $$P$$, then $$\alpha(P)\sqsubseteq p$$, that is, $$\gamma(\alpha(P))\subseteq \gamma(p)$$, that is, $$\alpha(P)$$ is more precise.

The operator $$-_\pm$$ was naturally defined such that it's optimal w.r.t. the abstract properties, that is

$$s_1 -_\pm s_2 = \alpha_\pm (\{x-y \mid x\in \gamma_\pm(s_1) \wedge y\in \gamma_\pm(s_2)\})$$

For instance:

\begin{align} (>0) -_\pm (<0) &= \alpha_\pm(\{x \mid x>0\} -^* \{y \mid y<0\}) \\ &= \alpha_\pm(\{x \mid x>0\} +^* \{y \mid y>0\}) \\ &= \alpha_\pm(\{x \mid x>0\}) \\ &= (>0) \end{align}

where I introduced the two star operators for convenience. (I leave the trivial definition to the reader.)

Let's define $$f$$ as follows:

$$f(s, t) = \{x-y \mid x\in \gamma_\pm(s) \wedge y\in \gamma_\pm(t)\}$$

Note that $$s_1\ -_\pm s_2 = \alpha_\pm(f(s_1, s_2))$$.

It's now easy to see that, for all valid $$s_2$$:

\begin{align} s_1 \sqsubseteq s_1' &\implies \gamma_\pm(s_1) \subseteq \gamma_\pm (s_1') \\ &\implies f(s_1, s_2) \subseteq f(s_1', s_2) \\ &\implies s_1 -_\pm s_2 \sqsubseteq s_1' -_\pm s_2 \end{align}

The last implication follows from the fact that $$\alpha$$ is also increasing. Indeed, for every properties $$P$$ and $$Q$$ such that $$P \subseteq Q$$, we must have $$P \subseteq Q \subseteq \gamma(\alpha(Q))$$, which means that $$\alpha(Q)$$ is also a sound abstraction for $$P$$. For the optimality of $$\alpha$$, we must thus have $$\alpha(P) \sqsubseteq \alpha(Q)$$, which proves the monotonicity.

We can reason analogously for $$s_2$$, which concludes the proof.