This is the thirty eighth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Today we are going to implement basic data structure: array. If you know functional programming and immutable data structures, you will find this post as almost direct implementation of that concepts.

Table of Contents

Idea

Let’s begin with explaining what an array is. In our case this is simply a zero-based vector of variables. Having such a vector we can extract element with specified index, or set value at specified index. Our array is static — it will not expand dynamically. We are also not going to cover bound checks, we assume that we use correct indexes.

More formally, we have the following array:

$\begin{gather*} A = (a_0, a_1, \ldots, a_{n-1}) \end{gather*}$

We can extract element:

$\begin{gather*} x = \text{Get}(A, i) \equiv x = a_i \end{gather*}$

We can also set element:

$\begin{gather*} \text{Set}(A, i, a_{i}') \equiv A = (a_0, a_1, \ldots, a_{i-1}, a_{i}', a_{i+1}, \ldots, a_{n-1}) \end{gather*}$

Extracting element

In order to get element we could use simple conditions:

$\begin{gather*} x = \text{Get}(A, i) \equiv \\ \equiv x = i \stackrel{?}{=} 0\ ?\ a_0 : \\ i \stackrel{?}{=} 1\ ?\ a_1 : \\ \cdots \\ i \stackrel{?}{=} n-1\ ?\ a_{n-1} : \\ 0 \end{gather*}$

We compare index with consecutive values and extract matching value from the array. If we cannot match the index — we return zero (or any other default value).

However, this is a bit slow. In theory we could implement binary search to match the index, but for now let’s stick to linear search.

However, instead of using conditions, we can simulate them in binary logic. Key idea here is: if we define result value ( $x$ in our case), we can construct constraint saying that $x$ must be equal to some value when index matches position in element. Crazy, huh? Formula is:

$\begin{gather*} \text{Get}(A, i) \equiv \\ i \stackrel{?}{=} 0 \implies x \stackrel{?}{=} a_0 = 1 \\ i \stackrel{?}{=} 1 \implies x \stackrel{?}{=} a_1 = 1 \\ \cdots \\ i \stackrel{?}{=} n-1 \implies x \stackrel{?}{=} a_{n-1} = 1 \end{gather*}$

How does it work? If $i$ is not zero, left side of implication is false. This means, that whole implication is true (remember logic tables?), so this constraints changes nothing. We move on to next value. When we come to the right value, which means that $i$ is equal to some specified index, left side of implication is true. Since we require whole implication to hold, its right side must be true as well — this means, that $x$ will get value of $a_i$ . We still compare values but we don’t need to calculate condition operation which is quite heavy.

Please also note, that this has unspecified behavior when index doesn’t point to any correct index — previous approach returned default value in that case, this time $x$ can be simply anything.

Setting element

This part is a bit harder — in theory any element can be modified, so we need to update all of them:

$\begin{gather*} \text{Set}(A, i, a_{i}') \equiv \\ a_0 = i \stackrel{?}{=} 0\ ?\ a_{i}' : a_0 \\ a_1 = i \stackrel{?}{=} 1\ ?\ a_{i}' : a_1 \\ \cdots \\ a_{n-1} = i \stackrel{?}{=} n-1\ ?\ a_{i}' : a_{n-1} \end{gather*}$

Summary

This is whole implementation. Extraction takes linear time, changing element takes linear time as well. However, please note that this structure can be easily transformed into dictionary. Next time we will see how to utilize array to implement nondeterministic Turing machine in ILP. Stay tuned.