next up previous
Next: Reducing Domino Problems to Up: Consistency of - is Previous: Domino Systems

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 \textsc{NExp\-Time}-completeness proof by reduction of bounded domino problems.

To be able to apply Corollary 3.3 to \ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}} consistency for \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}, we must characterise the torus $\mathbb{Z} _{2^n}
\times \mathbb{Z} _{2^n}$ with a \ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}} 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 Xi (resp., Yi) 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)) :=...{I}$ } \\
1, & \text{otherwise} \ .
\end{cases} \end{array}
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

\begin{displaymath}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 .

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
... D_{\textit{north}}\xspace& = & \dots
\end{array} $ } \end{center} \end{figure}

The \ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}} Tn 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(2n-1,2n-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 Xi and Yi 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}$.

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

The \ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}} Tn defines a torus of exponential size in the following sense:

Lemma 3.6
Let Tn be the \ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}} as defined in Figure 3. Let $\mathcal{I} = (\Delta^\mathcal{I},\cdot^\mathcal{I})$ be a model of Tn. Then

\begin{displaymath}(\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(2n,2n) is the torus $\mathbb{Z} _{2^n}
\times \mathbb{Z} _{2^n}$ and S1,S2 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(2n,2n). 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

\begin{displaymath}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 a1,b1 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(a1) = d(b1) < d(a) and $\textit{pos}\xspace(a_1) =
\textit{pos}\xspace(b_1)$, the induction hypothesis yields a1 = b1. 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)
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 a1 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 Tn, 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 Tn, the extension of C(2n-1,2n-1) must have at most one element. This cannot be expressed with a \ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}-TBox consisting of terminological axioms.

next up previous
Next: Reducing Domino Problems to Up: Consistency of - is Previous: Domino Systems

Stephan Tobies
May 02 2000