Defining a Torus of Exponential Size

Similar to proving undecidability by reduction of unbounded domino problems, where defining infinite grids is the key problem, defining a torus of exponential size is the key to obtaining a -completeness proof by reduction of bounded domino problems.

To be able to apply Corollary 3.3 to consistency for , we must characterise the torus $\mathbb{Z} _{2^n} \times \mathbb{Z} _{2^n}$ with a of polynomial size. To characterise this torus, we use 2n concepts $X_0,\dots,X_{n-1}$ and $Y_0,\dots,Y_{n-1}$, where X_i (resp., Y_i) codes the ith bit of the binary representation of the X-coordinate (resp., Y-coordinate) of an element a.

For an interpretation $\mathcal{I}$ and an element $a \in \Delta^\mathcal{I}$, we define $\textit{pos}\xspace(a)$by

$$\begin{gather*}\textit{pos}\xspace(a) := (\textit{xpos}(a), \textit{ypos}(a)) :=... ...cal{I}$ } \\ 1, & \text{otherwise} \ . \end{cases} \end{array} \end{gather*}$$

We use a well-known characterisation of binary addition (e.g. [BGG97]) to relate the positions of the elements in the torus:

Lemma 3.4
Let x,x' be natural numbers with binary representations

$$x = \sum_{i=0}^{n-1} x_i \cdot 2^i \quad \text{and} \quad x' = \sum_{i=0}^{n-1} x'_i \cdot 2^i .$$

Then
$$\begin{multline*}\begin{split} x' \equiv x+1 \pmod{2^n} \quad \text{iff} \quad ... ...{j=0}^{k-1} x_j = 0) \rightarrow (x_k = x'_k) \; , \end{split} \end{multline*}$$
where the empty conjunction and disjunction are interpreted as true and false, respectively.

  

Figure 3: A TCBOX defining a torus of exponential size

The T_n is defined in Figure 3. The concept C_(0,0) is satisfied by all elements a of the domain for which $\textit{pos}\xspace(a) = (0,0)$ holds. C_{(2ⁿ-1,2ⁿ-1)} is a similar concept, whose instances asatisfy $\textit{pos}\xspace(a) = (2^n-1, 2^n-1)$.

The concept $D_{\textit{north}}\xspace$ is similar to $D_{\textit{east}}\xspace$ where the role ${\textit{north}}\xspace$ has been substituted for ${\textit{east}}\xspace$ and variables X_i and Y_i have been swapped. The concept $D_{\textit{east}}\xspace$ (resp. $D_{\textit{north}}\xspace$) enforces that, along the role ${\textit{east}}\xspace$(resp. ${\textit{north}}\xspace$), the value of $\textit{xpos}$ (resp. $\textit{ypos}$) increases by one while the value of $\textit{ypos}$ (resp. $\textit{xpos}$) is unchanged. They are analogous to the formula in Lemma 3.4.

The following lemma is a consequence of the definition of $\textit{pos}\xspace$ and Lemma 3.4.

Lemma 3.5
Let $\mathcal{I} = (\Delta^\mathcal{I},\cdot^\mathcal{I})$ be an interpretation, $D_{\textit{east}}\xspace, D_{\textit{north}}\xspace$ defined as in Figure 3, and $a,b \in \Delta^\mathcal{I}$.

$$\begin{gather*}\begin{array}{lll} \text{$(a,b) \in {\textit{east}}\xspace^\math... ...xtit{ypos}(b) & \equiv \textit{ypos}(a) +1 \pmod{2^n} \end{array} \end{gather*}$$

The T_n defines a torus of exponential size in the following sense:

Lemma 3.6
Let T_n be the as defined in Figure 3. Let $\mathcal{I} = (\Delta^\mathcal{I},\cdot^\mathcal{I})$ be a model of T_n. Then

$$(\Delta^\mathcal{I},{\textit{east}}\xspace^\mathcal{I},{\textit{north}}\xspace^\mathcal{I}) \cong (U(2^n,2^n),S_1,S_2) \; ,$$

where U(2ⁿ,2ⁿ) is the torus $\mathbb{Z} _{2^n} \times \mathbb{Z} _{2^n}$ and S₁,S₂ are the horizontal and vertical successor relations on this torus.

Proof. We show that the function pos is an isomorphism from $\ensuremath{\Delta^\mathcal{I}}$ to U(2ⁿ,2ⁿ). Injectivity of $\textit{pos}\xspace$ is shown by induction on the ``Manhattan distance'' d(a) of the $\textit{pos}\xspace$-value of an element a to the $\textit{pos}\xspace$-value of the upper right corner.

For an element $a \in \Delta^\mathcal{I}$ we define d(a) by

$$d(a) = (2^n-1 - \textit{xpos}(a)) + (2^n-1 - \textit{ypos}(a)) .$$

Note that $\textit{pos}\xspace(a) = \textit{pos}\xspace(b)$ implies d(a) = d(b). Since $\mathcal{I}\models (\leqslant 1 \; C_{(2^n-1,2^n-1)})$, there is at most one element $a \in \Delta^\mathcal{I}$ such that d(a)=0. Hence, there is exactly one element a such that $\textit{pos}\xspace(a) = (2^n-1, 2^n-1)$. Now assume there are elements $a,b \in \Delta^\mathcal{I}$ such that $\textit{pos}\xspace(a) = \textit{pos}\xspace(b)$ and d(a) = d(b) > 0. Then either $\textit{xpos}(a) < 2^n-1$ or $\textit{ypos}(a) < 2^n-1$. W.l.o.g., we assume $\textit{xpos}(a) < 2^n-1$. From $\mathcal{I}\models T_n$, it follows that $a,b \in (\exists {\textit{east}}\xspace.\top)^\mathcal{I}$. Let a₁,b₁ be elements such that $(a,a_1) \in {\textit{east}}\xspace^\mathcal{I}$ and $(b,b_1) \in {\textit{east}}\xspace^\mathcal{I}$. Since d(a₁) = d(b₁) < d(a) and $\textit{pos}\xspace(a_1) = \textit{pos}\xspace(b_1)$, the induction hypothesis yields a₁ = b₁. From Lemma 3.5 it follows that

$$\begin{align*}\textit{xpos}(a_1) & \equiv \textit{xpos}(b_1) \equiv \textit{xpos... ... \\ \textit{ypos}(a_1) & = \textit{ypos}(b_1) = \textit{ypos}(a) \end{align*}$$

This also implies a=b because $a_1 \in (=1 \ {\textit{east}}\xspace^{-1}.\top)^\mathcal{I}$ and $\{(a,a_1), (b,a_1) \} \subseteq {\textit{east}}\xspace^\mathcal{I}$. Hence $\textit{pos}\xspace$ is injective. To prove that $\textit{pos}\xspace$ is also surjective we use a similar technique. This time, we use an induction on the distance from the lower left corner. For each element $(x,y) \in U(2^n,2^n)$, we define:

d'(x,y) = x+y .

We show by induction that, for each $(x,y) \in U(2^n,2^n)$, there is an element $a \in \Delta^\mathcal{I}$ such that $\textit{pos}\xspace(a) = (x,y)$. If d'(x,y) = 0, then x=y=0. Since $\mathcal{I}\models (\geqslant 1 \; C_{(0,0)})$, there is an element $a \in \Delta^\mathcal{I}$ such that $\textit{pos}\xspace(a) = (0,0)$. Now consider $(x,y) \in U(2^n,2^n)$ with d'(x,y) >0. Without loss of generality we assume x > 0 (if x = 0 then y > 0 must hold). Hence $(x-1,y) \in U(2^n,2^n)$ and d'(x-1,y) < d'(x,y). From the induction hypothesis, it follows that there is an element $a \in \Delta^\mathcal{I}$ such that $\textit{pos}\xspace(a) = (x-1,y)$. Then there must be an element a₁ such that $(a,a_1) \in {\textit{east}}\xspace^\mathcal{I}$ and Lemma 3.5 implies that $\textit{pos}\xspace(a_1) = (x,y)$. Hence $\textit{pos}\xspace$ is also surjective. Finally, $\textit{pos}\xspace$ is indeed a homomorphism as an immediate consequence of Lemma 3.5. It is interesting to note that we need inverse roles only to guarantee that pos is injective. The same can be achieved by adding the cardinality restriction $(\leqslant (2^n \cdot 2^n) \ \top)$ to T_n, from which the injectivity of pos follows from its surjectivity and simple cardinality considerations. Of course the size of this cardinality restriction would only be polynomial in n if we assume binary coding of numbers. Also note that we have made explicit use of the special expressive power of cardinality restrictions by stating that, in any model of T_n, the extension of C_{(2ⁿ-1,2ⁿ-1)} must have at most one element. This cannot be expressed with a -TBox consisting of terminological axioms.