🍽 🥨 MensaarLecker -- A beloved tool to find out Mensa Ladies' favourite menu using Selenium🥨 🍽

Previous chapter: Encoding real numbers

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

In this section, we will illustrate the key ideas in the translation from linear arithmetic to automata through a simple example.

Consider the formula $x+y=z$ and the following encoding of the valuation $x\mapsto1$, $y\mapsto1$, $z\mapsto2$:

$$\alpha_\sigma=\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix} \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline 2\end{bmatrix}$$

Homogeneity

A equation is homogenous if there are no constant terms. The key property of homogeneity is that we can simply scaling without being unbounded. In other words, for a homogenous equation $D$, we have:

$D∼0$ (where $∼$ is an arbitrary (in)equality) if and only if, for all $k\in\mathbb{Z},2^k\cdot D∼0$. (Scaling behaviour)

As we can see the equation $x+y=z$ is homogenous, i.e., $D: x+y−z = 0$ and $2^k\cdot x+2^k\cdot y−2^k\cdot z∼0$

We immediately observe that:

• $2^k\cdot D$ has constant sign,
• If $D\neq0$, it is strictly increasing in $k$, and thus
• For any threshold $N$, we will have that $|2^k\cdot D|>N$ for all sufficiently large $k$.

Shifting the ${$}$ Delimiter

The key observation is that multiplying by a power of $2$ = shifting the ${$}$ delimiter in the binary representation.

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix} \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline{$}\newline{$}\end{bmatrix} \left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega= \begin{bmatrix}1\newline 1\newline 2\end{bmatrix},\newline \begin{bmatrix}2^2\cdot x\newline 2^2\cdot y\newline 2^2\cdot z\end{bmatrix} = \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix} \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix} \begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline{$}\newline{$}\end{bmatrix} \left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega= \begin{bmatrix}2^2\cdot 1\newline 2^2\cdot 1\newline 2^2\cdot 2\end{bmatrix}= \begin{bmatrix}4\newline 4\newline 8\end{bmatrix},$$

For any variable $z$, and $t\geq1$, we denote by $z_t$ the integer encoded by the leftmost $t$ digits of $z$ (the ${$}$ is ignored):

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix} \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix} \begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\dots$$

$\begin{array}{lclc} \hspace{1cm}\cdot\ x_5 =& -2^4\cdot0+2^3\cdot0+2^2\cdot0+2^1\cdot1+2^0\cdot1&=&3\newline \hspace{1cm}\cdot\ y_3 =& -2^2\cdot0+2^1\cdot0+2^0\cdot0&=&0\newline \hspace{1cm}\cdot\ z_4 =& -2^3\cdot0+2^2\cdot1+2^1\cdot0+2^1\cdot0&=&4\newline \hspace{1cm}\cdot\ z_5 =& -2^4\cdot0+2^3\cdot1+2^1\cdot0+2^2\cdot0+2^0\cdot0&=&8\newline \end{array}$

key linear recurrence

We can see the above definition is initialized as $z_1=−c_{z,1}$, and key linear recurrence holds for any variable: $z_{t+1}=2z_t+c_{z,t+1}$, where $c_{z,t+1}$ is the $(t+1)$-th digit from the left in the encoding of $z$.

Now, in our example we can define $D_t=x_t+y_t−z_t$, and by linearity, the same recurrences hold for $D_t$, too:

$$D_1=c_{z,1}-c_{x,1}-c_{y,1}\newline D_{t+1}=2D_t+c_{z,t}-c_{x,t}-c_{y,t}$$

Thus, we have $D_1=0,D_2=−1,D_3=−2$, and $D_t=−2$ for subsequent $t$.

Fractional part

To account for the digits other than the $t$ leftmost digits, we define the fractional part $\lbrack z\rbrack_t = \sum_{i=1}^{\infty}2^{-i}\cdot c_{z,t+i}$.

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix} \begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix} \begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\dots$$

$\begin{array}{lclc} \hspace{1cm}\cdot\ [x]_1 =& 2^{-1}\cdot0+2^{-2}\cdot0+2^{-3}\cdot1+2^{-4}\cdot1+\dots&=&{1\over4}\newline \hspace{1cm}\cdot\ [y]_2 =& 2^{-1}\cdot0+2^{-2}\cdot1+2^{-3}\cdot1+2^{-4}\cdot1+\dots&=&{1\over2}\newline \hspace{1cm}\cdot\ [z]_1 =& 2^{-1}\cdot1+2^{-2}\cdot0+2^{-3}\cdot0+\dots&=&{1\over2}\newline \hspace{1cm}\cdot\ [z]_3 =& 2^{-1}\cdot0+2^{-2}\cdot0+2^{-3}\cdot0+\dots&=&0\newline \end{array}$

Here, we can see $0\leq[z]_t\leq1$, and that $z_t+[z]_t = 2^k\cdot z$ for some $k\in\mathbb{Z}$.

If the $2^k\cdot z$ doesn’t seem intuitive to you, check this out:
let say we have $z=011{$}0111\dots = 3+{1\over2}=3.5$, and we set $t=7$, so $z_7=-2^6\cdot0+2^5\cdot1+2^4\cdot1+2^3\cdot0+2^2\cdot1+2^1\cdot1+2^0\cdot1=55$ and $[z]_7={1\over2}+{1\over4}+{1\over8}+\cdots=1$. Thus we have $z_7+[z]_7 = 56 = 2^4\cdot 3.5$.

We can then extend the definition of fractional part to $D$ in the obvious way: $[D]_t = [x]_t+[y]_t−[z]_t$.
We thus have that $−1\leq [D]_t\leq 2$, and that $D_t+[D]_t=2^k\cdot D$ for some $k$.

1. If $D_t<−2$ for some $t$. then $D_t+[D]_t<0$. For the corresponding $k$, we have that $2^k \cdot D<0$. Therefore $x+y-z<0$ and thus we conclude $x+y<z$.

2. If $D_t>1$ for some $t$, then $D_t+[D]_t>0$. For the corresponding $k$, we have that $2^k \cdot D>0$. Therefore $x+y-z>0$ and thus we conclude $x+y>z$.

3. If $−2\leq D_t\leq 1$ for all $t$, then $|D_t+[D]_t|\leq 3$. For arbitrarily large $k$, $|2^k\cdot D|\leq3$. This implies that $x+y=z$ (only option left)

From Linear Arithmetic to Automaton

From the above deduction, $x+y=z$ holds if and only if $−2\leq D_t\leq 1$. To check whether it holds with an automaton, we use the encoding to compute the sequence $D_t$ term by term, and accept if and only if each term is at least $−2$ and at most $1$.

Indeed, in our example, the sequence of terms is $0,−1,−2,−2,\dots$, and we accept.

As an example, we could also consider a different encoding of $x\mapsto1$, $y\mapsto1$, $z\mapsto2$:

$$\alpha’_\sigma=\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 1\end{bmatrix} \begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline 2\end{bmatrix}$$

In this example the sequence of $D_t$ is $0, 1, 1, 1,\dots$, which is again bounded, and we accept.

On the other hand, a rejecting example may look like this:

$$\alpha_{\sigma’}=\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix} \begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline -2\end{bmatrix}$$

The sequence of $D_t$ is $1, 4, 8, 15,\dots$, which is out of bounded, and we reject.

---

Next chapter: Homogenous Inequality Testing is Automatic

Further Reading:

---

Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com