Subsumption of Weakly Well-Designed SPARQL Patterns is Undecidable

TL;DR

This paper proves that determining whether one weakly well-designed SPARQL pattern subsumes another is an undecidable problem, highlighting a significant computational complexity difference from well-designed patterns.

Contribution

It establishes the undecidability of subsumption for weakly well-designed SPARQL patterns, contrasting with known decidability results for well-designed patterns.

Findings

Subsumption is undecidable for weakly well-designed patterns.

Contrasts with decidability of equivalence and containment.

Highlights computational complexity challenges in SPARQL analysis.

Abstract

Weakly well-designed SPARQL patterns is a recent generalisation of well-designed patterns, which preserve good computational properties but also capture almost all patterns that appear in practice. Subsumption is one of static analysis problems for SPARQL, along with equivalence and containment. In this paper we show that subsumption is undecidable for weakly well-designed patterns, which is in stark contrast to well-designed patterns, and to equivalence and containment.

Equations

$$(\mathbf{I}\cup \mathbf{X})\times (\mathbf{I}\cup \mathbf{X})\times (\mathbf{I}\cup \mathbf{X}).$$

$$P$$

$$\begin{gathered} {\Omega }_{1}to0.0pt\text{hss}\bowtie {\Omega }_2=\{{\mu }_1\cup {\mu }_2\mid {\mu }_1\in {\Omega }_1,{\mu }_2\in {\Omega }_2,\text{ and }{\mu }_1\sim {\mu }_2\}\cup \\ \{{\mu }_1\mid {\mu }_1\in {\Omega }_1,{\mu }_1\nsim {\mu }_2\text{ for all }{\mu }_2\in {\Omega }_2\}. \end{gathered}$$

$$\Phi =\{(P_{\mathbb{T}},P_{\mathbb{T}}^{\prime })\mid P_{\mathbb{T}}/⊑P_{\mathbb{T}}^{\prime }\}$$

$$\begin{array}[]{llllll}&&\{&(c_{11},\mathit{hType},\mathit{inInitRow}),(c_{11},\mathit{cType},\mathit{Cell}),\\ &&&(c_{11},\mathit{hNext},c_{12}),(c_{11},\mathit{vNext},c_{21}),(c_{12},\mathit{vNext},c_{22}),\\ &&&(?\mathit{b},\mathit{bType},\mathit{Base_{\sqsubseteq}})~{}~{}~{}\};\end{array}$$

$$\begin{array}[]{lllllllll}\lx@intercol(\cdots((\cdots((\cdots(B_{\text{root}}\mathbin{\mathsf{OPT}}{}\hfil\lx@intercol\\ &\qquad B^{1}_{\text{h-incompat}})&\mathbin{\mathsf{OPT}}&\cdots&\mathbin{\mathsf{OPT}}&B^{\ell}_{\text{h-incompat}})&\mathbin{\mathsf{OPT}}\\ &\qquad~{}B^{1}_{\text{v-incompat}})&~{}\mathbin{\mathsf{OPT}}&~{}\cdots&~{}\mathbin{\mathsf{OPT}}&~{}B^{m}_{\text{v-incompat}})&~{}\mathbin{\mathsf{OPT}}\\ &\qquad~{}~{}B^{1}_{\text{tiling}})&~{}~{}\mathbin{\mathsf{OPT}}&~{}~{}\cdots&~{}~{}\mathbin{\mathsf{OPT}}&~{}~{}B^{n}_{\text{tiling}})&~{}~{}\mathbin{\mathsf{OPT}}\\ &\qquad~{}~{}~{}B_{\text{base}},\end{array}$$

$$\begin{array}[]{rlll}B_{\text{root}}&=&\{\,(?\mathit{r},\mathit{hType},\mathit{inInitRow}),\\ &&~{}~{}(?\mathit{c},\mathit{cType},\mathit{Cell}),\\ &&~{}~{}(?\mathit{s}_{1},\mathit{hNext},?\mathit{s}_{2}),(?\mathit{s}_{1},\mathit{vNext},?\mathit{s}_{3}),(?\mathit{s}_{2},\mathit{vNext},?\mathit{s}_{4})\,\},\\ \\ B^{i}_{\text{h-incompat}}&=&\{\,(?\mathit{b},\mathit{bType},\mathit{Base_{\sqsubseteq}}),\\ &&~{}~{}(?\mathit{tile}_{1},\mathit{hNext},?\mathit{tile}_{2}),(?\mathit{tile}_{1},tType,t_{1}^{i}),(?\mathit{tile}_{2},tType,t_{2}^{i})\,\},\\ &&~{}\qquad\qquad\text{ for each }i=1,\ldots,\ell,\\ &&~{}\qquad\qquad\text{ where }(t_{1}^{i},t_{2}^{i})\text{ is the }i\text{'th pair in }(T\times T)\setminus\mathcal{H},\\ \\ B^{j}_{\text{v-incompat}}&=&\{\,(?\mathit{b},\mathit{bType},\mathit{Base_{\sqsubseteq}}),\\ &&~{}~{}(?\mathit{tile}_{1},\mathit{vNext},?\mathit{tile}_{2}),(?\mathit{tile}_{1},tType,t_{1}^{j}),(?\mathit{tile}_{2},tType,t_{2}^{j})\,\},\\ &&~{}\qquad\qquad\text{ for each }j=1,\ldots,m,\\ &&~{}\qquad\qquad\text{ where }(t_{1}^{j},t_{2}^{j})\text{ is the }j\text{'th pair in }(T\times T)\setminus\mathcal{V},\\ \\ B^{k}_{\text{tiling}}&=&\{\,(?\mathit{b},\mathit{bType},\mathit{Base_{\not\sqsubseteq}}),\\ &&~{}~{}(?\mathit{r},\mathit{cType},\mathit{Cell}),(?\mathit{r},\mathit{hNext},?\mathit{r}^{\prime}),(?\mathit{r}^{\prime},\mathit{hType},\mathit{inInitRow}),\\ &&~{}~{}(?\mathit{c},tType,t_{k}),(?\mathit{c},\mathit{vNext},?\mathit{c}^{\prime}),(?\mathit{c}^{\prime},\mathit{cType},\mathit{Cell}),\\ &&~{}~{}(?\mathit{s}_{3},\mathit{hNext},?\mathit{s}_{4})\,\},\\ &&~{}\qquad\qquad\text{ for each }k=1,\ldots,n,\\ \\ B_{\text{base}}&=&\{\,(?\mathit{b},\mathit{bType},\mathit{Base_{\sqsubseteq}})\,\}.\end{array}$$

$$(b_{⊑},tType,Bas{e}_{⊑}),(b_{/⊑},tType,Bas{e}_{/⊑}),$$

$$\begin{array}[]{ll}(c_{1j},\mathit{hType},\mathit{inInitRow}),&\text{ for each }j=1,\ldots,q,\\ (c_{ij},\mathit{cType},\mathit{Cell}),&\text{ for each }i=1,\ldots,p\text{ and }j=1,\ldots,q,\\ (c_{ij},tType,\tau(i,j)),&\text{ for each }i=1,\ldots,p\text{ and }j=1,\ldots,q,\\ (c_{ij},\mathit{hNext},c_{i(j+1)}),&\text{ for each }i=1,\ldots,p\text{ and }j=1,\ldots,q-1,\\ (c_{iq},\mathit{hNext},c_{i1}),&\text{ for each }i=1,\ldots,p,\\ (c_{ij},\mathit{vNext},c_{(i+1)j}),&\text{ for each }i=1,\ldots,p-1\text{ and }j=1,\ldots,q,\\ (c_{pj},\mathit{vNext},c_{1j}),&\text{ for each }j=1,\ldots,q.\end{array}$$

$$\begin{array}[]{llllll}(c_{11},\mathit{hType},\mathit{inInitRow}),(c_{11},\mathit{cType},\mathit{Cell}),\\ (c_{11},\mathit{hNext},c_{12}),(c_{11},\mathit{vNext},c_{21}),(c_{12},\mathit{vNext},c_{22}),\\ (\mathit{b_{\sqsubseteq}},\mathit{bType},\mathit{Base_{\sqsubseteq}})\end{array}$$

$$(c_{11},cType,Cell),(c_{11},hNext,c_{12}^{\prime }),(c_{12}^{\prime },hType,inInitRow)$$

$$(c_{12},cType,Cell),(c_{12},hNext,c_{13}),(c_{13},hType,inInitRow)$$

$$(c_{1j},cType,Cell),(c_{1(j+1)},hNext,c_{1(j+1)})$$

$$(c_{1j},tType,t_k),(c_{1j},vNext,c_{2j}),(c_{2j},cType,Cell)$$

$$(c_{2j},tType,t_k),(c_{2j},vNext,c_{3j}),(c_{3j},cType,Cell)$$

$$(c_{ij},tType,t_{ij}),(c_{ij},vNext,c_{(i+1)j}),(c_{(i+1)j},cType,Cell)$$

Full text

Subsumption of Weakly Well-Designed SPARQL Patterns is Undecidable

Mark Kaminski

Department of Computer Science,

University of Oxford,

Oxford, UK

mark.kaminski@cs.ox.ac.uk

  

Egor V. Kostylev

Department of Computer Science,

University of Oxford,

Oxford, UK

egor.kostylev@cs.ox.ac.uk

The Resource Description Framework (RDF) [1, 4] is the W3C standard for representing linked data on the Web. SPARQL [11, 3] is the default query language for RDF graphs.

A distinctive feature of SPARQL is the $\mathsf{OPTIONAL}$ operator (abbreviated as $\mathbin{\mathsf{OPT}}$ in this paper), which was introduced to “not reject (solutions) because some part of the query pattern does not match” [11]. The $\mathbin{\mathsf{OPT}}$ operator accounts in a natural way for the open world assumption and the fundamental incompleteness of the Web. However, evaluating queries that use $\mathbin{\mathsf{OPT}}$ is computationally expensive: the corresponding decision problem is PSpace-complete [8, 12], even if only projection-free queries (i.e., patterns) are considered.

Pérez et al. [8] introduced the well-designed fragment of SPARQL queries by imposing a syntactic restriction on the use of variables in $\mathbin{\mathsf{OPT}}$-expressions. On the one hand, well-designed patterns have lower complexity of query evaluation—the problem is coNP-complete. On the other hand, such queries have a more intuitive behaviour than arbitrary SPARQL queries and enjoy specific monotonicity properties. However, by far not all SPARQL queries are well-designed [9]. Weakly well-designed SPARQL fragment has been recently introduced to overcome this shortcoming: it possesses the same complexity of evaluation, but also includes almost all queries that appear in practice [5, 6].

Besides evaluation, every query language has associated static analysis problems, such as query equivalence and containment. For SPARQL there is also a specific static analysis problem, namely, query subsumption [7]. It is known that equivalence and containment are both NP-complete for well-designed patterns, while subsumption is $\Pi_{2}^{p}$-complete for such queries [7, 10]. Moreover, all three problems are undecidable for well-designed queries with projection [7, 10]. From the results of Zhang et al. [13] it follows that all these problems are undecidable for arbitrary patterns. Finally, equivalence and containment for weakly well-designed patterns are both $\Pi_{2}^{p}$-complete [5, 6]. It is also claimed that subsumption is also $\Pi_{2}^{p}$-complete for such patterns [5]. In this paper, however, we show that this problem is much more difficult; in fact, it is undecidable.

1 SPARQL Patterns

We adopt the formalisation of SPARQL that mostly follows [8]. However, we concentrate on patterns constructed using only basic graph patterns and optional matching.

RDF Graphs   An RDF graph is a labelled graph where nodes can also serve as edge labels. Formally, let $\mathbf{I}$ be a set of IRIs. Then an RDF triple is a tuple $(s,p,o)$ from $\mathbf{I}\times\mathbf{I}\times\mathbf{I}$, where $s$ is called subject, $p$ predicate, and $o$ object. An RDF graph is a finite set of RDF triples.

SPARQL Syntax   Let $\mathbf{X}$ be an infinite set $\{?x,?y,\ldots\}$ of variables, disjoint from $\mathbf{I}$. A basic (graph) pattern is a possibly empty set of triples from

[TABLE]

An (optional SPARQL graph) patterns $P$ are defined by the following grammar, where $B$ ranges over basic patterns:

[TABLE]

We denote $\mathsf{vars}(P)$ the set of all variables that appear in a pattern $P$.

Note that a given pattern can occur more than once within a larger pattern. In what follows we will need to distinguish between a (sub-)pattern $P$ as a possibly repeated building block of another pattern $P^{\prime}$ and its occurrences in $P^{\prime}$—that is, unique subtrees in the parse tree. Then, the left (right) argument of an occurrence $i$ is the subtree rooted in the left (right) child of the root of $i$ in the parse tree, and an occurrence $i$ is inside an occurrence $j$ if the root of $i$ is a descendant of the root of $j$.

A pattern $P$ is well-designed (Pérez et al. [8]) if for every occurrence $i$ of an $\mathbin{\mathsf{OPT}}$-pattern $P_{1}\mathbin{\mathsf{OPT}}P_{2}$ in $P$ the variables from $\mathsf{vars}(P_{2})\setminus\mathsf{vars}(P_{1})$ occur in $P$ only inside $i$.

Given a pattern $P$, an occurrence $i_{1}$ in $P$ dominates an occurrence $i_{2}$ if there exists an occurrence $j$ of an $\mathbin{\mathsf{OPT}}$-pattern such that $i_{1}$ is inside the left argument of $j$ and $i_{2}$ is inside the right argument. A pattern $P$ is weakly well-designed ([5, 6]) if, for each occurrence $i$ of an $\mathbin{\mathsf{OPT}}$-subpattern $P_{1}\mathbin{\mathsf{OPT}}P_{2}$, the variables in $\mathsf{vars}(P_{2})\setminus\mathsf{vars}(P_{1})$ appear outside $i$ only in subpatterns whose occurrences are dominated by $i$.

SPARQL Semantics   The semantics of graph patterns is defined in terms of mappings—that is, partial functions from variables to IRIs. The domain $\mathsf{dom}(\mu)$ of a mapping $\mu$ is the set of variables on which $\mu$ is defined. Two mappings $\mu_{1}$ and $\mu_{2}$ are compatible, written $\mu_{1}\sim\mu_{2}$, if $\mu_{1}(?x)=\mu_{2}(?x)$ for all variables $?x\in\mathsf{dom}(\mu_{1})\cap\mathsf{dom}(\mu_{2})$. Mapping $\mu_{1}$ is subsumed by mapping $\mu_{2}$, written $\mu_{1}\sqsubseteq\mu_{2}$, if $\mu_{1}\sim\mu_{2}$ and $\mathsf{dom}(\mu)_{1}\subseteq\mathsf{dom}(\mu_{2})$. If $\mu_{1}\sim\mu_{2}$, then $\mu_{1}\cup\mu_{2}$ constitutes a mapping with domain $\mathsf{dom}(\mu_{1})\cup\mathsf{dom}(\mu_{2})$ that coincides with $\mu_{1}$ on $\mathsf{dom}(\mu_{1})$ and with $\mu_{2}$ on $\mathsf{dom}(\mu_{2})$.

Given two sets of mappings $\Omega_{1}$ and $\Omega_{2}$, we define their left outer join operation as follows:

[TABLE]

Given a graph $G$, the evaluation $\llbracket P\rrbracket_{G}$ of a pattern $P$ over $G$ is defined as follows:

if $B$ is a basic pattern, then $\llbracket B\rrbracket_{G}=\{\mu:\mathsf{vars}(B)\rightarrow\mathbf{I}\mid\mu(B)\subseteq G\};$ 2. 2.

$\llbracket(P_{1}\mathbin{\mathsf{OPT}}P_{2})\rrbracket_{G}=\llbracket P_{1}\rrbracket_{G}\mathbin{\mathbin{\rule[0.3014pt]{3.00003pt}{0.4pt}\hbox to0.0pt{\hss\rule[5.94167pt]{3.00003pt}{0.4pt}}\mkern-6.5mu\Join}}\llbracket P_{2}\rrbracket_{G}$.

A pattern $P$ is contained in a pattern $P^{\prime}$ if $\llbracket P\rrbracket_{G}\subseteq\llbracket P^{\prime}\rrbracket_{G}$ for every graph $G$. Patterns $P$ and $P^{\prime}$ are equivalent if they contain each other. Pattern $P$ is subsumed by $P^{\prime}$, written $P\sqsubseteq P^{\prime}$, if, for every graph $G$, each $\mu\in\llbracket P\rrbracket_{G}$ has $\mu^{\prime}\in\llbracket P^{\prime}\rrbracket_{G}$ such that $\mu\sqsubseteq\mu^{\prime}$ (Letelier et al. [7]).

2 Pattern Subsumption

Theorem 1

The problem of checking whether $P\sqsubseteq P^{\prime}$ for weakly well-designed patterns $P$ and $P^{\prime}$ is undecidable.

Proof.  We prove undecidability by a reduction of a variant of the tiling problem, which is known to be undecidable (see e.g., [2]). We start by introducing the notation used throughout the proof.

A tiling instance $\mathbb{T}$ consists of a collection $T=\{t_{1},\ldots,t_{n}\}$ of tile types and edge compatibility relations $\mathcal{H}$ and $\mathcal{V}$ on $T$. Intuitively, $\mathcal{H}(t,t^{\prime})$ means that a tile of type $t^{\prime}$ can be placed to the right of a tile of type $t$ in a row, while $\mathcal{V}(t,t^{\prime})$ means that $t^{\prime}$ can be placed above $t$ in a column.

A tiling of the positive plane with $\mathbb{T}$ is a function $\tau:\mathbb{N}\times\mathbb{N}\rightarrow T$, for the set of natural numbers $\mathbb{N}$, such that, for all $i,j\in\mathbb{N}$,

• –

$\mathcal{H}(\tau(i,j),\tau(i+1,j))$, and

• –

$\mathcal{V}(\tau(i,j),\tau(i,j+1))$.

Tiling $\tau$ is periodic if there exist positive numbers $p$ and $q$, called horizontal and vertical periods, respectively, such that $\tau(i,j)=\tau(p+i,j)=\tau(i,q+j)$ for all $i,j\in\mathbb{N}$. A periodic tiling can be seen as a tiling of a torus, since column $p+1$ and row $q+1$ can be “glued” with the left-most column and bottom row, respectively.

Let $S_{\textrm{tiling}}$ denote the set of all tiling instances that allow for tilings of the positive plane, and $S_{\textrm{period}}$ the set of all tiling instances that allow for periodic tilings. To prove undecidability we will use the following fact.

Fact 1** (Gurevich and Koryakov [2])**

Sets $S_{\textrm{\em tiling}}$ and $S_{\textrm{\em period}}$ are recursively inseparable—that is, there is no recursive set $S$ with ${S_{\textrm{\em period}}\subseteq S\subseteq S_{\textrm{\em tiling}}}$.

In what follows we first construct, for each tiling instance $\mathbb{T}$, weakly well-designed patterns $P_{\mathbb{T}}$ and $P^{\prime}_{\mathbb{T}}$, and then show that the set

[TABLE]

contains $\{(P_{\mathbb{T}},P^{\prime}_{\mathbb{T}})\mid\mathbb{T}\in S_{\textrm{period}}\}$, and is contained in ${\{(P_{\mathbb{T}},P^{\prime}_{\mathbb{T}})\mid\mathbb{T}\in S_{\textrm{tiling}}\}}$. This will imply, by Fact 1, that $\Phi$ (and, hence, the complement of $\Phi$) cannot be recursive.

Let $\mathbb{T}$ be a tiling instance with tile types $T=\{t_{1},\ldots,t_{n}\}$, and compatibility relations $\mathcal{H}$ and $\mathcal{V}$. Let $P_{\mathbb{T}}$ be

[TABLE]

so, $P_{\mathbb{T}}$ is a basic pattern with 6 triples, only one of which mentions a variable, $?\mathit{b}$. The other pattern has a more complex structure: let $P^{\prime}_{\mathbb{T}}$ be

[TABLE]

where $\ell=|(T\times T)\setminus\mathcal{H}|$, $m=|(T\times T)\setminus\mathcal{V}|$,

[TABLE]

Having the construction complete, next we show that $P_{\mathbb{T}}\not\sqsubseteq P^{\prime}_{\mathbb{T}}$ for any tiling instance $\mathbb{T}$ in $S_{\textrm{period}}$. In particular, on the base of a witnessing periodic tiling we build a graph $G$ and a mapping $\mu$ such that $\mu\in\llbracket P_{\mathbb{T}}\rrbracket_{G}$, but there is no $\mu^{\prime}\in\llbracket P^{\prime}_{\mathbb{T}}\rrbracket_{G}$ such that $\mu\sqsubseteq\mu^{\prime}$. Assume that $\mathbb{T}$ has tile types $T=\{t_{1},\ldots,t_{n}\}$, compatibility relations $\mathcal{H}$ and $\mathcal{V}$, and periodic tiling $\tau$ with the horizontal and vertical periods $p\geq 2$ and $q\geq 2$, respectively. Let $G$ consist of the triples

[TABLE]

as well as the triples

[TABLE]

Let also $\mu=\{?\mathit{b}\mapsto\mathit{b_{\sqsubseteq}}\}$.

It is immediate to see that $\mu\in\llbracket P_{\mathbb{T}}\rrbracket_{G}$. Moreover, assuming that $P_{\mathbb{T}}$ has form (1), $\llbracket B_{\text{root}}\rrbracket_{G}$ consists of $q\cdot(p\cdot q)\cdot(p\cdot q)$ mappings sending $?\mathit{r}$ to one of $c_{1j}$, $?\mathit{c}$ to one of $c_{ij}$, $?\mathit{s}_{1}$ also to one of $c_{ij}$, while $?\mathit{s}_{2}$, $?\mathit{s}_{3}$ and $?\mathit{s}_{4}$ to the IRIs accordingly connected to the value of $?\mathit{c}$ (note that the values of $?\mathit{r}$, $?\mathit{c}$, and $?\mathit{s}_{1}$ do not depend on each other).

Since the tiling agrees with $\mathcal{H}$ and $\mathcal{V}$, none of basic patterns $B^{i}_{\text{h-incompat}}$ and $B^{j}_{\text{v-incompat}}$ has a match in $G$, because each of them requires a pair of horizontally or vertically adjacent cells with incompatible tile types. So, none of the mappings in $\llbracket B_{\text{root}}\rrbracket_{G}$ are extendable to any of $B^{i}_{\text{h-incompat}}$ and $B^{j}_{\text{v-incompat}}$. However, each mapping $\mu^{\prime}_{\text{root}}\in\llbracket B_{\text{root}}\rrbracket_{G}$ extends to $B^{k}_{\text{tiling}}$ such that $t_{k}=\tau(i,j)$ with $\mu^{\prime}_{\text{root}}(?\mathit{c})=c_{ij}$. In particular, this extension $\mu^{\prime}$ sends $?\mathit{b}$ to $\mathit{b_{\not\sqsubseteq}}$, which implies that $\mu\not\sqsubseteq\mu^{\prime}$. Therefore, $G$ and $\mu$ are a witness for the required $P_{\mathbb{T}}\not\sqsubseteq P^{\prime}_{\mathbb{T}}$.

We continue by showing that $P_{\mathbb{T}}\not\sqsubseteq P^{\prime}_{\mathbb{T}}$ implies $\mathbb{T}\in S_{\textrm{tiling}}$ for any tiling instance $\mathbb{T}$. In particular, on the base of a graph $G$ and mapping $\mu$ witnessing $P_{\mathbb{T}}\not\sqsubseteq P^{\prime}_{\mathbb{T}}$ we construct a tiling $\tau$ of the positive plane with $\mathbb{T}$. Assume that $\mathbb{T}$ has tile types $T=\{t_{1},\ldots,t_{n}\}$ as well as compatibility relations $\mathcal{H}$ and $\mathcal{V}$. Since $\mu\in\llbracket P_{\mathbb{T}}\rrbracket_{G}$, graph $G$ contains triples

[TABLE]

for the IRI $\mathit{b_{\sqsubseteq}}$ such that $\mu=\{?\mathit{b}\mapsto\mathit{b_{\sqsubseteq}}\}$. Therefore, assuming that $P^{\prime}_{\mathbb{T}}$ has form (1), $\llbracket B_{\text{root}}\rrbracket_{G}$ contains a mapping $\mu^{\prime}_{\text{root}}$ sending $?\mathit{r}$ to $c_{11}$. Mapping $\mu^{\prime}_{\text{root}}$ is extendable to $B^{k}_{\text{tiling}}$ for some $k$; indeed, if it is not the case, then $\llbracket P^{\prime}_{\mathbb{T}}\rrbracket_{G}$ contains an extension $\mu^{\prime}$ of $\mu^{\prime}_{\text{root}}$ sending $?\mathit{b}$ to $\mathit{b_{\sqsubseteq}}$, because all $B^{i}_{\text{h-incompat}}$, $B^{j}_{\text{v-incompat}}$, and $B_{\text{base}}$ contain $(?\mathit{b},tType,\mathit{Base_{\sqsubseteq}})$, while $B_{\text{base}}$ matches $G$, which implies $\mu\sqsubseteq\mu^{\prime}$ contradicting the fact that $G$ and $\mu$ are a witness for non-subsumption. Therefore, triples $(?\mathit{r},\mathit{cType},\mathit{Cell}),(?\mathit{r},\mathit{hNext},?\mathit{r}^{\prime}),(?\mathit{r}^{\prime},\mathit{hType},\mathit{inInitRow})$ are matched in $G$ extending $\mu^{\prime}_{\text{root}}$, that is, $G$ contains triples

[TABLE]

for some IRI $c^{\prime}_{12}$. Just for uniformity, assume that $c^{\prime}_{12}=c_{12}$. Therefore, $\llbracket B_{\text{root}}\rrbracket_{G}$ contains a mapping $\mu^{\prime\prime}_{\text{root}}$ sending $?\mathit{r}$ to $c_{12}$ (and all other variables same as $\mu^{\prime}_{\text{root}}$). Reasoning in the same way as for $\mu^{\prime}_{\text{root}}$, we obtain that $G$ has triples

[TABLE]

for some IRI $c_{13}$. Continuing like this, we conclude that $G$ contains

[TABLE]

for all $j\geq 1$ (note that many of these $c_{1j}$ coincide, because $G$ is finite).

For each $j\geq 1$, $\llbracket B_{\text{root}}\rrbracket_{G}$ contains a mapping sending $?\mathit{c}$ to $c_{1j}$. As before, this mapping is extendable in $G$ to $B^{k}_{\text{tiling}}$ for some $k$. In particular, it is extendable to the triples $(?\mathit{c},tType,t_{k})$, $(?\mathit{c},\mathit{vNext},?\mathit{c}^{\prime})$, and $(?\mathit{c}^{\prime},\mathit{cType},\mathit{Cell})$—that is, $G$ contains triples

[TABLE]

for some IRI $c_{2j}$ (again, if $j$ is 1 or 2, then we assume that $c_{2j}$ is the same as in $P_{\mathbb{T}}$ for uniformity). Similarly as before, $\llbracket B_{\text{root}}\rrbracket_{G}$ contains a mapping sending $?\mathit{c}$ to $c_{2j}$, from which we have that $G$ has triples

[TABLE]

for some $c_{3j}$ and $k$. Repeating this process, we conclude that $G$ contains, for any $i\geq 1$ and $j\geq 1$,

[TABLE]

for some $c_{ij}$ and $t_{ij}$. Set $\tau(i,j)=t_{ij}$ for each $i$ and $j$.

We need to show that $\tau$ is indeed a tiling with $\mathbb{T}$. To this end, we first note that $G$ contains the triple $(c_{ij},\mathit{hNext},c_{i(j+1)})$ for all $i$ and $j$: we already showed this fact for $i=1$, and for all other $i$ it can be proved very similarly to the reasoning above, based on the fact that $\llbracket B_{\text{root}}\rrbracket_{G}$ contains a mapping sending $?\mathit{s}_{1}$, $?\mathit{s}_{2}$, $?\mathit{s}_{3}$, and $?\mathit{s}_{4}$ to $c_{(i-1)j}$, $c_{(i-1)(j+1)}$, $c_{ij}$, and $c_{i(j+1)}$, respectively. Now, to see that $\tau$ is a tiling with $\mathbb{T}$ we just note that if there exist horizontally or vertically adjacent tiles that do not agree with $\mathcal{H}$ or $\mathcal{V}$, then there exists $i$ or $j$ such that $B^{i}_{\text{h-incompat}}$ or $B^{j}_{\text{v-incompat}}$ is matched in $G$; since this basic patterns does not have any variables in common with $B_{\text{root}}$, any mapping in $\llbracket B_{\text{root}}\rrbracket_{G}$ is then extendable to this BGP and hence $\llbracket P^{\prime}_{\mathbb{T}}\rrbracket_{G}$ contains a mapping sending $?\mathit{b}$ to $\mathit{b_{\sqsubseteq}}$, contradicting the fact that graph $G$ and mapping $\mu$ are a witness for non-subsumption. $\Box$