Previous chapter: Linear Arithmetic (Theory)
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
In last section, we have seen the definiton of Linera Arithmetic, which is similar to S1S. Let see how we can apply it in math and moreover, the connection between logic and automata.
Encoding Real Numbers
We can encode any real number $x\in\mathbb{R}$ into the form $(0+1)(0+1)^\ast{$}(0+1)^\omega$ in two steps:
Step 1
For a real number $x\in\mathbb{R}$, represent it as a pair $(x_I,x_F)$ so that $x=x_I+x_F$.
integer part = $x_I\in\mathbb{Z}$, and fractional part = $x_F\in[0, 1]$, a real number between $0$ and $1$ (both inclusive)
For example, the $1.5 = (1, 0.5)$, and $-{2\over 3}=(−1, {1\over3})$. Note that integers always have two different representations depends on setting the fractional part as $0$ or $1$, and Negative sign can only be represented using the integer part. For example $3=(2,1)$ or $(3,0)$
Step 2
Then we can further encode $(x_I,x_F)$ as an infinite word $w_I{$}\beta_F$,
$x_I$ is encoded as $w_I=a_na_{n−1}\dots a_0\in\lbrace 0,1\rbrace^\ast$, a finite nonempty word, and
$x_F$ is encoded as $\beta_F=b_1b_2\dots\in\lbrace 0,1\rbrace^\omega$, an infinite word such that
$$x_I=-a_n\cdot 2^n+ \sum_{i=0}^{n-1}a_i\cdot 2^i
\hspace{2cm}\text{and}\hspace{2cm}
x_F= \sum_{i=1}^{\infty}b_i\cdot 2^{-i}$$
Note that now every pair has (infinitely) many different encodings because digits are forever:
for example, $(0,{1\over2})$ is encoded by all words in $0^\ast0{$}10^\omega = {1\over2}+0+0+\dots$ and $0^\ast0{$}01^\omega=0+{1\over4}+{1\over8}+\dots$.
As you may notice, we can always increase the length of the finite integer part by ‘padding’ arbitrary finitely long $0$ and $1$ on positive and negative number respectively. This is becasue of the following property of the geometric-series sum: for all $a$, $n$, $k$, we have that:
$$-a_n\cdot 2^n=-a\cdot 2^{n+k}+ \sum_{j=0}^{k}a\cdot 2^{n+j}$$
For example, $110{$}0^\omega=-1\ast2^2+1\ast2^1=-2$, $11110{$}0^\omega=-1\ast2^4+1\ast2^3+1\ast2^2+1\ast2^1=-2$,
Example
| $x\in\mathbb{R}$ | $(x_I,x_F)$ | $w_I{$}\beta_F$ |
|---|---|---|
| $1$ | $(1, 0)$ | $0^\ast01{$}0^\omega$ and $0^\ast0{$}1^\omega$ |
| ${4\over 3}$ | $(1, {1\over 3})$ | $0^\ast01{$}(01)^\omega$ |
| $-{3\over 2}$ | $(-2, {1\over 2})$ | $1^\ast10{$}10^\omega$ |
$0^\ast/1^\ast$ may be empty so make sure there is at least one $0$ or $1$ to ensure it is positive or negative, respectively.
Encoding Valuations $\sigma:V’\rightarrow\mathbb{R}$
Assume there’s an arbitrary ordering of the free variables $V’=\lbrace x_0,x_1,\dots,x_k\rbrace$. The valuation is then encoded as a word $\alpha_\sigma$ over the alphabet $\lbrace0,1\rbrace^k\cup\lbrace{$}\rbrace^k$. Each letter of the word $\alpha_\sigma$ is a tuple, where the $i$-th position indicates the encoding of $x_i$. Also, we ensure that the encodings of all $x_i$ synchronize on the separation symbol ${$}$
Continue the example, one possible encoding of the valuation $x_1\mapsto1$, $x_2\mapsto{4\over3}$, $x_3\mapsto-{3\over2}$ is the infinite word
$$\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\left(\begin{bmatrix}0\newline 1\newline 0\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\right)^\omega$$
In the next section, we will illustrate an example of translation from linear arithmetic to automata.
Next chapter: Translation from Linear Arithmetic to Automata
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