[a] [a,b] [b]

# Expressiveness of SHACL Features and Extensions for Full Equality and
Disjointness Tests

Bart Bogaerts0000-0003-3460-4251  ,  Maxime Jakubowski0000-0002-7420-1337  and
Jan Van den Bussche0000-0003-0072-3252  Vrije Universiteit Brussel, Belgium
<EMAIL_ADDRESS>Universiteit Hasselt, Belgium
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

SHACL is a W3C-proposed schema language for expressing structural constraints
on RDF graphs. Recent work on formalizing this language has revealed a
striking relationship to description logics. SHACL expressions can use three
fundamental features that are not so common in description logics. These
features are equality tests; disjointness tests; and closure constraints.
Moreover, SHACL is peculiar in allowing only a restricted form of expressions
(so-called targets) on the left-hand side of inclusion constraints.

The goal of this paper is to obtain a clear picture of the impact and
expressiveness of these features and restrictions. We show that each of the
four features is primitive: using the feature, one can express boolean queries
that are not expressible without using the feature. We also show that the
restriction that SHACL imposes on allowed targets is inessential, as long as
closure constraints are not used.

In addition, we show that enriching SHACL with “full” versions of equality
tests, or disjointness tests, results in a strictly more powerful language.

###### Key words and phrases:

Expressive power, schema languages

This paper is an extended version of our work presented at ICDT 2022
[BJVdB22].

##  1\. Introduction

On the Web, the Resource Description Framework (RDF [RDF14]) is a standard
format for representing knowledge and publishing data. RDF represents
information in the form of directed graphs, where labeled edges indicate
properties of nodes. To facilitate more effective access and exchange, it is
important for a consumer of an RDF graph to know what properties to expect,
or, more generally, to be able to rely on certain structural constraints that
the graph is guaranteed to satisfy. We therefore need a declarative language
in which such constraints can be expressed formally. In database terms, we
need a schema language.

Two prominent proposals in this vein have been ShEx [BGP17] and SHACL [SHA17].
Both approaches use formulas that express the presence or absence of certain
properties of a node or its neighbors in the graph. Such formulas are called
“shapes.” When we evaluate a shape on a node, that node is called the “focus
node.” Some examples of shapes, expressed for now in English, could be the
following:111In real RDF, names of properties and nodes must conform to IRI
syntax, but in this paper, to avoid clutter, we take the liberty to use simple
names.

  1. (1)

“The focus node has a phone property, but no email.”

  2. (2)

“The focus node has at least five incoming managed-by edges.”

  3. (3)

“Through a path of friend edges, the focus node can reach a node with a CEO-of
edge to the node Apple.”

  4. (4)

“The focus node has at least one colleague who is also a friend.”

  5. (5)

“The focus node has no other properties than name, address, or birthdate.”

In this paper, we look deeper into SHACL, the language recommended by the
World Wide Web Consortium. We do not use the actual SHACL syntax, but work
with the elegant formalization proposed by Corman, Reutter and Savkovic
[CRS18], and used in subsequent works by several authors [ACO+20, LS+20,
PK+20]. That formalization reveals a striking similarity between shapes on the
one hand, and concepts, familiar from description logics [BHLS17], on the
other hand. The similarity between SHACL and description logics runs even
deeper when we account for targeting, which is the actual mechanism to express
constraints on an RDF graph using shapes.

Specifically, a non-recursive _shape schema 222Real SHACL uses the term
_shapes graph_ instead of shape schema._ is essentially a finite list of
shapes, where each shape $\phi$ is additionally associated with a target query
$q$. An RDF graph $G$ is said to conform to such a schema if for every
target–shape combination $(q,\phi)$, and every node $v$ returned by $q$ on
$G$, we have that $v$ satisfies $\phi$ in $G$. Let us see some examples of
target–shape pairs, still expressed in English:

  1. (6)

“Every node of type Person has an email or phone property.” Here, the target
query returns all nodes with an edge labeled type to node Person; the shape
checks that the focus node has an email or phone property.

  2. (7)

“Different nodes never have the same email.” Here the target query returns all
nodes with an incoming email edge, and the shape checks that the focus node
does not have two or more incoming email edges.

  3. (8)

“Every mathematician has a finite Erdős number.” Here the target query returns
all nodes of type Mathematician, and the shape checks that the focus node can
reach the node Erdős by a path that matches the regular expression
$(\textsf{author}^{-}/\textsf{author})^{*}$. Here, the minus superscript
denotes an inverse edge.

Interestingly, and apparent in the examples 6–8, the target queries considered
for this purpose in SHACL, as well as in ShEx, actually correspond to simple
cases of shapes. It is then only a small step to consider _generalized_ shape
schemas as finite sets of inclusion statements of the form
$\phi_{1}\subseteq\phi_{2}$, where $\phi_{1}$ and $\phi_{2}$ are shapes.
Since, as noted above, shapes correspond to concepts, we thus see that shape
schemas correspond to TBoxes in description logics.

We stress that the task we are focusing on in this paper is checking
conformance of RDF graphs against shape schemas. Every shape schema
$\mathcal{S}$ defines a decision problem: given an RDF graph $G$, check
whether $G$ conforms to $\mathcal{S}$. In database terms, we are processing a
_boolean query_ on a graph database. In description logic terms, this amounts
to _model checking_ of a TBox: given an interpretation, check whether it
satisfies the TBox. Thus our focus is a bit different from that of typical
applications of description logics. There, facts are declared in ABoxes, which
should not be confused with interpretations. The focus is then on higher
reasoning tasks, such as checking satisfiability of an ABox and a TBox, or
deciding logical entailment.

Given the above context, let us now look in more detail at the logical
constructs that can be used to build shapes. Some of these constructs are well
known concept constructors from expressive description logics [CDGNL03]: the
boolean connectives; constants; qualified number restriction (a combination of
existential quantification and counting); and regular path expressions with
inverse. To illustrate, example shapes 1–3 are expressible as follows:

  1. (1)

$\mathop{\geq}\nolimits_{1}\textsf{phone}.\top\land\neg\mathop{\geq}\nolimits_{1}\textsf{email}.\top$.
This uses qualified number restriction with count 1 (so essentially
existential quantification), conjunction, and negation; $\top$ stands for
true.

  2. (2)

$\mathop{\geq}\nolimits_{5}\textsf{managed-by}^{-}.\top$. This uses counting
to 5, and inverse.

  3. (3)

$\mathop{\geq}\nolimits_{1}\textsf{friend}^{*}/\textsf{CEO-
of}.\\{\textsf{Apple}\\}$. This uses a regular path expression and the
constant Apple.

However, SHACL also has three specific logical features that are less common:

Equality:

The shape $\mathit{eq}(E,r)$, for a path expression $E$ and a property $r$,
tests equality of the sets of nodes reachable from the focus node by an
$r$-edge on the one hand, and by an $E$-path on the other hand.

Disjointness:

A similar shape $\mathit{disj}(E,r)$ tests disjointness of the two sets of
reachable nodes. To illustrate, example shape 4 is expressed as
$\neg\mathit{disj}(\textsf{colleague},\textsf{friend})$.

Closure constraints:

RDF graphs to be checked for conformance against some shape schema need not
obey some fixed vocabulary. Thus SHACL provides shapes of the form
$\mathit{closed}(R)$, with $R$ a finite set of properties, expressing that the
focus node has no properties other than those in $R$. This was already
illustrated as example shape 5, with
$R=\\{\textsf{name},\textsf{address},\textsf{birthdate}\\}$.

Our goal in this paper is to clarify the impact of the above four features on
the expressiveness of SHACL as a language for boolean queries on graph
databases. Thereto, we offer the following contributions.

  * •

We show that each of the three features is primitive in a strong sense.
Specifically, for each feature, we exhibit a boolean query $Q$ such that $Q$
is expressible by a single target–shape pair, using only the feature and the
basic constructs; however, $Q$ is not expressible by any generalized shape
schema when the feature is disallowed.

  * •

We also clarify the significance of the restriction that SHACL puts on allowed
targets. We observe that as long as closure constraints are not used, the
restriction is actually insignificant. Any generalized shape schema, allowing
arbitrary but closure-free shapes on the left-hand sides of the inclusion
statements, can be equivalently written as a shape schema with only targets on
the left-hand sides. However, allowing closure constraints on the left-hand
side strictly adds expressive power.

  * •

We additionally show that “full” variants of equality tests or disjointness
tests result in strictly more expressive languages. This result anticipates
planned extensions of SHACL [Knu21, Jak22].

  * •

Our results continue to hold when the definition of _recursive_ shapes is
allowed, provided that recursion through negation is stratified.

This paper is organized as follows. Section 2 presents clean formal
definitions of non-recursive shape schemas, building on and inspired by the
work of Andreşel, Corman, et al. cited above. Section 3 and Section 4 present
our results, and Section 5 extends our result for “full” equality and
disjointness tests. Section 6 presents the extension to stratified recursion.
Section 7 offers concluding remarks.

##  2\. Shape schemas

In this section we define shapes, RDF graphs, shape schemas, and the
conformance of RDF graphs to shape schemas. Perhaps curiously to those
familiar with SHACL, our treatment for now omits _shape names_. Shape names
are redundant as far as expressive power is concerned, as long as we are in a
non-recursive setting, because shape name definitions can then always be
unfolded. Indeed, for clarity of exposition, we have chosen to work first with
non-recursive shape schemas. Section 6 then presents the extension to
recursion (and introduces shape names in the process). We point out that the
W3C SHACL recommendation only considers non-recursive shape schemas.

#### Node and property names

From the outset we assume two disjoint, infinite universes $N$ and $P$ of
_node names_ and _property names_ , respectively.333In practice, node names
and property names are IRIs [RDF14], so the disjointness assumption would not
hold. However, this assumption is only made for simplicity of notation; it can
be avoided if we make our notation for vocabularies and interpretations (see
below) more complicated.

###  2.1. Shapes

We define _path expressions_ $E$ and _shapes_ $\phi$ by the following grammar:

$\displaystyle E$ $\displaystyle::=\mathit{id}\mid p\mid p^{-}\mid E\cup E\mid
E/E\mid E^{*}$ $\displaystyle\phi$
$\displaystyle::=\top\mid\\{c\\}\mid\phi\land\phi\mid\phi\lor\phi\mid\neg\phi\mid{}\mathop{\geq}\nolimits_{n}E.\phi\mid\mathit{eq}(E,p)\mid\mathit{disj}(E,p)\mid\mathit{closed}(R)$

Here, $p$ and $c$ stand for property names and node names, respectively; $n$
stands for nonzero natural numbers; and $R$ stands for finite sets of property
names. A node name $c$ is also referred to as a _constant_. In $p^{-}$, $-$
stands for inverse.

Abbreviation:

We will use $\exists E.\phi$ as an abbreviation for
$\mathop{\geq}\nolimits_{1}E.\phi$.

######  Remark 1.

Real SHACL supports some further shapes which have to do with tests on IRI
constants and literals, as well as comparisons on numerical values and
language tags. Like other work on the formal aspects of SHACL, we abstract
these away, as many questions are already interesting without these features.

######  Remark 2.

Universal quantification $\forall E.\phi$ could be introduced as an
abbreviation for $\neg\exists E.\neg\phi$. Likewise, $\leq_{n}E.\phi$ may be
used as an abbreviation for $\neg\mathop{\geq}\nolimits_{n+1}E.\phi$.

######  Remark 3.

In our formalization, a path expression can be ‘$\mathit{id}$’. We show in
Lemma 7 that every path expression is equivalent to $\mathit{id}$,
$E^{\prime}\cup\mathit{id}$ or $E^{\prime}$, where $E^{\prime}$ does not use
$\mathit{id}$. In real SHACL, it is possible to write
$E^{\prime}\cup\mathit{id}$ using “zero-or-one” path expressions. Explicitly
writing $\mathit{id}$ is not possible, but this poses no problem. Path
expressions can only appear in counting quantifiers, equality and disjointness
shapes. The shape $\mathop{\geq}\nolimits_{n}\mathit{id}.\phi$ is clearly
equivalent to $\phi$ if $n=1$, otherwise, it is equivalent to $\neg\top$. The
shapes $\mathit{eq}(E,p)$ or $\mathit{disj}(E,p)$ where $E$ is $\mathit{id}$
are implicitly expressible in SHACL by writing the equality or disjointness
constraint in node shapes, rather than property shapes.

A _vocabulary_ $\Sigma$ is a subset of $N\cup P$. A path expression is said to
be _over_ $\Sigma$ if it only uses property names from $\Sigma$. Likewise, a
shape is over $\Sigma$ if it only uses constants from $\Sigma$ and path
expressions over $\Sigma$.

Following common practice in logic, shapes are evaluated in _interpretations_.
We recall the familiar definition of an interpretation. Let $\Sigma$ be a
vocabulary. An interpretation $I$ over $\Sigma$ consists of

  * •

a set $\Delta^{I}$, called the _domain_ of $I$;

  * •

for each constant $c\in\Sigma$, an element $\llbracket
c\rrbracket^{I}\in\Delta^{I}$; and

  * •

for each property name $p\in\Sigma$, a binary relation $\llbracket
p\rrbracket^{I}$ on $\Delta^{I}$.

The semantics of shapes is now defined as follows.

  * •

On any interpretation $I$ as above, every path expression $E$ over $\Sigma$
evaluates to a binary relation $\llbracket E\rrbracket^{I}$ on $\Delta^{I}$,
defined in Table 1.

  * •

Now for any shape $\phi$ over $\Sigma$ and any element $a\in\Delta^{I}$, we
define when _$a$ conforms to $\phi$ in $I$_, denoted by $I,a\vDash\phi$. For
the boolean operators $\top$ (true), $\land$ (conjunction), $\lor$
(disjunction), $\neg$ (negation), the definition is obvious. For the other
constructs, the definition is given in Table 2, taking note of the following:

    * –

We use the notation $R(x)$, for a binary relation $R$, to denote the set
$\\{y\mid(x,y)\in R\\}$. We apply this notation to the case where $R$ is of
the form $\llbracket E\rrbracket^{I}$.

    * –

We also use the notation $\sharp X$ for the cardinality of a set $X$.

  * •

For a shape $\phi$ and interpretation $I$, the notation

$\llbracket\phi\rrbracket^{I}:=\\{a\in\Delta^{I}\mid I,a\vDash\phi\\}$

will be convenient.

Table 1. Semantics of path expressions. $E$ | $\llbracket E\rrbracket^{I}$
---|---
$\mathit{id}$ | $\\{(x,x)\mid x\in\Delta^{I}\\}$
$p^{-}$ | $\\{(a,b)\mid(b,a)\in\llbracket p\rrbracket^{I}\\}$
${E_{1}\cup E_{2}}$ | $\llbracket E_{1}\rrbracket^{I}\cup\llbracket E_{2}\rrbracket^{I}$
${E_{1}/E_{2}}$ | $\\{(a,b)\mid\exists x:(a,x)\in\llbracket E_{1}\rrbracket^{I}\land(x,b)\in\llbracket E_{2}\rrbracket^{I}\\}$
${E^{*}}$ | the reflexive-transitive closure of $\llbracket E\rrbracket^{I}$
Table 2. Conditions for conformance of a node to a shape. $\phi$ |  $I,a\vDash\phi$ if:
---|---
$\\{c\\}$ | $a=\llbracket c\rrbracket^{I}$
$\mathop{\geq}\nolimits_{n}E.\psi$ | $\sharp\\{b\in\llbracket E\rrbracket^{I}(a)\mid I,b\vDash\psi\\}\geq n$
$\mathit{eq}(E,p)$ | the sets $\llbracket E\rrbracket^{I}(a)$ and $\llbracket p\rrbracket^{I}(a)$ are equal
$\mathit{disj}(E,p)$ | the sets $\llbracket E\rrbracket^{I}(a)$ and $\llbracket p\rrbracket^{I}(a)$ are disjoint
$\mathit{closed}(R)$ |  $\llbracket p\rrbracket^{I}(a)$ is empty for each $p\in\Sigma-R$

In the Introduction we already gave three examples (1), (2), and (3) of shapes
expressed in English and the formal syntax. The target query of example (7)
from the Introduction can be expressed as the shape
$\exists\textsf{email}^{-}.\top$. The shape of example (7) can be written as
$\leq_{1}\textsf{email}^{-}.\top$.

###  2.2. Graphs and their interpretation

Remember from Table 2 that a shape $\mathit{closed}(R)$ states that the focus
node may only have outgoing properties that are mentioned in $R$. It may
appear that such a shape is simply expressible as the conjunction of
$\neg\exists p.\top$ for $p\in\Sigma-R$. However, since shapes must be finite
formulas, this only works if $\Sigma$ is finite. In practice, shapes can be
evaluated over arbitrary RDF graphs, which can involve arbitrary property
names (and node names), not limited to a finite vocabulary that is fixed in
advance.

Formally, we define a _graph_ as a finite set of triples of the form
$(a,p,b)$, where $p$ is a property name and $a$ and $b$ are (not necessarily
distinct) node names. We refer to the node names appearing in a graph $G$
simply as the _nodes_ of $G$; the set of nodes of $G$ is denoted by $N_{G}$. A
pair $(a,b)$ with $(a,p,b)\in G$ is referred to as an _edge_ , or a _$p$
-edge_, in $G$.

We now canonically view any graph $G$ as an interpretation over the _full_
vocabulary $N\cup P$ as follows:

  * •

$\Delta^{G}$ equals $N$ (the universe of all node names).

  * •

$\llbracket c\rrbracket^{G}$ equals $c$ itself, for every node name $c$.

  * •

$\llbracket p\rrbracket^{G}$ equals the set of $p$-edges in $G$, for every
property name $p$.

Note that since graphs are finite, $\llbracket p\rrbracket^{G}$ will be empty
for all but a finite number of $p$’s.

Given this canonical interpretation, path expressions and shapes obtain a
semantics on all graphs $G$. Thus for any path expression $E$, the binary
relation $\llbracket E\rrbracket^{G}$ on $N$ is well-defined; for any shape
$\phi$ and $a\in N$, it is well-defined whether or not $G,a\vDash\phi$; and we
can also use the notation $\llbracket\phi\rrbracket^{G}$.

######  Remark 4.

Since a graph is considered to be an interpretation with the infinite domain
$N$, it may not be immediately clear that shapes can be effectively evaluated
over graphs. Adapting well-known methods, however, we can reduce to a finite
domain over a finite vocabulary [AHV95, Theorem 5.6.1], [AGSS86, HS94].
Formally, let $\phi$ be a shape and let $G$ be a graph. Recall that $N_{G}$
denotes the set of nodes of $G$; similarly, let $P_{G}$ be the set of property
names appearing in $G$. Let $C$ be the set of constants mentioned in $\phi$.
We can then form the finite vocabulary $\Sigma=N_{G}\cup C\cup P_{G}$. Now
define the interpretation $I$ over $\Sigma$ as follows:

  * •

$\Delta^{I}=N_{G}\cup C\cup\\{\star\\}$, where $\star$ is an element not in
$N$;

  * •

$\llbracket c\rrbracket^{I}=c$ for each node name $c\in\Sigma$;

  * •

$\llbracket p\rrbracket^{I}=\llbracket p\rrbracket^{G}$ for each property name
$p\in\Sigma$.

Note that no constant symbol names $\star$ in $I$. Then for every $x\in
N_{G}\cup C$, one can show that $x\in\llbracket\phi\rrbracket^{G}$ if and only
if $x\in\llbracket\phi\rrbracket^{I}$. For all other node names $x$, one can
show that $x\in\llbracket\phi\rrbracket^{G}$ if and only if
$\star\in\llbracket\phi\rrbracket^{I}$.

[Example 2.1 continued] Consider the graph $G_{\mathit{ex}}$ depicted in
Figure 1. This graph can be seen as the interpretation $I_{\mathit{ex}}$ with
an infinite domain containing the elements $a$, $b$, $m_{1}$, and $m_{2}$. It
interprets the predicate name email as $\\{(a,m_{1}),(b,m_{1}),(b,m_{2})\\}$
and all other predicate names as the empty set. If we look at the
interpretation of example (7) from the Introduction in $I_{\mathit{ex}}$, we
have
$\llbracket\leq_{1}\textsf{email}^{-}.\top\rrbracket^{I_{\mathit{ex}}}=\\{m_{1}\\}$
for the shape, and
$\llbracket\exists\textsf{email}^{-}.\top\rrbracket^{I_{\mathit{ex}}}=\\{m_{1},m_{2}\\}$
for the target.

$a$$m_{1}$$b$$m_{2}$emailemailemail Figure 1. An example graph
$G_{\mathit{ex}}$

###  2.3. Targets and shape schemas

SHACL identifies four special forms of shapes and calls them _targets_ :

Node targets:

$\\{c\\}$ for any constant $c$.

Class-based targets:

$\exists\textsf{type}/\textsf{subclass}^{*}.\\{c\\}$ for any constant $c$.
Here, type and subclass represent distinguished IRIs from the RDF Schema
vocabulary [RDF14].

Subjects-of targets:

$\exists p.\top$ for any property name $p$.

Objects-of targets:

$\exists p^{-}.\top$ for any property name $p$.

We now define a _generalized shape schema_ (or shape schema for short) as a
finite set of inclusion statements, where an inclusion statement is of the
form $\phi_{1}\subseteq\phi_{2}$, with $\phi_{1}$ and $\phi_{2}$ shapes. A
_target-based shape schema_ is a shape schema that only uses targets, as
defined above, on the left-hand sides of its inclusion statements. This
restriction corresponds to the shape schemas considered in real SHACL.

As already explained in the Introduction, a graph $G$ _conforms_ to a shape
schema $\mathcal{S}$, denoted by $G\vDash\mathcal{S}$, if
$\llbracket\phi_{1}\rrbracket^{G}$ is a subset of
$\llbracket\phi_{2}\rrbracket^{G}$, for every statement
$\phi_{1}\subseteq\phi_{2}$ in $\mathcal{S}$.

Thus, any shape schema $\mathcal{S}$ defines the class of graphs that conform
to it. We denote this class of graphs by

$\llbracket\mathcal{S}\rrbracket:=\\{\text{graph $G$}\mid
G\vDash\mathcal{S}\\}.$

Accordingly, two shape schemas $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are
said to be _equivalent_ if
$\llbracket\mathcal{S}_{1}\rrbracket=\llbracket\mathcal{S}_{2}\rrbracket$.

[Example 4 continued] Constraint (7) from the Introduction can be written as:

$\exists\textsf{email}^{-}.\top\subseteq{}\leq_{1}\textsf{email}.\top$

We can see that $G_{ex}$ does not satisfy the constraint, because
$\\{m_{1},m_{2}\\}\not\subseteq\\{m_{2}\\}$. However, if we remove the triple
$(b,\textsf{email},m_{1})$ from $G_{ex}$, then the shape is interpreted as
$\llbracket\leq_{1}\textsf{email}.\top\rrbracket^{I_{\mathit{ex}}}=\\{m_{1},m_{2}\\}$
and the constraint does hold, as
$\\{m_{1},m_{2}\\}\subseteq\\{m_{1},m_{2}\\}$.

##  3\. Expressiveness of SHACL features

When a complicated but influential new tool is proposed in the community, in
our case SHACL, we feel it is important to have a solid understanding of its
design. Concretely, as motivated in the Introduction, our goal is to obtain a
clear picture of the relative expressiveness of the features $\mathit{eq}$,
$\mathit{disj}$, and $\mathit{closed}$. Our methodology is as follows.

A _feature set_ $F$ is a subset of
$\\{\mathit{eq},\mathit{disj},\mathit{closed}\\}$. The set of all shape
schemas using only features from $F$, besides the standard constructs, is
denoted by $\mathcal{L}(F)$. In particular, shape schemas in
$\mathcal{L}(\emptyset)$ use only the standard constructs and none of the
three features. Specifically, they only involve shapes built from boolean
connectives, constants, and qualified number restrictions, with path
expressions built from property names, $\mathit{id}$ and the standard
operators union, composition, and Kleene star.

We say that feature set $F_{1}$ is _subsumed_ by feature set $F_{2}$, denoted
by $F_{1}\preceq F_{2}$, if every shape schema in $\mathcal{L}(F_{1})$ is
equivalent to some shape schema in $\mathcal{L}(F_{2})$. As it will turn out,

$F_{1}\preceq F_{2}\quad\Leftrightarrow\quad F_{1}\subseteq F_{2},$ ($*$)

or intuitively, “every feature counts.” Note that the implication from right
to left is trivial, but the other direction is by no means clear from the
outset.

More specifically, for every feature, we introduce a class of graphs, as
follows. In what follows we fix some property name $r$.

Equality:

$Q_{\mathit{eq}}$ is the class of graphs where all $r$-edges are symmetric.
Note that $Q_{\mathit{eq}}$ is definable in $\mathcal{L}(\mathit{eq})$ by the
single, target-based, inclusion statement $\exists
r.\top\subseteq\mathit{eq}(r^{-},r)$.

Disjointness:

$Q_{\mathit{disj}}$ is the class of graphs where all nodes with an outgoing
$r$-edge have at least one symmetric $r$-edge. This time, $Q_{\mathit{disj}}$
is definable in $\mathcal{L}(\mathit{disj})$, by the single, target-based,
inclusion statement $\exists r.\top\subseteq\neg\mathit{disj}(r^{-},r)$.

Closure:

$Q_{\mathit{closed}}$ is the class of graphs where for all nodes with an
outgoing $r$-edge, all outgoing edges have label $r$. Again
$Q_{\mathit{closed}}$ is definable in $\mathcal{L}(\mathit{closed})$ by the
single, target-based, inclusion statement $\exists
r.\top\subseteq\mathit{closed}(r)$.

We establish the following theorem, from which the above equivalence ($*$ ‣ 3)
immediately follows:

######  Theorem 5.

Let $X\in\\{\mathit{eq},\mathit{disj},\mathit{closed}\\}$ and let $F$ be a
feature set with $X\notin F$. Then $Q_{X}$ is not definable in
$\mathcal{L}(F)$.

For $X=\mathit{closed}$, Theorem 5 is proven differently than for the other
two features. First, we deal with the remaining features through the following
concrete result, illustrated in Figure 2. The formal definition of the graphs
illustrated in Figure 2 for $X=\mathit{disj}$ will be provided in Definition
3.2.

######  Proposition 6.

Let $X=\mathit{disj}$ or $\mathit{eq}$. Let $\Sigma$ be a finite vocabulary
including $r$, and let $m$ be a nonzero natural number. There exist two graphs
$G$ and $G^{\prime}$ with the following properties:

  1. (1)

$G^{\prime}$ belongs to $Q_{X}$, but $G$ does not.

  2. (2)

For every shape $\phi$ over $\Sigma$ such that $\phi$ does not use $X$, and
$\phi$ counts to at most $m$, we have

$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}.$

Here, “counting to at most $m$” means that all quantifiers $\geq_{n}$ used in
$\phi$ satisfy $n\leq m$. For $X=\mathit{eq}$, this proposition is
reformulated as Proposition 12, and for $X=\mathit{disj}$, this proposition is
reformulated as Proposition 14.

To see that Proposition 6 indeed establishes Theorem 5 for the three features
under consideration, we use the notion of _validation shape_ of a shape
schema. This shape evaluates to the set of all nodes that violate the schema.
Thus, the validation shape is an abstraction of the “validation report” in
SHACL [SHA17]: a graph conforms to a schema if and only if the validation
shape evaluates to the empty set. The validation shape can be formally
constructed as the disjunction of $\phi_{1}\land\neg\phi_{2}$ for all
statements $\phi_{1}\subseteq\phi_{2}$ in the schema.

Now consider a shape schema $\mathcal{S}$ not using feature $X$. Let $m$ be
the maximum count used in shapes in $\mathcal{S}$, and let $\Sigma^{\prime}$
be the set of constants and property names mentioned in $\mathcal{S}$. Now
given $\Sigma=\Sigma^{\prime}\cup\\{r\\}$ and $m$, let $G$ and $G^{\prime}$ be
the two graphs exhibited by the Proposition, and let $\phi$ be the validation
shape for $\mathcal{S}$. Then $\phi$ will evaluate to the same result on $G$
and $G^{\prime}$. However, for $\mathcal{S}$ to define $Q_{X}$, validation
would have to return the empty set on $G^{\prime}$ but a nonempty set on $G$.
We conclude that $\mathcal{S}$ does not define $Q_{X}$.

We will prove Proposition 6 for $X=\mathit{disj}$ in Section 3.2, and
$X=\mathit{eq}$ in Section 3.3. We will show Theorem 5 for $X=\mathit{closed}$
in Section 3.4. However, we first need to establish some preliminaries on path
expressions.

$X$ | $G$ | $G^{\prime}$
---|---|---
$\mathit{eq}$ |  |
$\mathit{disj}$ |  |
Figure 2. Graphs used to prove Proposition 6. The nodes are taken outside
$\Sigma$. For $X=\mathit{eq}$, the cloud shown for $G^{\prime}$ represents a
complete directed graph on $m+1$ nodes, with self-loops, and $G$ is the same
graph with one directed edge removed. For $X=\mathit{disj}$, in the picture
for $G$, each cloud again stands for a complete graph, but this time on
$M=\max(m,3)$ nodes, and without the self-loops. Each oval stands for a set of
$M$ separate nodes. An arrow from one blob to the next means that every node
of the first blob has a directed edge to every node of the next blob. So, $G$
is a directed 4-cycle of alternating clouds and ovals, and $G^{\prime}$ is a
directed 4-cycle of clouds.

###  3.1. Preliminaries on path expressions

We call a path expression $E$ _equivalent_ to a path expression $E^{\prime}$
when for every graph $G$, $\llbracket E\rrbracket^{G}=\llbracket
E^{\prime}\rrbracket^{G}$. We call a path expression $E$ _$id$ -free_ whenever
$\mathit{id}$ is not present in the expression.

######  Lemma 7.

Every path expression $E$ is equivalent to: $\mathit{id}$, or
$E^{\prime}\cup\mathit{id}$, or $E^{\prime}$ where $E^{\prime}$ is an
$\mathit{id}$-free path expression.

######  Proof 3.1.

The proof is by induction on the structure of $E$. When $E$ is $id$-free or
$\mathit{id}$, the claim directly follows. We consider the following inductive
cases:

  * •

$E$ is $E_{1}/E_{2}$. By induction, we consider nine cases. When both $E_{1}$
and $E_{2}$ are $\mathit{id}$-free, $E$ is $\mathit{id}$-free. Whenever
$E_{1}$ is $\mathit{id}$, clearly $E$ is equivalent to $E_{2}$. Analogously,
whenever $E_{2}$ is $\mathit{id}$, $E$ is equivalent to $E_{1}$.

Consider the two cases where $E_{1}$ is $E_{1}^{\prime}\cup\mathit{id}$ with
$E_{1}^{\prime}$ an $\mathit{id}$-free path expression. First, when $E_{2}$ is
$E_{2}^{\prime}\cup\mathit{id}$ with $E_{2}^{\prime}$ an $\mathit{id}$-free
path expression, then $E$ is equivalent to $E_{1}^{\prime}/E_{2}^{\prime}\cup
E_{1}^{\prime}\cup E_{2}^{\prime}\cup\mathit{id}$ which is of the form
$E^{\prime}\cup\mathit{id}$ with $E^{\prime}$ the $\mathit{id}$-free path
expression $E_{1}^{\prime}/E_{2}^{\prime}\cup E_{1}^{\prime}\cup
E_{2}^{\prime}$. Second, when $E_{2}$ is $\mathit{id}$-free, $E$ is equivalent
to $E_{1}^{\prime}/E_{2}\cup E_{2}$ which is $\mathit{id}$-free.

Finally, consider the two case where $E_{1}$ is $\mathit{id}$-free and $E_{2}$
is $E_{2}^{\prime}\cup\mathit{id}$ with $E_{2}^{\prime}$ an $\mathit{id}$-free
path expression, then $E$ is equivalent to $E_{1}/E_{2}^{\prime}\cup E_{1}$
which is $\mathit{id}$-free.

  * •

$E$ is $E_{1}\cup E_{2}$. This case follows immediately by induction.

  * •

$E$ is $E_{1}^{*}$. There are three cases. When $E_{1}$ is $\mathit{id}$, $E$
is equivalent to $\mathit{id}$. When $E_{1}$ is
$E_{1}^{\prime}\cup\mathit{id}$ with $E_{1}^{\prime}$ an $\mathit{id}$-free
path expression, then $E$ is equivalent to $E_{1}^{\prime*}$ and clearly
$E_{1}^{\prime*}$ is $\mathit{id}$-free. Lastly, when $E_{1}$ is $id$-free,
clearly $E$ is as well.

We also need the notion of “safe” path expressions together with the following
Lemma, detailing how path expressions can behave on the nodes outside a graph.
One can divide all path expressions into the “safe” and the “unsafe” ones.

[Safety] A path expression is _safe_ if one of the following conditions holds:

  * •

$E$ is $p$ or $p^{-}$ with $p$ a property name

  * •

$E$ is $E_{1}\cup E_{2}$ and both $E_{1}$ and $E_{2}$ are safe

  * •

$E$ is $E_{1}/E_{2}$ and at least one of $E_{1}$ or $E_{2}$ is safe

Otherwise, $E$ is _unsafe_.

######  Lemma 8.

Let $E$ be an $\mathit{id}$-free path expression and let $G$ be a graph.

  * •

If $E$ is safe, then $\llbracket E\rrbracket^{G}\subseteq N_{G}\times N_{G}$.

  * •

If $E$ is unsafe, then $\llbracket E\rrbracket^{G}=(\llbracket
E\rrbracket^{G}\cap N_{G}\times N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$.

######  Proof 3.2.

By induction. If $E$ is a property name or its inverse, then the claim clearly
holds. Now assume $E$ is of the form $E_{1}\cup E_{2}$. The cases where both
$E_{1}$ and $E_{2}$ are safe, or both are unsafe, are clear by induction. If
$E_{1}$ is safe but $E_{2}$ is not, then $\llbracket
E\rrbracket^{G}=\llbracket E_{1}\rrbracket^{G}\cup\llbracket
E_{2}\rrbracket^{G}=(\llbracket E_{1}\rrbracket^{G}\cap N_{G}\times
N_{G})\cup(\llbracket E_{2}\rrbracket^{G}\cap N_{G}\times
N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}=\llbracket
E\rrbracket^{G}\cap(N_{G}\times N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$. The
same reasoning can be used when $E_{2}$ is safe but $E_{1}$ is not.

Next, assume $E$ is of the form $E_{1}/E_{2}$. Furthermore assume $E_{1}$ is
safe, so that $E$ is safe. Let $(x,y)\in\llbracket E\rrbracket^{G}$. Then
there exists $z$ such that $(x,z)\in\llbracket E_{1}\rrbracket^{G}$ and
$(z,y)\in\llbracket E_{2}\rrbracket^{G}$. Since $E_{1}$ is safe, $x$ and $z$
are in $N_{G}$. Now regardless of whether $E_{2}$ is safe or not, since
$(z,y)\in\llbracket E_{2}\rrbracket^{G}$ and $z\in N_{G}$, we get $y\in N_{G}$
as desired. The same reasoning can be used when $E_{2}$ is safe.

If $E$ is not safe, we verify that $\llbracket E\rrbracket^{G}=(\llbracket
E\rrbracket^{G}\cap N_{G}\times N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$. For
the inclusion from left to right, take $(x,y)\in\llbracket E\rrbracket^{G}$.
Then there exists $z$ such that $(x,z)\in\llbracket E_{1}\rrbracket^{G}$ and
$(z,y)\in\llbracket E_{2}\rrbracket^{G}$. By induction, there are four cases.
If both $(x,z)$ and $(z,y)$ are in $N_{G}\times N_{G}$, then clearly
$(x,y)\in\llbracket E\rrbracket^{G}\cap N_{G}\times N_{G}$. If both
$(x,z),(z,y)$ are in $\\{(a,a)\mid a\in N-N_{G}\\}$ clearly
$(x,y)\in\\{(a,a)\mid a\in N-N_{G}\\}$. Lastly, the two cases where one of
$(x,z)$ and $(z,y)$ is in $N_{G}\times N_{G}$ and the other in $\\{(a,a)\mid
a\in N-N_{G}\\}$, are not possible.

For the inclusion from right to left, take $(x,y)\in\llbracket
E\rrbracket^{G}\cap(N_{G}\times N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$. If
$(x,y)\in\llbracket E\rrbracket^{G}\cap N_{G}\times N_{G}$ then
$(x,y)\in\llbracket E\rrbracket^{G}$. Otherwise, $(x,y)=(a,a)$ for some $a\in
N-N_{G}$. Then $(a,a)\in\llbracket E_{1}\rrbracket^{G}$ and
$(a,a)\in\llbracket E_{2}\rrbracket^{G}$ since $E_{1}$ and $E_{2}$ are not
safe. We conclude $(a,a)\in\llbracket E_{1}/E_{2}\rrbracket^{G}$ as desired.

Next, assume $E$ is of the form $E_{1}^{*}$. Note that $E$ is unsafe. By
definition of Kleene star, we only need to verify that $\llbracket
E\rrbracket^{G}\subseteq(\llbracket E\rrbracket^{G}\cap N_{G}\times
N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$. Let $(x,y)\in\llbracket
E\rrbracket^{G}$. If $x=y$, the claim clearly holds. Otherwise, we consider
two cases:

  * •

If $E_{1}$ is safe, we know $\llbracket E_{1}\rrbracket^{G}\subseteq
N_{G}\times N_{G}$. Clearly the reflexive-transitive closure of a subset of
$N_{G}\times N_{G}$ is also a subset of $N_{G}\times N_{G}$. Therefore,
$(x,y)\in N_{G}\times N_{G}$ as desired.

  * •

If $E_{1}$ is unsafe, then by induction $\llbracket
E_{1}\rrbracket^{G}=(\llbracket E_{1}\rrbracket^{G}\cap N_{G}\times
N_{G})\cup\\{(a,a)\mid a\in N-N_{G}\\}$. As $x\neq y$ we know $(x,y)$ is in
the reflexive-transitive closure of $\llbracket E_{1}\rrbracket^{G}\cap
N_{G}\times N_{G}$ which is a subset of $N_{G}\times N_{G}$.

Lastly, we define the notion of a _string_ , together with the following
Lemma, detailing a convenient property of path expressions.

A string $s$ is a path expression of the form: $\mathit{id}$, or
$s^{\prime}/p$ or $s^{\prime}/p^{-}$ where $s^{\prime}$ is a string and $p$ is
a property name.

######  Lemma 9.

For every path expression $E$ and every natural number $n$, there exists a
finite non-empty set of strings $U$ s.t. for every graph $G$ with at most $n$
nodes we have $\llbracket E\rrbracket^{G}=\bigcup_{s\in U}\llbracket
s\rrbracket^{G}$.

The proof of Lemma 9 can be found in the appendix.

###  3.2. Disjointness

We present here the proof for $X=\mathit{disj}$. The general strategy is to
first characterize the behavior of path expressions on $G$ and $G^{\prime}$.
Then the Proposition is proven with a stronger induction hypothesis, to allow
the induction to carry through. A similar strategy is followed in the proof
for $X=\mathit{eq}$.

We begin by defining the graphs $G$ and $G^{\prime}$ more formally.
[$G_{\mathit{disj}}(\Sigma,m)$] Let $\Sigma$ be a finite vocabulary including
$r$, and let $m$ be a natural number. We define the graph
$G_{\mathit{disj}}(\Sigma,m)$ over the set of property names in $\Sigma$ as
follows. Let $M=\max(m,3)$. There are $4M$ nodes in the graph, which are
chosen outside of $\Sigma$. We denote these nodes by $x_{i}^{j}$ for
$i=1,2,3,4$ and $j=1,\dots,M$. (In the description that follows, subscripts
range from $1$ to $4$ and superscripts range from $1$ to $M$.) For each
property name $p$ in $\Sigma$, the graph has the same set of $p$-edges. We
describe these edges next. There is an edge from $x_{i}^{j}$ to $x_{i\bmod
4+1}^{j^{\prime}}$ for every $i$, $j$ and $j^{\prime}$. Moreover, if $i$ is 2
or 4, there is an edge from $x_{i}^{j}$ to $x_{i}^{j^{\prime}}$ for all $j\neq
j^{\prime}$. So, formally, we have:
$G_{\mathit{disj}}(\Sigma,m):=\\{(x_{i}^{j},p,x_{i\bmod 4+1}^{j^{\prime}})\mid
i\in\\{1,\dots,4\\}\;\text{and}\;j,j’\in\\{1,\dots,M\\}\;\text{and}\;p\in\Sigma\cap
P\\}\cup\\{(x_{i}^{j},p,x_{i}^{j^{\prime}})\mid
i\in\\{1,\dots,4\\}\;\text{and}\;j,j’\in\\{1,\dots,M\\}\;\text{and}\;j\neq
j’\;\text{and}\;p\in\Sigma\cap P\\}$.

Thus, in Figure 2, bottom left, one can think of the left oval as the set of
nodes $x_{1}^{j}$; the top cloud as the set of nodes $x_{2}^{j}$; and so on.
We call the nodes $x_{i}^{j}$ with $i=2,4$ the _even nodes_ , and the nodes
$x_{i}^{j}$ with $i=1,3$ the _odd nodes_.

[$G^{\prime}_{\mathit{disj}}(\Sigma,m)$] We define the graph
$G^{\prime}_{\mathit{disj}}(\Sigma,m)$ in the same way as
$G_{\mathit{disj}}(\Sigma,m)$ except that there is an edge from $x_{i}^{j}$ to
$x_{i}^{j^{\prime}}$ for all $i$ and $j\neq j^{\prime}$ (not only for even $i$
values).

We characterize the behavior of path expressions on the graph
$G_{\mathit{disj}}(\Sigma,m)$ as follows.

######  Lemma 10.

Let $G$ be $G_{\mathit{disj}}(\Sigma,m)$. Call a path expression _simple_ if
it is a union of expressions of the form $s_{1}/\dots/s_{n}$, where $n\geq 1$
and one of the $s_{i}$ is a property name while the other $s_{i}$ are
“$\mathit{id}$”. Let $E$ be a non-simple, $\mathit{id}$-free path expression
over $\Sigma$. The following three statements hold:

  1. (1)

    1. (a)

for all even nodes $v$ of $G$, we have $\llbracket
E\rrbracket^{G}(v)\supseteq\llbracket r\rrbracket^{G}(v)$; or

    2. (b)

for all even nodes $v$ of $G$, we have $\llbracket
E\rrbracket^{G}(v)\supseteq\llbracket r^{-}\rrbracket^{G}(v)$.

  2. (2)

    1. (c)

for all odd nodes $v$ of $G$, we have $\llbracket
E\rrbracket^{G}(v)\supseteq\llbracket r\rrbracket^{G}(v)$; or

    2. (d)

for all odd nodes $v$ of $G$, we have $\llbracket
E\rrbracket^{G}(v)\supseteq\llbracket r^{-}\rrbracket^{G}(v)$.

  3. (3)

For all nodes $v$ of $G$, we have $\llbracket E\rrbracket^{G}(v)-\llbracket
r\rrbracket^{G}(v)\neq\emptyset$.

######  Proof 3.3.

For $i=1,2,3,4$, define the _i-th blob of nodes_ to be the set
$X_{i}=\\{x_{i}^{1},\dots,x_{i}^{M}\\}$ (see Figure 2). We also use the
notations $\mathit{next}(1)=2$; $\mathit{next}(2)=3$; $\mathit{next}(3)=4$;
$\mathit{next}(4)=1$; $\mathit{prev}(4)=3$; $\mathit{prev}(3)=2$;
$\mathit{prev}(2)=1$; $\mathit{prev}(1)=4$. Thus $\mathit{next}(i)$ indicates
the next blob in the cycle, and $\mathit{prev}(i)$ the previous.

The proof is by induction on the structure of $E$. If $E$ is a property name,
$E$ is simple so the claim is trivial. If $E$ is of the form $p^{-}$, cases B
and D are clear and we only need to verify the third statement. That holds
because for any $i$, if $v\in X_{i}$, then $\llbracket
p^{-}\rrbracket^{G}(v)\supseteq X_{\mathit{prev}(i)}$ and clearly
$X_{\mathit{prev}(i)}-\llbracket r\rrbracket^{G}(v)\neq\emptyset$. We next
consider the inductive cases.

First, assume $E$ is of the form $E_{1}\cup E_{2}$. When at least one of
$E_{1}$ and $E_{2}$ is not simple, the three statements immediately follow by
induction, since $\llbracket E\rrbracket^{G}\supseteq\llbracket
E_{1}\rrbracket^{G}$ and $\llbracket E\rrbracket^{G}\supseteq\llbracket
E_{2}\rrbracket^{G}$. If $E_{1}$ and $E_{2}$ are simple, then $E$ is simple
and the claim is trivial.

Next, assume $E$ is of the form $E_{1}^{*}$. If $E_{1}$ is not simple, the
three statements follow immediately by induction, since $\llbracket
E\rrbracket^{G}\supseteq\llbracket E_{1}\rrbracket^{G}$. If $E_{1}$ is simple,
cases A and C clearly hold for $E$, so we only need to verify the third
statement. That holds because, by the form of $E$, every node $v$ is in
$\llbracket E\rrbracket^{G}(v)$, but not in $\llbracket r\rrbracket^{G}(v)$,
as $G$ does not have any self-loops.

Finally, assume $E$ is of the form $E_{1}/E_{2}$. Note that if $E_{1}$ or
$E_{2}$ is simple, clearly cases A and C apply to them. The argument that
follows will therefore also apply when $E_{1}$ or $E_{2}$ is simple. We will
be careful not to apply the induction hypothesis for the third statement to
$E_{1}$ and $E_{2}$.

We first focus on the even nodes, and show the first and the third statement.
We distinguish two cases.

  * •

If case A applies to $E_{2}$, then we show that case A also applies to $E$.
Let $v\in X_{i}$ be an even node. We verify the following two inclusions:

    * –

$\llbracket E\rrbracket^{G}(v)\supseteq X_{i}$. Let $u\in X_{i}$. If $u\neq
v$, choose a third node $w\in X_{i}$. Since $X_{i}$ is a clique,
$(v,w)\in\llbracket E_{1}\rrbracket^{G}$ regardless of whether case A or B
applies to $E_{1}$. By case A for $E_{2}$, we also have $(w,u)\in\llbracket
E_{2}\rrbracket^{G}$, whence $u\in\llbracket E\rrbracket^{G}(v)$ as desired.
If $u=v$, we similarly have $(v,w)\in\llbracket E_{1}\rrbracket^{G}$ and
$(w,u)\in\llbracket E_{2}\rrbracket^{G}$ as desired.

    * –

$\llbracket E\rrbracket^{G}(v)\supseteq X_{\mathit{next}(i)}$. Let $u\in
X_{\mathit{next}(i)}$ and choose $w\neq v\in X_{i}$. Regardless of whether
case A or B applies to $E_{1}$, we have $(v,w)\in\llbracket
E_{1}\rrbracket^{G}$. By case A for $E_{2}$, we also have $(w,u)\in\llbracket
E_{2}\rrbracket^{G}$, whence $u\in\llbracket E\rrbracket^{G}(v)$ as desired.

We conclude that $\llbracket E\rrbracket^{G}(v)\supseteq X_{i}\cup
X_{\mathit{next}(i)}\supseteq\llbracket r\rrbracket^{G}$ as desired.

  * •

If case B applies to $E_{2}$, then we show that case B also applies to $E$.
This is analogous to the previous case, now verifying that $\llbracket
E\rrbracket^{G}(v)\supseteq X_{i}\cup X_{\mathit{prev}(i)}$.

In both cases, the third statement now follows for even nodes $v$. Indeed,
$v\in X_{i}\subseteq\llbracket E\rrbracket^{G}(v)$ but $v\notin\llbracket
r\rrbracket^{G}(v)$.

We next focus on the odd nodes, and show the second and the third statement.
We again consider two cases.

  * •

If case C applies to $E_{1}$, then we show that case C also applies to $E$.
Let $v\in X_{i}$ be an odd node. Note that $\llbracket
r\rrbracket^{G}(v)=X_{\mathit{next}(i)}$. To verify that $\llbracket
E\rrbracket^{G}(v)\supseteq X_{\mathit{next}(i)}$, let $u\in
X_{\mathit{next}(i)}$. Then $u$ is even. Choose $w\neq u\in
X_{\mathit{next}(i)}$. Since case C applies to $E_{1}$, we have
$(v,w)\in\llbracket E_{1}\rrbracket^{G}$. Moreover, since
$X_{\mathit{next}(i)}$ is a clique, $(w,u)\in\llbracket E_{2}\rrbracket^{G}$
regardless of whether case A or B applies to $E_{2}$. We obtain
$(v,u)\in\llbracket E\rrbracket^{G}$ as desired.

We also verify the third statement for odd nodes in this case. We distinguish
two further cases.

    * –

If case A applies to $E_{2}$, any node $u\in
X_{\mathit{next}(\mathit{next}(i))}$ belongs to $\llbracket
E\rrbracket^{G}(v)$, and clearly these $u$ are not in
$X_{\mathit{next}(i)}=\llbracket r\rrbracket^{G}(v)$.

    * –

If case B applies to $E_{2}$, then, since $X_{i}$ is a clique, any node $u\in
X_{i}$ belongs to $\llbracket E\rrbracket^{G}(v)$, and again these $u$ are not
in $X_{\mathit{next}(i)}$.

  * •

If case D applies to $E_{1}$, then we show that case D also applies to $E$.
This is analogous to the previous case, now verifying that $\llbracket
E\rrbracket^{G}(v)\supseteq X_{\mathit{prev}(i)}$. In this case the third
statement for odd nodes is clear, as clearly
$X_{\mathit{prev}(i)}-X_{\mathit{next}(i)}\neq\emptyset$.

We similarly characterize the behavior of path expressions on the other graph.

######  Lemma 11.

Let $G^{\prime}$ be $G^{\prime}_{\mathit{disj}}(\Sigma,m)$ and let $E$ be a
non-simple, $\mathit{id}$-free path expression over $\Sigma$. The following
statements hold:

  1. (1)

$\llbracket E\rrbracket^{G^{\prime}}\supseteq\llbracket
r\rrbracket^{G^{\prime}}$ or $\llbracket
E\rrbracket^{G^{\prime}}\supseteq\llbracket r^{-}\rrbracket^{G^{\prime}}$.

  2. (2)

For all nodes $v$ of $G^{\prime}$, we have $\llbracket
E\rrbracket^{G^{\prime}}(v)-\llbracket
r\rrbracket^{G^{\prime}}(v)\neq\emptyset$.

######  Proof 3.4.

The proof is similar to the proof of Lemma 10, but simpler due to the
homogeneous nature of the graph $G^{\prime}$. We omit the proof.

We are now ready to prove the non-obvious part of Proposition 6 where
$X=\mathit{disj}$. We use the following version of the proposition.

######  Proposition 12.

Let $V$ be the common set of nodes of the graphs
$G=G_{\mathit{disj}}(\Sigma,m)$ and
$G^{\prime}=G^{\prime}_{\mathit{disj}}(\Sigma,m)$. Let $\phi$ be a shape over
$\Sigma$ that does not use $\mathit{disj}$, and that counts to at most $m$.
Then either $\llbracket\phi\rrbracket^{G}\cap V=\emptyset$ or
$\llbracket\phi\rrbracket^{G}\supseteq V$. Moreover,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$.

######  Proof 3.5.

This is proven by induction on the structure of $\phi$. Let $H$ be $G$ or
$G^{\prime}$. If $\phi$ is $\top$, then
$\llbracket\top\rrbracket^{H}=N\supseteq V$. If $\phi$ is $\\{c\\}$, then
$\llbracket\\{c\\}\rrbracket^{H}=\\{c\\}\subseteq\Sigma$ and we know that
$\Sigma\cap V=\emptyset$. Next assume $\phi$ is of the form
$\mathit{eq}(E,p)$. Using Lemma 7, we distinguish four different cases for
$E$.

  * •

$E$ is $\mathit{id}$. According to Lemma 10 and Lemma 11 $\llbracket
E\rrbracket^{H}$ will always contain either $\llbracket p\rrbracket^{H}$ or
$\llbracket p^{-}\rrbracket^{H}$. In both cases, $\llbracket
E\rrbracket^{H}(v)$ clearly never equals
$\llbracket\mathit{id}\rrbracket^{H}(v)=\\{v\\}$. Therefore,
$\llbracket\phi\rrbracket^{H}\cap V=\emptyset$.

  * •

$E$ is $E^{\prime}\cup\mathit{id}$ where $E^{\prime}$ is $\mathit{id}$-free or
$E$ itself is $\mathit{id}$-free and non-simple. Lemmas 10 and 11 tell us that
$\llbracket E\rrbracket^{H}(v)-\llbracket r\rrbracket^{H}(v)\neq\emptyset$ for
every $v\in V$. Since $\llbracket r\rrbracket^{H}=\llbracket p\rrbracket^{H}$,
this means $H,v\nvDash\phi$ for $v\in V$, or, equivalently,
$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$. To see that, moreover,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$, it
remains to show that $G,v\vDash\phi$ iff $G^{\prime},v\vDash\phi$ for all node
names $v\notin V$.

  * •

$E$ is $\mathit{id}$-free and simple. Then $\llbracket
E\rrbracket^{H}=\llbracket p\rrbracket^{H}$, so clearly
$\llbracket\phi\rrbracket^{H}=N\supseteq V$.

We still need to show
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$. Clearly,
$\llbracket p\rrbracket^{G}(v)=\llbracket
p\rrbracket^{G^{\prime}}(v)=\emptyset$. Now by Lemma 8, if $E$ is safe, then
also $\llbracket E\rrbracket^{G}(v)=\llbracket
E\rrbracket^{G^{\prime}}(v)=\emptyset$, so $G,v\vDash\phi$ and
$G^{\prime},v\vDash\phi$. On the other hand, if $E$ is unsafe, then by the
same Lemma $\llbracket E\rrbracket^{G}(v)=\llbracket
E\rrbracket^{G^{\prime}}(v)=\\{v\\}\neq\emptyset$, so $G,v\nvDash\phi$ and
$G^{\prime},v\nvDash\phi$, as desired.

As the final base case, assume $\phi$ is of the form $\mathit{closed}(R)$. If
$\Sigma$ contains a property name $p$ not in $R$, then
$\llbracket\phi\rrbracket^{H}\cap V=\emptyset$, since every node in $H$ has an
outgoing $p$-edge. Otherwise, i.e., if $\Sigma\subseteq R$, we have
$\llbracket\phi\rrbracket^{H}\supseteq V$, since every node in $H$ has only
outgoing edges labeled by property names in $\Sigma$. To see that, moreover,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$, it
suffices to observe that trivially $H,v\vDash\phi$ for all node names $v\notin
V$.

We next consider the inductive cases. The cases for the boolean connectives
follow readily by induction. Finally, assume $\phi$ is of the form
$\mathop{\geq}\nolimits_{n}E.\phi_{1}$. By induction, there are two
possibilities for $\phi_{1}$:

  * •

If $\llbracket\phi_{1}\rrbracket^{H}\cap V=\emptyset$, then also
$\llbracket\phi\rrbracket^{H}\cap V=\emptyset$ since path expressions can only
reach nodes in some graph from nodes in that graph.

  * •

If $\llbracket\phi_{1}\rrbracket^{H}\supseteq V$, we distinguish three cases
using Lemma 7. First, when $E$ is $\mathit{id}$, then if $n=1$,
$\llbracket\phi\rrbracket^{H}\supseteq V$. Otherwise, if $n\neq 1$, then
$\llbracket\phi\rrbracket^{H}=\emptyset$. Next, when $E$ is $\mathit{id}$-free
or $E^{\prime}\cup\mathit{id}$ with $E^{\prime}$ an $\mathit{id}$-free path
expression, it suffices to show that $\sharp\llbracket
E^{\prime}\rrbracket^{H}(v)\geq n$ for all $v\in V$. By Lemmas 10 and 11 we
know that $\llbracket E_{1}\rrbracket^{H}(v)$ contains $\llbracket
r\rrbracket^{H}(v)$ or $\llbracket r^{-}\rrbracket^{H}(v)$. Inspecting $H$, we
see that each of these sets has at least $\max(3,m)\geq n$ elements, as
desired. Finally, when $E$ is equivalent to an $\mathit{id}$-free path
expression or whenever $E$ simply does not use $\mathit{id}$, the argument is
analogous to the previous case.

In both cases we still need to show that
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$. We
already showed that $\llbracket\phi\rrbracket^{G}\supseteq V$ and
$\llbracket\phi\rrbracket^{G^{\prime}}\supseteq V$, or
$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$ and
$\llbracket\phi\rrbracket^{G^{\prime}}\cap V=\emptyset$. Therefore, towards a
proof of the equality, we only need to consider the node names not in $V$.

For the inclusion from left to right, take
$x\in\llbracket\phi\rrbracket^{G}-V$. Since $G,x\vDash\phi$, there exist
$y_{1}$, …, $y_{n}$ such that $(x,y_{i})\in\llbracket E\rrbracket^{G}$ and
$G,y_{i}\vDash\phi_{1}$ for $i=1,\dots,n$. However, since $x\notin V$, by
Lemma 8, all $y_{i}$ must equal $x$. Hence, $n=1$ and $(x,x)\in\llbracket
E\rrbracket^{G}$ and $G,x\vDash\phi_{1}$. Then again by the same Lemma,
$(x,x)\in\llbracket E\rrbracket^{G^{\prime}}$, since $G$ and $G^{\prime}$ have
the same set of nodes $V$. Moreover, by induction,
$G^{\prime},x\vDash\phi_{1}$. We conclude that $G^{\prime},x\vDash\phi$ as
desired. The inclusion from right to left is argued symmetrically.

###  3.3. Equality

Next, we turn our attention to Proposition 6 for $X=\mathit{eq}$. We define
the graphs from Figure 2 formally.

Let $\Sigma$ be a finite vocabulary including $r$, and let $m$ be a natural
number. Choose a set $V$ of node names outside $\Sigma$, of cardinality
$M:=\max(3,m+1)$. Fix two arbitrary nodes $a$ and $b$ from $V$. We define the
graph $G_{\mathit{eq}}(\Sigma)$ over the set of property names from $\Sigma$
as follows. For each property name $p$ in $\Sigma$, the set of $p$-edges in
$G_{\mathit{eq}}(\Sigma)$ equals $V\times V-(b,a)$. We define the graph
$G_{\mathit{eq}}^{\prime}(\Sigma)$ similarly, but with $V\times V$ as the set
of $p$-edges.

So, $G^{\prime}_{\mathit{eq}}(\Sigma,m)$ is a complete graph, and
$G_{\mathit{eq}}(\Sigma,m)$ is a complete graph with one edge $(b,a)$ removed.

######  Lemma 13.

Let $E$ be an $\mathit{id}$-free path expression over $\Sigma$ and let
$H=G_{\mathit{eq}}(\Sigma,m)$ or $G^{\prime}_{\mathit{eq}}(\Sigma,m)$. Then

  1. (1)

$\llbracket E\rrbracket^{H}\supseteq\llbracket r\rrbracket^{H}$, or

  2. (2)

$\llbracket E\rrbracket^{H}\supseteq\llbracket r^{-}\rrbracket^{H}$.

######  Proof 3.6.

The claim is obvious for $G^{\prime}_{\mathit{eq}}(\Sigma,m)$, being a
complete graph. So we focus on the graph $G_{\mathit{eq}}(\Sigma,m)$. The
proof is by induction. If $E$ is a property name or its inverse, the claim is
clear. If $E$ is of the form $E_{1}\cup E_{2}$, the claim is immediate by
induction.

Assume $E$ is of the form $E_{1}/E_{2}$. We show that A applies.444Actually,
$\llbracket E\rrbracket^{G}$ always contains $V\times V$ in this case, but we
do not need this. If A applies to $E_{1}$, this is clear, since we can follow
any edge by $E_{1}$ and then stay at the head of the edge by $E_{2}$ using the
self-loop. If B applies to $E_{1}$, the same can still be done for all edges
except for $(a,b)$, which is the only nonsymmetrical edge. To go from $a$ to
$b$ by $E$, we go by $E_{1}$ from $a$ to a node $c$ distinct from $a$ and $b$,
then go by $E_{2}$ from $c$ to $b$.

If $E$ is of the form $E_{1}^{*}$, again A applies, since ${E_{1}^{*}}$
contains ${E_{1}/E_{1}}$.

We are now ready to prove the non-obvious part of Proposition 6 where
$X=\mathit{eq}$. We use the following version of the proposition.

######  Proposition 14.

Let $G$ be $G_{\mathit{eq}}(\Sigma,m)$ and let $G^{\prime}$ be
$G^{\prime}_{\mathit{eq}}(\Sigma,m)$. Let $\phi$ be a shape over $\Sigma$ that
does not use $\mathit{eq}$ and that counts to at most $m$. Then either
$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$ or
$\llbracket\phi\rrbracket^{G}\supseteq V$. Moreover,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$.

######  Proof 3.7.

This is proven by induction on the structure of $\phi$. Let $H$ be $G$ or
$G^{\prime}$. We focus directly on the relevant cases. Assume $\phi$ is of the
form $\mathit{disj}(E_{1},E_{2})$. Lemma 13 clearly yields that
$\llbracket\phi\rrbracket^{H}\cap V=\emptyset$. It again remains to verify
that $G,v\vDash\phi$ iff $G^{\prime},v\vDash\phi$ for all node names $v\notin
V$. By Lemma 8, for such $v$ and $H=G$ or $G^{\prime}$, we indeed have
$H,v\vDash\phi$ if exactly one of $E_{1}$ and $E_{2}$ is safe. If both are
safe or both are unsafe, we have $H,v\nvDash\phi$.

The last base case of interest is the case where $\phi$ is of the form
$\mathit{closed}(R)$. This goes again exactly as in the proof for
$X=\mathit{disj}$.

We next consider the inductive cases. The cases for the boolean connectives
follow readily by induction. Finally, assume $\phi$ is of the form
$\mathop{\geq}\nolimits_{n}E.\phi_{1}$. By induction, there are two
possibilities for $\phi_{1}$:

  * •

If $\llbracket\phi_{1}\rrbracket^{G}\cap V=\emptyset$ then
$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$ since path expressions can only
reach nodes in some graph from nodes in that graph.

  * •

If $\llbracket\phi_{1}\rrbracket^{H}\supseteq V$, we distinguish three cases
using Lemma 7. First, when $E$ is $\mathit{id}$, then if $n=1$,
$\llbracket\phi\rrbracket^{H}\supseteq V$. Otherwise, if $n\neq 1$, then
$\llbracket\phi\rrbracket^{H}=\emptyset$. Next, when $E$ is $\mathit{id}$-free
or $E^{\prime}\cup\mathit{id}$ with $E^{\prime}$ an $\mathit{id}$-free path
expression, it suffices to show that $\sharp\llbracket
E^{\prime}\rrbracket^{H}(v)\geq n$ for all $v\in V$. By Lemma 13, we know that
$\llbracket E\rrbracket^{H}(v)$ contains $\llbracket r\rrbracket^{H}(v)$ or
$\llbracket r^{-}\rrbracket^{H}(v)$. These sets contain at least $M-1\geq
m\geq n$ elements as desired. (The number $M-1$ is reached only when $H$ is
$G$ and $v=b$ or $v=a$; otherwise the sets contain $M$ elements.)

The equality
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$ is shown
in the same way as in the proof for $X=\mathit{disj}$ (Section 3.2).

###  3.4. Closure

Without using $\mathit{closed}$, shapes cannot say anything about properties
that they do not explicitly mention. We formalize this intuitive observation
as follows. The proof is straightforward.

######  Lemma 15.

Let $\Sigma$ be a vocabulary, let $E$ be a path expression over $\Sigma$, and
let $\phi$ be a shape over $\Sigma$ that does not use $\mathit{closed}$. Let
$G_{1}$ and $G_{2}$ be graphs such that $\llbracket
p\rrbracket^{G_{1}}=\llbracket p\rrbracket^{G_{2}}$ for every property name
$p$ in $\Sigma$. Then $\llbracket E\rrbracket^{G_{1}}=\llbracket
E\rrbracket^{G_{2}}$ and
$\llbracket\phi\rrbracket^{G_{1}}=\llbracket\phi\rrbracket^{G_{2}}$. ∎

Theorem 5 now follows readily for $X=\mathit{closed}$. Let $F$ be a feature
set without $\mathit{closed}$, let $\mathcal{S}$ be a shape schema in
$\mathcal{L}(F)$, and let $\phi$ be the validation shape of $\mathcal{S}$. Let
$p$ be a property name not mentioned in $\mathcal{S}$, and different from $r$.
Consider the graphs $G=\\{(a,r,a),(a,p,a)\\}$ and $G^{\prime}=\\{(a,r,a)\\}$,
so that $G^{\prime}$ belongs to $Q_{\mathit{closed}}$ but $G$ does not. By
Lemma 15 we have
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$, showing
that $\mathcal{S}$ does not define $Q_{\mathit{closed}}$.

######  Remark 16.

Lemma 15 fails completely in the presence of closure constraints. The simplest
counterexample is to consider $\Sigma=\emptyset$ and the shape
$\mathit{closed}(\emptyset)$. Trivially, any two graphs agree on the property
names from $\Sigma$. However,
$\llbracket\mathit{closed}(\emptyset)\rrbracket^{G}$, which equals the set of
node names that do not have an outgoing edge in $G$ (they may still have an
incoming edge), obviously depends on the graph $G$.

The reader may wonder if this statement still holds under active domain
semantics. In such semantics, which we denote by
$\llbracket\phi\rrbracket^{G}_{\mathit{adom}}$, we would view $G$ as an
interpretation with domain _not_ the whole of $N$; rather we would take as
domain the set $N_{G}\cup C$, with $C$ the set of constants mentioned in
$\phi$. When assuming active domain semantics, a modified lemma is required.
To see this, consider the graph $G=\\{(a,p,b)\\}$ and
$G^{\prime}=\\{(a,p,b),(a,q,c)\\}$. Let $\phi$ simply be $\top$. We have
$\llbracket\phi\rrbracket^{G}_{\mathit{adom}}=\\{a,b\\}$ and
$\llbracket\phi\rrbracket^{G^{\prime}}_{\mathit{adom}}=\\{a,b,c\\}$, so Lemma
15 no longer holds. We can, however, give the following more refined variant
of Lemma 15:

######  Lemma 17.

Let $\Sigma$ be a vocabulary, let $E$ be a path expression over $\Sigma$, and
let $\phi$ be a shape over $\Sigma$ that does not use $\mathit{closed}$. Let
$I_{1}$ and $I_{2}$ be interpretations such that $\llbracket
p\rrbracket^{I_{1}}=\llbracket p\rrbracket^{I_{2}}$ for every property name
$p$ in $\Sigma$. Then $\llbracket
E\rrbracket^{I_{1}}\cap\Delta^{I_{2}}\times\Delta^{I_{2}}=\llbracket
E\rrbracket^{I_{2}}\cap\Delta^{I_{1}}\times\Delta^{I_{1}}$ and
$\llbracket\phi\rrbracket^{I_{1}}\cap\Delta^{I_{2}}=\llbracket\phi\rrbracket^{I_{2}}\cap\Delta^{I_{1}}$.
∎

The same reasoning as given after Lemma 15, now using the new Lemma, then
shows that $\mathit{closed}$ is still primitive under active domain semantics.

##  4\. Are target-based shape schemas enough?

Lemma 15 also allows us to clarify that, as far as expressive power is
concerned, and in the absence of closure constraints, the restriction to
target-based shape schemas is inconsequential.

######  Theorem 18.

Every generalized shape schema that does not use closure constraints is
equivalent to a target-based shape schema (that still does not use closure
constraints).

In order to prove this theorem, we first establish the following lemma.

######  Lemma 19.

Let $\phi$ be a shape and let $C$ be the set of constants mentioned in $\phi$.
Assume there exists a graph $G$ and a node name $x\notin N_{G}\cup C$ such
that $G,x\vDash\phi$. Then for any graph $H$ and any node name $y\notin
N_{H}\cup C$, also $H,y\vDash\phi$.

######  Proof 4.1.

By induction on $\phi$. The case where $\phi$ is of the form $\\{c\\}$ cannot
occur, and the case where $\phi$ is $\top$ is trivial.

If $\phi$ is $\phi_{1}\lor\phi_{2}$ or $\neg\phi_{1}$, the claim follows
readily by induction.

Now assume $\phi$ is of the form $\mathop{\geq}\nolimits_{n}E.\phi_{1}$. Then
there exists $x_{1},\dots,x_{n}$ such that $(x,x_{i})\in\llbracket
E\rrbracket^{G}$ and $G,x_{i}\vDash\phi_{1}$ for $i=1,\dots,n$. However, since
$x\notin N_{G}$, by Lemma 8, all $x_{i}$ must equal $x$. Hence, $n=1$ and
$(x,x)\in\llbracket E\rrbracket^{G}$ and $G,x\vDash\phi_{1}$. By the same
Lemma, $(y,y)\in\llbracket E\rrbracket^{H}$, since $y\notin N_{H}$.
Furthermore, by induction, $H,y\vDash\phi_{1}$. We conclude that
$H,y\vDash\phi$ as desired.

Next, assume $\phi$ is $\mathit{eq}(E,p)$. Since $G,x\vDash\phi$, but
$\llbracket p\rrbracket^{G}=\emptyset$ since $x\notin N_{G}$, also $\llbracket
E\rrbracket^{G}(x)=\emptyset$. Then by Lemma 8, also $\llbracket
E\rrbracket^{H}(y)=\emptyset$, since $y\notin N_{H}$. Furthermore, also
$\llbracket p\rrbracket^{H}(y)=\emptyset$. We conclude that $H,y\vDash\phi$ as
desired.

Next assume $\phi$ is $\mathit{disj}(E,p)$. Then $H,y\vDash\phi$ is clear.
Indeed, since $y\notin N_{H}$, we have $\llbracket
p\rrbracket^{H}(y)=\emptyset$.

Finally, assume $\phi$ is $\mathit{closed}(R)$. Then again $H,y\vDash\phi$ is
clear because $y\notin N_{H}$.

We can now show the theorem.

######  Proof 4.2 (Proof of Theorem 18).

Let $\phi$ be the validation shape for shape schema $\mathcal{S}$, so that
$G\vDash\mathcal{S}$ if and only if $\llbracket\phi\rrbracket^{G}$ is empty.
Let $C$ be the set of constants mentioned in $\phi$.

Let us say that $\phi$ is _internal_ if for every graph $G$ and every node
name $v$ such that $G,v\vDash\phi$, we have $v\in N_{G}\cup C$. If $\phi$ is
not internal, then, using Lemma 19, for every graph $G$ and every node
$v\notin N_{G}\cup C$, we have $G,v\vDash\phi$. Thus, if $\phi$ is not
internal, $\mathcal{S}$ is unsatisfiable and is equivalent to the single
target-based inclusion $\\{c\\}\subseteq\neg\top$, for an arbitrary constant
$c$.

So now assume $\phi$ is internal. Define the target-based shape schema
$\mathcal{T}$ consisting of the following inclusions:

  * •

For each constant $c\in C$, the inclusion $\\{c\\}\subseteq\neg\phi$.

  * •

For each property name mentioned in $\phi$, the two inclusions $\exists
p.\top\subseteq\neg\phi$ and $\exists p^{-}.\top\subseteq\neg\phi$.

We will show that $\mathcal{S}$ and $\mathcal{T}$ are equivalent. Let $\psi$
be the validation shape for $\mathcal{T}$.

Let $G$ be any graph, and let $G^{\prime}$ be the graph obtained from $G$ by
removing all triples involving property names not mentioned in $\phi$. We
reason as follows:

$\displaystyle G\vDash\mathcal{S}$
$\displaystyle\Leftrightarrow\llbracket\phi\rrbracket^{G}=\emptyset$
$\displaystyle\Leftrightarrow\llbracket\phi\rrbracket^{G^{\prime}}=\emptyset$
by Lemma 15 $\displaystyle\Leftrightarrow G^{\prime}\vDash\mathcal{T}$ since
$\phi$ is internal
$\displaystyle\Leftrightarrow\llbracket\psi\rrbracket^{G^{\prime}}=\emptyset$
$\displaystyle\Leftrightarrow\llbracket\psi\rrbracket^{G}=\emptyset$ by Lemma
15 $\displaystyle\Leftrightarrow G\vDash\mathcal{T}$

######  Remark 20.

Note that we do not need class-based targets in the proof, so such targets are
redundant on the left-hand sides of inclusions. This can also be seen
directly: any inclusion

$\exists\textsf{type}/\textsf{subclass}^{*}.\\{c\\}\subseteq\phi$

with a class-based target is equivalent to the following inclusion with a
subjects-of target:

$\exists\textsf{type}.\top\subseteq\neg\exists\textsf{type}/\textsf{subclass}^{*}.\\{c\\}\lor\phi$

######  Remark 21.

Theorem 18 fails in the presence of closure constraints. For example, the
inclusion $\neg\mathit{closed}(\emptyset)\subseteq\exists r.\top$ defines the
class of graphs where every node with an outgoing edge has an outgoing
$r$-edge. Suppose this inclusion would be equivalent to a target-based shape
schema $\mathcal{S}$, and let $R$ be the set of all property names mentioned
in the targets of $\mathcal{S}$. Let $p$ be a property name not in $R$ and
distinct from $r$; let $a$ be a node name not used as a constant in
$\mathcal{S}$; and consider the graph $G=\\{(a,p,a)\\}$. This graph trivially
satisfies $\mathcal{S}$, but violates the inclusion.

##  5\. Extensions for full equality and disjointness tests

A quirk in the design of SHACL is that it only allows equality and
disjointness tests $\mathit{eq}(E_{1},E_{2})$ and $\mathit{disj}(E_{1},E_{2})$
where $E_{1}$ can be a general path expression, but $E_{2}$ needs to be a
property name. The next question we can ask is whether allowing “full”
equality or disjointness tests, i.e., allowing a general path expression for
$E_{2}$, strictly increases the expressive power. Within the community there
are indeed plans to extend SHACL in this direction [Knu21, Jak22].

When we allow for such “full” equality and disjointness tests, it gives rise
to two new features: $\mathit{full\text{-}eq}$ and
$\mathit{full\text{-}disj}$. Formally, we extend the grammar of shapes with
two new constructs: $\mathit{eq}(E_{1},E_{2})$ and
$\mathit{disj}(E_{1},E_{2})$.

######  Remark 22.

We extend Remark 3 by noting that in real SHACL, we cannot explicitly write
the shapes $\mathit{eq}(\mathit{id},\mathit{id})$ and
$\mathit{disj}(\mathit{id},\mathit{id})$. However, these shapes are equivalent
to $\top$ and $\neg\top$ respectively.

We are going to show that each of these new features strictly adds expressive
power. Concretely, we introduce the following classes of graphs.

Full equality:

$Q_{\mathit{full\text{-}eq}}$ is the class of graphs where all objects of a
property name $p$ do not have the same subjects for $p$ and $q$. Note that
$Q_{\mathit{full\text{-}eq}}$ is definable in
$\mathcal{L}(\mathit{full\text{-}eq})$ by the single, target-based, inclusion
statement $\exists p^{-}.\top\subseteq\neg\mathit{eq}(p^{-},q^{-})$.

Full disjointness:

$Q_{\mathit{full\text{-}disj}}$ is the class of graphs where all objects of a
property name $p$ do not have disjoint sets of subjects for $p$ and $q$. Note
that $Q_{\mathit{full\text{-}disj}}$ is definable in
$\mathcal{L}(\mathit{full\text{-}disj})$ by the single, target-based,
inclusion statement $\exists
p^{-}.\top\subseteq\neg\mathit{disj}(p^{-},q^{-})$.

In the spirit of Theorem 5, we are now going to show the following:

######  Theorem 23.

$Q_{\mathit{full\text{-}eq}}$ is not definable in
$\mathcal{L}(\mathit{eq},\mathit{full\text{-}disj},\mathit{closed})$ and
$Q_{\mathit{full\text{-}disj}}$ is not definable in
$\mathcal{L}(\mathit{disj},\mathit{full\text{-}eq},\mathit{closed})$.

These two non-definability results are proven in the following Sections 5.1
and 5.2. Then in Section 5.3 we will reconsider the non-definability results
for non-full equality and disjointness from Theorem 5 in the new light of
their full versions.

###  5.1. Full equality

We present here the proof for the primitivity of full equality tests. The
general strategy is the same as in Section 3, where again we will prove
appropriate versions of Proposition 6.

We begin by defining the graphs $G$ and $G^{\prime}$ formally. Note that, as
desired, $G^{\prime}$ belongs to $Q_{\mathit{full\text{-}eq}}$ but $G$ does
not. $G_{\mathit{full\text{-}eq}}(\Sigma,m)$ Let $\Sigma$ be a finite
vocabulary and let $m\geq 3$ be a natural number. Let
$A=\\{a_{1},\dots,a_{m}\\}$, $B=\\{b_{1},\dots,b_{m}\\}$ and
$C=\\{c_{1},\dots,c_{m}\\}$ be three disjoint sets of nodes, disjoint from
$\Sigma$. We define the graph $G_{\mathit{full\text{-}eq}}(\Sigma,m)$ to be
$\llbracket p\rrbracket^{G}=C\times(A\cup B)$ and $\llbracket
q\rrbracket^{G}=C\times A\cup\\{(c_{i},b_{j})\mid i\neq
j\in\\{1,\dots,m\\}\\}$.

$G^{\prime}_{\mathit{full\text{-}eq}}(\Sigma,m)$ We define the graph
$G^{\prime}_{\mathit{full\text{-}eq}}(\Sigma,m)$ like
$G_{\mathit{full\text{-}eq}}(\Sigma,m)$ but $\llbracket
q\rrbracket^{G}=\\{(c_{i},a_{j})\mid i\neq
j\in\\{1,\dots,m\\}\\}\cup\\{(c_{i},b_{j})\mid i\neq j\in\\{1,\dots,m\\}\\}$.

We identify the possible types of strings on the graphs
$G_{\mathit{full\text{-}eq}}(\Sigma,m)$ and
$G^{\prime}_{\mathit{full\text{-}eq}}(\Sigma,m)$ as follows.

######  Lemma 24.

Let $\Sigma$ be a vocabulary. Let $m\geq 3$ be a natural number. Let $G$ be
$G_{\mathit{full\text{-}eq}}(\Sigma,m)$ and let $G^{\prime}$ be
$G^{\prime}_{\mathit{full\text{-}eq}}(\Sigma,m)$. The only possibilities for a
string $s$ evaluated on $G$ and $G^{\prime}$ are the following:

  1. (1)

$\llbracket s\rrbracket^{G}=\llbracket p\rrbracket^{G}=\llbracket
s\rrbracket^{G^{\prime}}=C\times(A\cup B)$.

  2. (2)

$\llbracket s\rrbracket^{G}=\llbracket q\rrbracket^{G}=(C\times
A)\cup\\{(c_{i},b_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}$ and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
q\rrbracket^{G^{\prime}}=\\{(c_{i},a_{j})\mid i\neq
j\in\\{1,\dots,m\\}\\}\cup\\{(c_{i},b_{j})\mid i\neq j\in\\{1,\dots,m\\}\\}$.

  3. (3)

$\llbracket s\rrbracket^{G}=\llbracket p^{-}\rrbracket^{G}=\llbracket
s\rrbracket^{G^{\prime}}=(A\cup B)\times C$.

  4. (4)

$\llbracket s\rrbracket^{G}=\llbracket q^{-}\rrbracket^{G}=(A\times
C)\cup\\{(b_{i},c_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}$ and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
q^{-}\rrbracket^{G^{\prime}}=\\{(a_{i},c_{j})\mid i\neq
j\in\\{1,\dots,m\\})\\}\cup\\{(b_{i},c_{j})\mid i\neq
j\in\\{1,\dots,m\\})\\}$.

  5. (5)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=C\times C$.

  6. (6)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=(A\cup
B)\times(A\cup B)$.

  7. (7)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=\mathit{id}$.

  8. (8)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=\emptyset$.

######  Proof 5.1.

We show this by systematically enumerating all strings until no new binary
relations can be found. Note that we only enumerate over strings that
alternate between property names and reversed property names. Indeed, all
other strings evaluate to the empty relation on both $G$ and $G^{\prime}$.
Every time we encounter new binary relations, we put the string in boldface.

$s$ | $\llbracket s\rrbracket^{G}$ | $\llbracket s\rrbracket^{G^{\prime}}$
---|---|---
$\mathbf{id}$ | $\mathit{id}$ | $\mathit{id}$
$\mathbf{p}$ | $C\times(A\cup B)$ | $C\times(A\cup B)$
$\mathbf{q}$ | $(C\times A)\cup{}$ | $\\{(c_{i},a_{j})\mid i\neq j\in\\{1,\dots,m\\}\\}\cup{}$
| $\\{(c_{i},b_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}$ | $\\{(c_{i},b_{j})\mid i\neq j\in\\{1,\dots,m\\}\\}$
$\mathbf{p^{-}}$ | $(A\cup B)\times C$ | $(A\cup B)\times C$
$\mathbf{q^{-}}$ | $(A\times C)\cup{}$ | $\\{(a_{i},c_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}\cup{}$
| $\\{(b_{i},c_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}$ | $\\{(b_{i},c_{j})\mid i\neq j\in\\{1,\dots,m\\})\\}$
$\mathbf{p/p^{-}}$ | $C\times C$ | $C\times C$
$p/q^{-}$ | $C\times C$ | $C\times C$
$q/p^{-}$ | $C\times C$ | $C\times C$
$q/q^{-}$ | $C\times C$ | $C\times C$
$\mathbf{p^{-}/p}$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$p^{-}/q$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$q^{-}/p$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$q^{-}/q$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$p/p^{-}/p$ | $C\times(A\cup B)$ | $C\times(A\cup B)$
$p/p^{-}/q$ | $C\times(A\cup B)$ | $C\times(A\cup B)$
$p^{-}/p/p^{-}$ | $(A\cup B)\times C$ | $(A\cup B)\times C$
$p^{-}/p/q^{-}$ | $(A\cup B)\times C$ | $(A\cup B)\times C$

We are now ready to prove the key proposition.

######  Proposition 25.

Let $\Sigma$ be a vocabulary. Let $m\geq 3$ be a natural number. Let $V=A\cup
B\cup C$ be the common set of nodes of the graphs
$G=G_{\mathit{full\text{-}eq}}(\Sigma,m)$ and
$G^{\prime}=G^{\prime}_{\mathit{full\text{-}eq}}(\Sigma,m)$. For all shapes
$\phi$ over $\Sigma$ counting to at most $m-1$, we have
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$.
Moreover,

  * •

$\llbracket\phi\rrbracket^{G}\cap V=A\cup B$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=C$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=V$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$.

######  Proof 5.2.

By induction on the structure of $\phi$. For the base cases, if $\phi$ is
$\top$ then
$\llbracket\top\rrbracket^{G}=\llbracket\top\rrbracket^{G^{\prime}}=N$ and
$N\cap V=V$. If $\phi$ is $\\{c\\}$, then
$\llbracket\\{c\\}\rrbracket^{G}=\llbracket\\{c\\}\rrbracket^{G^{\prime}}=\\{c\\}$
and $\\{c\\}\cap V=\emptyset$ since $c\in\Sigma$ and $V\cap\Sigma=\emptyset$.

If $\phi$ is $\mathit{closed}(Q)$, we consider the possibilities for $Q$. If
$Q$ does not contain both $p$ and $q$, then clearly
$\llbracket\phi\rrbracket^{G}\cap V=\llbracket\phi\rrbracket^{G^{\prime}}\cap
V=A\cup B$. Otherwise,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}=N$.

Before considering the remaining cases, we observe the following symmetries:

  * •

All elements of $A$ are symmetrical in $G$. This is obvious from the
definition of $G$.

  * •

Also in $G^{\prime}$, all elements of $A$ are symmetrical. Indeed, for any
$a_{i}\neq a_{j}$ in $A$, the function that swaps $a_{i}$ and $a_{j}$, as well
as $c_{i}$ and $c_{j}$, is an automorphism of $G^{\prime}$.

  * •

Similarly, all elements of $B$ are symmetrical in $G$, and also in
$G^{\prime}$.

  * •

Moreover, we see that all elements of $C$ are symmetrical in $G$, and in
$G^{\prime}$.

  * •

Finally, in $G^{\prime}$, any $a_{i}$ and $b_{j}$ are symmetrical. Indeed, the
function that swaps $a_{i}$ and $b_{i}$ is clearly an automorphism of
$G^{\prime}$. In turn, $b_{i}$ and $b_{j}$ are symmetrical by the above.

Therefore, we are only left to show:

  1. (1)

For any $a\in A$ and $b\in B$, we have $G,a\vDash\phi\iff G,b\vDash\phi$,

  2. (2)

For any $a\in A$, we have $G,a\vDash\phi\iff G^{\prime},a\vDash\phi$, and

  3. (3)

For any $c\in C$, we have $G,c\vDash\phi\iff G^{\prime},c\vDash\phi$.

  4. (4)

For any $x\not\in V$, we have $G,x\vDash\phi\iff G^{\prime},x\vDash\phi$.

Note that then also for any $b\in B$, we have $G,b\vDash\phi\iff
G^{\prime},b\vDash\phi$ because for any $a\in A$ and $b\in B$, we have
$G,b\vDash\phi\stackrel{{\scriptstyle\rm\ref{en:p11}}}{{\iff}}G,a\vDash\phi\stackrel{{\scriptstyle\rm\ref{en:p12}}}{{\iff}}G^{\prime},a\vDash\phi\stackrel{{\scriptstyle\mathit{symmetry}}}{{\iff}}G^{\prime},b\vDash\phi$.

Consider the case where $\phi$ is $\mathit{eq}(E,r)$. We verify 1, 2, 3, and
4.

  1. 1

By definition of $G$, $\llbracket r\rrbracket^{G}(a)=\llbracket
r\rrbracket^{G}(b)=\emptyset$ for any property name $r$. Therefore we need to
show $\llbracket E\rrbracket^{G}(a)=\emptyset\iff\llbracket
E\rrbracket^{G}(b)=\emptyset$. By Lemma 9 we know there is a set of strings
$U$ equivalent to $E$ in both $G$ and $G^{\prime}$. By Lemma 24 there are only
8 types of strings. We observe from Lemma 24 that for every $U$,
$\bigcup_{s\in U}\llbracket s\rrbracket^{G}(a)$ is empty whenever $U$ only
contains strings of type 1, 2, 5, or 8. These are also exactly the $U$ s.t.
$\bigcup_{s\in U}\llbracket s\rrbracket^{G}(b)$ is empty.

  2. 2

Furthermore, these are also exactly the sets of strings $U$ s.t.
$\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(a)$ is empty. Therefore,
as $\llbracket r\rrbracket^{G^{\prime}}(a)=\emptyset$, we have
$G^{\prime},a\vDash\phi$.

  3. 3

Assume $G,c\vDash\phi$. We consider the possibilities for $r$. First, suppose
$r=p$. The sets of strings $U$ s.t. $\bigcup_{s\in U}\llbracket
s\rrbracket^{G}(c)=\llbracket p\rrbracket^{G}(c)$ contain strings of type 1
but not strings of type 5 or 7. These are also exactly the $U$ s.t.
$\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)=\llbracket
p\rrbracket^{G^{\prime}}(c)$.

Next, suppose $r=q$. The sets of strings $U$ s.t. $\bigcup_{s\in U}\llbracket
s\rrbracket^{G}(c)=\llbracket p\rrbracket^{G}(c)$ contain strings of type 2
but not strings of type 1, 5 or 7. These are also exactly the types of strings
s.t. $\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)=\llbracket
q\rrbracket^{G^{\prime}}(c)$.

Finally, if $r$ is any other property name, then $\llbracket
r\rrbracket^{G}(c)=\llbracket r\rrbracket^{G^{\prime}}(c)=\emptyset$. This is
the case when $U$ does not contain any strings of type 1, 2, 3, or 7. These
are also exactly the types of strings $U$ s.t. $\bigcup_{s\in U}\llbracket
s\rrbracket^{G^{\prime}}(c)=\emptyset$.

  4. 4

Let $x\in N-V$. Clearly $\llbracket r\rrbracket^{G}(x)=\llbracket
r\rrbracket^{G^{\prime}}(x)=\emptyset$. By Lemma 8, if $E$ is safe, then
$\llbracket E\rrbracket^{G}(x)=\llbracket
E\rrbracket^{G^{\prime}}(x)=\emptyset$. Therefore $G,x\vDash\phi$ and
$G^{\prime},x\vDash\phi$. On the other hand, whenever $E$ is unsafe,
$\llbracket E\rrbracket^{G}(x)=\llbracket
E\rrbracket^{G^{\prime}}(x)=\\{x\\}\neq\emptyset$. Therefore,
$G,x\not\vDash\phi$ and $G^{\prime},x\not\vDash\phi$.

Next, consider the case where $\phi$ is $disj(E_{1},E_{2})$. We again verify
1, 2, 3, and 4.

  1. 1

Assume $G,a\vDash\mathit{disj}(E_{1},E_{2})$. This can only be the case when
the corresponding sets of strings $U_{1}$ and $U_{2}$ are of the following
form. $U_{1}$ can consist only of strings of type 3, 4, 1, 2, 5, and 8 (Here,
types 1, 2, 5 and 8 evaluate to empty from $a$ as already seen above). $U_{2}$
can then only consist of strings of type 6, 7, 1, 2, 5, and 8 (or vice versa).
These are also the only cases where $G,b\vDash\mathit{disj}(E_{1},E_{2})$.

  2. 2

Exactly the same situation occurs in $G^{\prime}$ and these are then also the
only cases where $G^{\prime},a\vDash\mathit{disj}(E_{1},E_{2})$.

  3. 3

Assume $G,c\vDash\mathit{disj}(E_{1},E_{2})$. This can only be the case when
the corresponding sets of strings $U_{1}$ and $U_{2}$ are of the following
form. $U_{1}$ can consist only of strings of type 1, 2, 3, 4, 6, and 8 (Here,
types 3, 4, 6, and 8 evaluate to empty from $c$ as already seen above).
$U_{2}$ can then only consist of strings of type 5, 7, 3, 4, 6, and 8. We
observe that this is also the case in $G^{\prime}$.

  4. (1)

4 Let $x\in N-V$. Whenever $E_{1}$ is safe, by Lemma 8 $\llbracket
E_{1}\rrbracket^{G}(x)=\llbracket E_{1}\rrbracket^{G^{\prime}}(x)=\emptyset$.
Therefore, $G,x\vDash\phi$ and $G^{\prime},x\vDash\phi$. Clearly, the same
holds whenever $E_{2}$ is safe. When both $E_{1}$ and $E_{2}$ are unsafe,
$\llbracket E_{1}\rrbracket^{G}(x)=\llbracket
E_{1}\rrbracket^{G^{\prime}}(x)=\\{x\\}\neq\emptyset$. Therefore,
$G,x\not\vDash\phi$ and $G^{\prime},x\not\vDash\phi$.

The cases where $\phi$ is $\phi_{1}\land\phi_{2}$, $\phi_{1}\lor\phi_{2}$ or
$\neg\phi_{1}$ are handled by induction in a straightforward manner.

Lastly, we consider the case where $\phi$ is
$\mathop{\geq}\nolimits_{n}E.\phi_{1}$.

  1. 1

Assume $G,a\vDash\phi$. Then, there exist distinct $x_{1},\dots,x_{n}$ s.t.
$(a,x_{i})\in\llbracket E\rrbracket^{G}$ and $G,x_{i}\vDash\phi_{1}$ for
$1\leq i\leq n$. Again, by Lemma 9 we know there is a set of strings $U$
equivalent to $E$ in both $G$ and $G^{\prime}$. By Lemma 24 there are only 8
types of strings. By induction, we consider three cases.

First, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=A\cup B$, then
$x_{i},\dots,x_{n}\in A\cup B$. Therefore, we know $U$ must at least contain
strings of type 6 or 7. Suppose $U$ contains strings of type 6. Then, we
verify that $\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G}(b)\cap(A\cup
B))\geq m-1\geq n$. Whenever $U$ contains strings of type 7, and not of type
6, we know $n=1$ and clearly $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G}(b)\cap(A\cup B))=1$.

Next, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=C$, then
$x_{i},\dots,x_{n}\in C$. Therefore, we know $U$ must at least contain strings
of type 3 or 4. Whenever $U$ contains 3 or 4, we verify that
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G}(b)\cap C)\geq m-1\geq n$.

Next, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=V$, then
$x_{i},\dots,x_{n}\in V$. Therefore, we know $U$ must at least contain strings
of type 3, 4, 6 or 7. All these types have already been handled in the
previous two cases.

Finally, the case where $\llbracket\phi_{1}\rrbracket^{G}\cap V=\emptyset$
cannot occur as $n>0$.

The sets of strings $U$ above are also exactly the sets used to argue the
implication from right to left.

  2. 2

For every case of $U$ above, for every inductive case of $\phi_{1}$, we can
also verify that $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G^{\prime}}(a)\cap(A\cup B))\geq m-1\geq n$,
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(a)\cap C)\geq
m-1\geq n$, and $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G^{\prime}}(a)\cap V)\geq m-1\geq n$.

  3. 3

Assume $G,c\vDash\phi$. Then, there exist distinct $x_{1},\dots,x_{n}$ s.t.
$(c,x_{i})\in\llbracket E\rrbracket^{G}$ and $G,x_{i}\vDash\phi_{1}$ for
$1\leq i\leq n$. By induction, we consider three cases.

First, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=A\cup B$, then
$x_{i},\dots,x_{n}\in A\cup B$. Therefore, we know $U$ must at least contain
strings of type 1 or 2. Whenever $U$ contains 1 or 2, we verify that
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)\cap(A\cup
B))\geq m\geq n$.

Next, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=C$, then
$x_{i},\dots,x_{n}\in C$. Therefore, we know $U$ must at least contain strings
of type 5 or 7. Whenever $U$ contains 5, we verify that $\sharp(\bigcup_{s\in
U}\llbracket s\rrbracket^{G^{\prime}}(c)\cap C)\geq m\geq n$. Otherwise,
whenever $U$ contains strings of type 7, and not of type 5, we know $n=1$ and
clearly $\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)\cap
C)=1$.

Next, if $\llbracket\phi_{1}\rrbracket^{G}\cap V=V$, then
$x_{i},\dots,x_{n}\in V$. Therefore, we know $U$ must at least contain strings
of type 1, 2, 5 or 7. All these types have already been handled in the
previous two cases.

Finally, the case where $\llbracket\phi_{1}\rrbracket^{G}\cap V=\emptyset$
cannot occur as $n>0$.

The sets of strings $U$ above are also exactly the sets used to argue the
implication from right to left.

  4. 4

For the direction from left to right, take
$x\in\llbracket\phi\rrbracket^{G}\setminus V$. Since $G,x\vDash\phi$, there
exists $y_{1},\dots,y_{n}$ s.t. $(x,y_{i})\in\llbracket E\rrbracket^{G}$ and
$G,y_{i}\vDash\phi_{1}$ for $i=1,\dots,n$. However, since $x\not\in V$, by
Lemma 8, all $y_{i}$ must equal $x$. Hence, $n=1$ and $(x,x)\in\llbracket
E\rrbracket^{G}$ and $G,x\vDash\phi_{1}$. Then again, by the same Lemma,
$(x,x)\in\llbracket E\rrbracket^{G^{\prime}}$, since $G$ and $G^{\prime}$ have
the same set of nodes $V$. Moreover, by induction,
$G^{\prime},x\vDash\phi_{1}$. We conclude $G^{\prime},x\vDash\phi$ as desired.
The direction from right to left is argued symmetrically.

###  5.2. Full disjointness

We present here the proof for the primitivity of full disjointness tests. The
general strategy is the same as in Section 5.1.

We begin by defining the graphs $G$ and $G^{\prime}$ formally.
$G_{\mathit{full\text{-}disj}}(\Sigma,m)$ Let $m$ be a natural number that is
a multiple of $8$. Let $A=\\{a_{1},\dots,a_{m}\\}$,
$B=\\{b_{1},\dots,b_{m}\\}$ and $C=\\{c_{1},\dots,c_{m}\\}$ be three disjoint
sets of nodes, disjoint from $\Sigma$. For any $i\leq j$, we write $a_{i\to
j}$ to denote the set

$\\{a_{1+(i-1+l\mod m)}\mid 0\leq l\leq j-i\\}$

We define $b_{i\to j}$ and $c_{i\to j}$ analogously.

We define the graph $G_{\mathit{full\text{-}disj}}(\Sigma,m)$ by:

$\displaystyle\llbracket p\rrbracket^{G}(c_{i})$ $\displaystyle=a_{i\to
i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\;\text{and}$
$\displaystyle\llbracket q\rrbracket^{G}(c_{i})$
$\displaystyle=a_{i-\frac{m}{2}\to i-1}\cup b_{i-\frac{m}{2}\to
i+\frac{m}{8}-1}\;\text{for $1\leq i\leq m$}$

The $p$ and $q$ relations are visualized in Figure 3.

To give an example for our notation, suppose $m=8$. Then,

$\displaystyle a_{2\to 5}$ $\displaystyle=\\{a_{1+(1+l\mod 8)}\mid 0\leq l\leq
3\\}=\\{a_{2},a_{3},a_{4},a_{5}\\}$ $\displaystyle a_{7\to 10}$
$\displaystyle=\\{a_{1+(6+l\mod 8)}\mid 0\leq l\leq
3\\}=\\{a_{7},a_{8},a_{1},a_{2}\\},\;\text{and}$ $\displaystyle a_{-4\to-1}$
$\displaystyle=\\{a_{1+(-5+l\mod 8)}\mid 0\leq l\leq
3\\}=\\{a_{4},a_{5},a_{6},a_{7}\\}$

$G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$ We define the graph
$G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$ on the same nodes as
$G_{\mathit{full\text{-}disj}}(\Sigma,m)$, with the only difference being the
relationship of the $p$\- and $q$-edges from $C$ to $A$:

$\displaystyle\llbracket p\rrbracket^{G}(c_{i})$
$\displaystyle=a_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to
i+\frac{m}{2}-1}\;\text{and}$ $\displaystyle\llbracket q\rrbracket^{G}(c_{i})$
$\displaystyle=a_{i-\frac{m}{2}\to i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to
i+\frac{m}{8}-1}\;\text{for $1\leq i\leq m$}$

The $p$ and $q$ relations are visualized in Figure 3.

Important to the intuition behind these graphs is the overlap generated by the
inverse $p$\- and $q$-edges. As demonstrated in Figure 4, in graph
$G=G_{\mathit{full\text{-}disj}}(\Sigma,m)$, the set of $c$ nodes reached from
$a$ nodes with inverse $p$ edges is disjoint from the set of $c$ nodes reached
with inverse $q$ edges. This is not the case for $b$ nodes: there, these sets
overlap by precisely one fourth of the $c$ nodes. For graph
$G^{\prime}=G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$, the sets of $c$
nodes reachable by inverse $p$ and $q$ edges overlap for both $a$ and $b$
nodes.

We precisely characterize the behavior of strings on the graphs $G$ and
$G^{\prime}$ as follows.

######  Lemma 26.

Let $\Sigma$ be a vocabulary. Let $m$ be a natural number that is a multiple
of $8$. Let $G$ be $G_{\mathit{full\text{-}disj}}(\Sigma,m)$ and let
$G^{\prime}$ be $G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$. The only
possibilities for a string $s$ evaluated on $G$ and $G^{\prime}$ are the
following:

  1. (1)

$\llbracket s\rrbracket^{G}=\llbracket
p\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i\to
i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1})$ and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
p\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{8}\to
i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1})$;

  2. (2)

$\llbracket s\rrbracket^{G}=\llbracket
q\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{2}\to
i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1})$ and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
q\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{2}\to
i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1})$;

  3. (3)

$\llbracket s\rrbracket^{G}=\llbracket
p^{-}\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{2}+1\to i})\cup(\\{b_{i}\\}\times c_{i-\frac{m}{2}+1\to
i+\frac{m}{8}})$ and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
p^{-}\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{2}+1\to i+\frac{m}{8}})\cup(\\{b_{i}\\}\times
c_{i-\frac{m}{2}+1\to i+\frac{m}{8}})$ ;

  4. (4)

$\llbracket s\rrbracket^{G}=\llbracket
q^{-}\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times c_{i+1\to
i+\frac{m}{2}})\cup(\\{b_{i}\\}\times c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})$
and
$\llbracket s\rrbracket^{G^{\prime}}=\llbracket
q^{-}\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})\cup(\\{b_{i}\\}\times
c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})$;

  5. (5)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=C\times C$;

  6. (6)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=(A\cup
B)\times(A\cup B)$;

  7. (7)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=C\times(A\cup
B)$;

  8. (8)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=(A\cup
B)\times C$;

  9. (9)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=\mathit{id}$;
or

  10. (10)

$\llbracket s\rrbracket^{G}=\llbracket s\rrbracket^{G^{\prime}}=\emptyset$

The first four types of strings are visualized in Figure 3 and Figure 4.

######  Proof 5.3.

The proof is performed as in the proof of Lemma 24. We now have the following
table:

$s$ | $\llbracket s\rrbracket^{G}$ | $\llbracket s\rrbracket^{G^{\prime}}$
---|---|---
$\mathbf{id}$ | $\mathit{id}$ | $\mathit{id}$
$\mathbf{p}$ | type 1 | type 1
$\mathbf{q}$ | type 2 | type 2
$\mathbf{p^{-}}$ | type 3 | type 3
$\mathbf{q^{-}}$ | type 4 | type 4
$\mathbf{p/p^{-}}$ | $C\times C$ | $C\times C$
$p/q^{-}$ | $C\times C$ | $C\times C$
$q/p^{-}$ | $C\times C$ | $C\times C$
$q/q^{-}$ | $C\times C$ | $C\times C$
$\mathbf{p^{-}/p}$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$p^{-}/q$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$q^{-}/p$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$q^{-}/q$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$\mathbf{p/p^{-}/p}$ | $C\times(A\cup B)$ | $C\times(A\cup B)$
$p/p^{-}/q$ | $C\times(A\cup B)$ | $C\times(A\cup B)$
$\mathbf{p^{-}/p/p^{-}}$ | $(A\cup B)\times C$ | $(A\cup B)\times C$
$p^{-}/p/q^{-}$ | $(A\cup B)\times C$ | $(A\cup B)\times C$
$p/p^{-}/p/p^{-}$ | $C\times C$ | $C\times C$
$p/p^{-}/p/q^{-}$ | $C\times C$ | $C\times C$
$p^{-}/p/p^{-}/p$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$
$p^{-}/p/p^{-}/q$ | $(A\cup B)\times(A\cup B)$ | $(A\cup B)\times(A\cup B)$

$\llbracket
p\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i\to
i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1})$

$c_{i}$

$a_{i}$

$b_{i}$

$\llbracket
q\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{2}\to
i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1})$

$c_{i}$

$a_{i}$

$b_{i}$

$\llbracket
p\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{8}\to
i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1})$

$c_{i}$

$a_{i}$

$b_{i}$

$\llbracket
q\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}\\{c_{i}\\}\times(a_{i-\frac{m}{2}\to
i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1})$

$c_{i}$

$a_{i}$

$b_{i}$

Figure 3. Illustration of the $p$ and $q$ relations in graphs
$G=G_{\mathit{full\text{-}disj}}(\Sigma,m)$ and
$G^{\prime}=G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$

$\llbracket
p^{-}\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{2}+1\to i})\cup(\\{b_{i}\\}\times c_{i-\frac{m}{2}+1\to
i+\frac{m}{8}})$

$a_{i}$

$c_{i}$

$b_{i}$

$c_{i}$

$\llbracket
q^{-}\rrbracket^{G}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times c_{i+1\to
i+\frac{m}{2}})\cup(\\{b_{i}\\}\times c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})$

$a_{i}$

$c_{i}$

$b_{i}$

$c_{i}$

$\llbracket
p^{-}\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{2}+1\to i+\frac{m}{8}})\cup(\\{b_{i}\\}\times
c_{i-\frac{m}{2}+1\to i+\frac{m}{8}})$

$a_{i}$

$c_{i}$

$b_{i}$

$c_{i}$

$\llbracket
q^{-}\rrbracket^{G^{\prime}}=\bigcup_{i\in\\{1,\dots,m\\}}(\\{a_{i}\\}\times
c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})\cup(\\{b_{i}\\}\times
c_{i-\frac{m}{8}+1\to i+\frac{m}{2}})$

$a_{i}$

$c_{i}$

$b_{i}$

$c_{i}$

Figure 4. Illustration of the $p^{-}$ and $q^{-}$ relations in graphs
$G=G_{\mathit{full\text{-}disj}}(\Sigma,m)$ and
$G^{\prime}=G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$

We are ready to present our key Proposition.

######  Proposition 27.

Let $\Sigma$ be a vocabulary. Let $m$ be a natural number and a multiple of 8.
Let $V=A\cup B\cup C$ be the common set of nodes of the graphs
$G=G_{\mathit{full\text{-}disj}}(\Sigma,m)$ and
$G^{\prime}=G^{\prime}_{\mathit{full\text{-}disj}}(\Sigma,m)$. For all shapes
$\phi$ over $\Sigma$ counting to at most $\frac{m}{2}$, we have
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}$.
Moreover,

  * •

$\llbracket\phi\rrbracket^{G}\cap V=A\cup B$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=C$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=V$, or

  * •

$\llbracket\phi\rrbracket^{G}\cap V=\emptyset$.

######  Proof 5.4.

By induction on the structure of $\phi$. For the base cases, if $\phi$ is
$\top$ then
$\llbracket\top\rrbracket^{G}=\llbracket\top\rrbracket^{G^{\prime}}=N$ and
$N\cap V=V$. If $\phi$ is $\\{c\\}$, then
$\llbracket\\{c\\}\rrbracket^{G}=\llbracket\\{c\\}\rrbracket^{G^{\prime}}=\\{c\\}$
and $\\{c\\}\cap V=\emptyset$ since $c\in\Sigma$ and $V\cap\Sigma=\emptyset$.

If $\phi$ is $\mathit{closed}(Q)$, we consider the possibilities for $Q$. If
$Q$ does not contain both $p$ and $q$, then clearly
$\llbracket\phi\rrbracket^{G}\cap V=\llbracket\phi\rrbracket^{G^{\prime}}\cap
V=A\cup B$. Otherwise,
$\llbracket\phi\rrbracket^{G}=\llbracket\phi\rrbracket^{G^{\prime}}=N$.

Before considering the remaining cases, we observe the following symmetries:

  * •

In both $G$ and $G^{\prime}$, all elements of $A$ are symmetrical, as are all
elements of $B$, and all elements of $C$. Indeed, for any
$i\in\\{1,\dots,m\\}$, the function that maps $x_{i}$ to $x_{1+i\mod m}$ where
$x_{i}$ is $a_{i}$, $b_{i}$ or $c_{i}$, is clearly an automorphism of $G$ and
also of $G^{\prime}$.

  * •

Furthermore, in $G^{\prime}$, any $a_{i}$ and $b_{j}$ are symmetrical. Indeed,
the function that swaps every $a_{i}$ with $b_{i}$ is an automorphism of
$G^{\prime}$. (We already know that $b_{i}$ and $b_{j}$ are symmetrical by the
above.)

Therefore, we are only left to show:

  1. (1)

For any $a\in A$ and $b\in B$, we have $G,a\vDash\phi\iff G,b\vDash\phi$,

  2. (2)

For any $a\in A$, we have $G,a\vDash\phi\iff G^{\prime},a\vDash\phi$, and

  3. (3)

For any $c\in C$, we have $G,c\vDash\phi\iff G^{\prime},c\vDash\phi$.

  4. (4)

For any $x\not\in V$, we have $G,x\vDash\phi\iff G^{\prime},x\vDash\phi$.

Note that then also for any $b\in B$, we have $G,b\vDash\phi\iff
G^{\prime},b\vDash\phi$ because for any $a\in A$ and $b\in B$, we have
$G,b\vDash\phi\stackrel{{\scriptstyle\rm\ref{en:p11}}}{{\iff}}G,a\vDash\phi\stackrel{{\scriptstyle\rm\ref{en:p12}}}{{\iff}}G^{\prime},a\vDash\phi\stackrel{{\scriptstyle\mathit{symmetry}}}{{\iff}}G^{\prime},b\vDash\phi$.

Consider the case where $\phi$ is $\mathit{disj}(E,r)$. We verify 1, 2, 3, and
4. First, to see that 1 and 2 hold, we observe that $\llbracket
r\rrbracket^{G}(a)=\llbracket r\rrbracket^{G}(b)=\llbracket
r\rrbracket^{G^{\prime}}(a)=\llbracket r\rrbracket^{G^{\prime}}(b)=\emptyset$.
Therefore, $G,a\vDash\phi$, $G,b\vDash\phi$, $G^{\prime},a\vDash\phi$, and
$G^{\prime},b\vDash\phi$ always hold, showing 1 and 2.

Next, to show 3 where $r=p$, assume $G,c\vDash\mathit{disj}(E,p)$. By Lemma 9
we know there is a set of strings $U$ equivalent to $E$ in both $G$ and
$G^{\prime}$. By Lemma 26 there are only 10 types of strings. We observe from
Lemma 26 that for every $U$, $\bigcup_{s\in U}\llbracket s\rrbracket^{G}(c)$
is disjoint from $\llbracket p\rrbracket^{G}(c)$ whenever $U$ does not contain
strings of type 1, 2, or 7. These are also exactly the $U$ s.t. $\bigcup_{s\in
U}\llbracket s\rrbracket^{G^{\prime}}(c)$ is disjoint from $\llbracket
p\rrbracket^{G^{\prime}}(c)$.

Next, to show 3 where $r=q$, assume $G,c\vDash\mathit{disj}(E,q)$. We observe
from Lemma 26 that for every $U$, $\bigcup_{s\in U}\llbracket
s\rrbracket^{G}(c)$ is disjoint from $\llbracket q\rrbracket^{G}(c)$ whenever
$U$ does not contain strings of type 1, 2, or 7. These are also exactly the
$U$ s.t. $\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)$ is disjoint
from $\llbracket q\rrbracket^{G^{\prime}}(c)$.

For every other property name $r$, $\llbracket r\rrbracket^{G}(a)=\llbracket
r\rrbracket^{G}(b)=\emptyset$. Therefore, $G,c\vDash\phi$ and
$G^{\prime},c\vDash\phi$ always hold.

Finally, we show 4 by observing that for any $x\in N\setminus V$, $\llbracket
r\rrbracket^{G}(x)=\llbracket r\rrbracket^{G^{\prime}}(x)=\emptyset$.
Therefore, $G,x\vDash\phi$ and $G^{\prime},x\vDash\phi$ always hold.

Next, consider the case where $\phi$ is $eq(E_{1},E_{2})$. We again verify 1,
2, 3, and 4.

We show 1 by using a canonical labeling argument. For any two sets $U_{1}$ and
$U_{2}$ of types, we call $U_{1}$ and $U_{2}$ equivalent in $a\in A$ if
$\bigcup_{s\in U_{1}}\llbracket s\rrbracket^{G}(a)=\bigcup_{s\in
U_{2}}\llbracket s\rrbracket^{G}(a)$. Similarly, we define when $U_{1}$ and
$U_{2}$ are equivalent in $b$ or $c$.

We can canonically label the equivalence classes in $a$ as follows. Let
$U=\\{u_{1},\dots,u_{l}\\}$ and $u_{1}<\dots<u_{l}$ with each
$u_{i}\in\\{1,\dots,10\\}$ a type.

There are only six unique singleton sets namely $\\{1\\}$, $\\{3\\}$,
$\\{4\\}$, $\\{6\\}$, $\\{8\\}$, and $\\{9\\}$. Replace each $u_{i}$ by their
singleton representative $\overline{u_{i}}$. In
$\\{\overline{u_{1}},\dots,\overline{u_{l}}\\}$, reorder and remove duplicates
to obtain an equivalent set
$\\{u^{\prime}_{1},\dots,u^{\prime}_{l^{\prime}}\\}$.

If $l^{\prime}=1$, we are done. Otherwise, we enumerate all nonequivalent
2-element sets that are not equivalent to a singleton: there are again six of
those, namely $\\{3,6\\}$, $\\{3,9\\}$, $\\{4,6\\}$, $\\{4,9\\}$, $\\{6,8\\}$,
and $\\{8,9\\}$.

Replace $u^{\prime}_{1}$ and $u^{\prime}_{2}$ by either
$\\{u^{\prime\prime}\\}$ in case $\\{u^{\prime}_{1},u^{\prime}_{2}\\}$ is
equivalent to a singleton; otherwise replace $u^{\prime}_{1}$ and
$u^{\prime}_{2}$ by their equivalent 2-element set
$\\{u^{\prime\prime}_{1},u^{\prime\prime}_{2}\\}$. If $l^{\prime}=2$, we are
again done.

We can repeat this process. However, it turns out that there are no 3-element
sets that are not equivalent to a singleton or a 2-element set. Hence, there
are only 12 representatives. The enumeration process is shown in Table 3,
giving the representative for equivalence in $a$ as well as for equivalence in
$b$. Crucially, in filling the table, we observe every set $U$ has the same
representative for equivalence in $a$ as for equivalence in $b$.

Next, 2 is shown in an analogous manner, where the enumeration process is
again shown in Table 3.

Next, 3 is again shown with an analogous manner, where the enumeration process
is shown in Table 4.

To show 4, assume $x\not\in V$. If both $E_{1}$ and $E_{2}$ are safe, then by
Lemma 8 $\llbracket E_{1}\rrbracket^{G}(x)=\llbracket
E_{2}\rrbracket^{G^{\prime}}(x)=\emptyset$. Thus, $G,x\vDash\phi$ and
$G^{\prime},x\vDash\phi$. If both $E_{1}$ and $E_{2}$ are unsafe, then by
Lemma 8 $\llbracket E_{1}\rrbracket^{G}(x)=\llbracket
E_{2}\rrbracket^{G^{\prime}}(x)=\\{x\\}$. Thus, $G,x\vDash\phi$ and
$G^{\prime},x\vDash\phi$. However, whenever only one of $E_{1}$ and $E_{2}$ is
safe, clearly $G,x\not\vDash\phi$ and $G^{\prime},x\not\vDash\phi$.

The cases where $\phi$ is $\phi_{1}\land\phi_{2}$, $\phi_{1}\lor\phi_{2}$ or
$\neg\phi_{1}$ are handled by induction in a straightforward manner.

Lastly, we consider the case where $\phi$ is
$\mathop{\geq}\nolimits_{n}E.\psi$.

  1. 1

Assume $G,a\vDash\phi$. Then, there exist distinct $x_{1},\dots,x_{n}$ s.t.
$(a,x_{i})\in\llbracket E\rrbracket^{G}$ and $G,x_{i}\vDash\psi$ for $1\leq
i\leq n$. Again, by Lemma 9 we know there is a set of strings $U$ equivalent
to $E$ in both $G$ and $G^{\prime}$. By Lemma 26 there are only 10 types of
strings. By induction, we consider three cases.

First, if $\llbracket\psi\rrbracket^{G}\cap V=A\cup B$, then
$x_{i},\dots,x_{n}\in A\cup B$. Therefore, we know $U$ must at least contain
strings of type 6 or 9. Suppose $U$ contains strings of type 6. Then, we
verify that $\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G}(b)\cap(A\cup
B))\geq m\geq n$. Otherwise, whenever $U$ contains strings of type 9, and not
of type 6, we know $n=1$ and clearly $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G}(b)\cap(A\cup B))=1$.

Next, if $\llbracket\psi\rrbracket^{G}\cap V=C$, then $x_{i},\dots,x_{n}\in
C$. Therefore, we know $U$ must at least contain strings of type 3, 4 or 8.
Whenever $U$ contains 3, 4 or 8, we verify that $\sharp(\bigcup_{s\in
U}\llbracket s\rrbracket^{G}(b)\cap C)\geq\frac{m}{2}\geq n$.

Next, if $\llbracket\psi\rrbracket^{G}\cap V=V$, then $x_{i},\dots,x_{n}\in
V$. Therefore, we know $U$ must at least contain strings of type 3, 4, 6, 8 or
9. All these types have already been handled in the previous two cases.

Finally, the case where $\llbracket\psi\rrbracket^{G}\cap V=\emptyset$ cannot
occur as $n>0$.

The sets of strings $U$ above are also exactly the sets used to argue the
implication from right to left.

  2. 2

For every case of $U$ above, for every inductive case of $\psi$, we can also
verify that $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G^{\prime}}(a)\cap(A\cup B))\geq m\geq n$, $\sharp(\bigcup_{s\in
U}\llbracket s\rrbracket^{G^{\prime}}(a)\cap C)\geq\frac{m}{2}\geq n$, and
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(a)\cap
V)\geq\frac{m}{2}\geq n$.

  3. 3

Assume $G,c\vDash\phi$. Then, there exist distinct $x_{1},\dots,x_{n}$ s.t.
$(c,x_{i})\in\llbracket E\rrbracket^{G}$ and $G,x_{i}\vDash\psi$ for $1\leq
i\leq n$. By induction, we consider three cases.

First, if $\llbracket\psi\rrbracket^{G}\cap V=A\cup B$, then
$x_{i},\dots,x_{n}\in A\cup B$. Therefore, we know $U$ must at least contain
strings of type 1, 2 or 7. Whenever $U$ contains 1, 2 or 7, we verify that
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)\cap(A\cup
B))\geq\frac{m}{2}\geq n$.

Next, if $\llbracket\psi\rrbracket^{G}\cap V=C$, then $x_{i},\dots,x_{n}\in
C$. Therefore, we know $U$ must at least contain strings of type 5 or 9.
Whenever $U$ contains 5, we verify that $\sharp(\bigcup_{s\in U}\llbracket
s\rrbracket^{G^{\prime}}(c)\cap C)\geq m\geq n$. Otherwise, whenever $U$
contains strings of type 9, and not of type 5, we know $n=1$ and clearly
$\sharp(\bigcup_{s\in U}\llbracket s\rrbracket^{G^{\prime}}(c)\cap C)=1$.

Next, if $\llbracket\psi\rrbracket^{G}\cap V=V$, then $x_{i},\dots,x_{n}\in
V$. Therefore, we know $U$ must at least contain strings of type 1, 2, 5, 7 or
9. All these types have already been handled in the previous two cases.

Finally, the case where $\llbracket\psi\rrbracket^{G}\cap V=\emptyset$ cannot
occur as $n>0$.

The sets of strings $U$ above are also exactly the sets used to argue the
implication from right to left.

  4. 4

For the direction from left to right, take
$x\in\llbracket\phi\rrbracket^{G}\setminus V$. Since $G,x\vDash\phi$, there
exists $y_{1},\dots,y_{n}$ s.t. $(x,y_{i})\in\llbracket E\rrbracket^{G}$ and
$G,y_{i}\vDash\psi$ for $i=1,\dots,n$. However, since $x\not\in V$, by Lemma
8, all $y_{i}$ must equal $x$. Hence, $n=1$ and $(x,x)\in\llbracket
E\rrbracket^{G}$ and $G,x\vDash\psi$. Then again, by the same Lemma,
$(x,x)\in\llbracket E\rrbracket^{G^{\prime}}$, since $G$ and $G^{\prime}$ have
the same set of nodes $V$/ Moreover, by induction, $G^{\prime},x\vDash\psi$.
We conclude $G^{\prime},x\vDash\phi$ as desired. The direction from right to
left is argued symmetrically.

Table 3. Sets of types starting from $a_{i}$, $b_{i}$ in $G$ and $a_{i}$ in $G^{\prime}$. $U$ | $\llbracket E\rrbracket^{G}(a_{i})$ | $\llbracket E\rrbracket^{G}(b_{i})$ | $\llbracket E\rrbracket^{G^{\prime}}(a_{i})$
---|---|---|---
$\mathbf{\\{1\\}}$ | $\emptyset$ | $\emptyset$ | $\emptyset$
$\\{2\\}$ | $\emptyset$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{3\\}}$ | $c_{i-\frac{k}{2}+1\to i}$ | $c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$ | $c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$
$\mathbf{\\{4\\}}$ | $c_{i+1\to i+\frac{k}{2}}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$
$\\{5\\}$ | $\emptyset$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{6\\}}$ | $A\cup B$ | $A\cup B$ | $A\cup B$
$\\{7\\}$ | $\emptyset$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{8\\}}$ | $C$ | $C$ | $C$
$\mathbf{\\{9\\}}$ | $\\{a_{i}\\}$ | $\\{b_{i}\\}$ | $\\{a_{i}\\}$
$\\{10\\}$ | $\emptyset$ | $\emptyset$ | $\emptyset$
$\\{3,4\\}$ | $C$ | $C$ | $C$
$\mathbf{\\{3,6\\}}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$
$\\{3,8\\}$ | $C$ | $C$ |
$\mathbf{\\{3,9\\}}$ | $c_{i+1\to i+\frac{k}{2}}\cup\\{a_{i}\\}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}\cup\\{b_{i}\\}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}\cup\\{a_{i}\\}$
$\mathbf{\\{4,6\\}}$ | $A\cup B\cup c_{i+1\to i+\frac{k}{2}}$ | $A\cup B\cup c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$ | $A\cup B\cup c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$
$\\{4,8\\}$ | $C$ | $C$ |
$\mathbf{\\{4,9\\}}$ | $c_{i+1\to i+\frac{k}{2}}\cup\\{a_{i}\\}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}\cup\\{b_{i}\\}$ | $c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}\cup\\{a_{i}\\}$
$\mathbf{\\{6,8\\}}$ | $V$ | $V$ | $V$
$\\{6,9\\}$ | $A\cup B$ | $A\cup B$ | $A\cup B$
$\mathbf{\\{8,9\\}}$ | $C\cup\\{a_{i}\\}$ | $C\cup\\{b_{i}\\}$ | $C\cup\\{a_{i}\\}$
$\\{3,6,4\\}$ | $V$ | $V$ | $V$
$\\{3,6,8\\}$ | $V$ | $V$ | $V$
$\\{3,6,9\\}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$ | $A\cup B\cup c_{i-\frac{k}{2}+1\to i+\frac{k}{8}}$
$\\{3,9,4\\}$ | $C\cup\\{a_{i}\\}$ | $C\cup\\{b_{i}\\}$ | $C\cup\\{a_{i}\\}$
$\\{4,9,6\\}$ | $A\cup B\cup c_{i+1\to i+\frac{k}{2}}$ | $A\cup B\cup c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$ | $A\cup B\cup c_{i-\frac{k}{8}+1\to i+\frac{k}{2}}$
$\\{4,9,8\\}$ | $C$ | $C$ | $C$
$\\{8,9,3\\}$ | $C\cup\\{a_{i}\\}$ | $C\cup\\{b_{i}\\}$ | $C\cup\\{a_{i}\\}$
$\\{4,6,3\\}$ | $V$ | $V$ | $V$
Table 4. Sets of types starting from $c_{i}$ in $G$ and in $G^{\prime}$. $U$ | $\llbracket E\rrbracket^{G}(c_{i})$ | $\llbracket E\rrbracket^{G^{\prime}}(c_{i})$
---|---|---
$\mathbf{\\{1\\}}$ | $a_{i\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$ | $a_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$
$\mathbf{\\{2\\}}$ | $a_{i-\frac{m}{2}\to i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$ | $a_{i-\frac{m}{2}\to i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$
$\mathbf{\\{3\\}}$ | $\emptyset$ | $\emptyset$
$\\{4\\}$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{5\\}}$ | $C$ | $C$
$\\{6\\}$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{7\\}}$ | $A\cup B$ | $A\cup B$
$\\{8\\}$ | $\emptyset$ | $\emptyset$
$\mathbf{\\{9\\}}$ | $\\{c_{i}\\}$ | $\\{c_{i}\\}$
$\\{10\\}$ | $\emptyset$ | $\emptyset$
$\\{1,2\\}$ | $A\cup B$ | $A\cup B$
$\mathbf{\\{1,5\\}}$ | $C\cup a_{i\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$ | $C\cup a_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$
$\\{1,7\\}$ | $A\cup B$ | $A\cup B$
$\mathbf{\\{1,9\\}}$ | $\\{c_{i}\\}\cup a_{i\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$ | $\\{c_{i}\\}\cup a_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$
$\mathbf{\\{2,5\\}}$ | $C\cup a_{i-\frac{m}{2}\to i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$ | $C\cup a_{i-\frac{m}{2}\to i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$
$\\{2,7\\}$ | $A\cup B$ | $A\cup B$
$\mathbf{\\{2,9\\}}$ | $\\{c_{i}\\}\cup a_{i-\frac{m}{2}\to i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$ | $\\{c_{i}\\}\cup a_{i-\frac{m}{2}\to i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$
$\mathbf{\\{5,7\\}}$ | $V$ | $V$
$\\{5,9\\}$ | $C$ | $C$
$\mathbf{\\{7,9\\}}$ | $\\{c_{i}\\}\cup A\cup B$ | $\\{c_{i}\\}\cup A\cup B$
$\\{1,5,2\\}$ | $V$ | $V$
$\\{1,5,7\\}$ | $V$ | $V$
$\\{1,5,9\\}$ | $C\cup a_{i\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$ | $C\cup a_{i-\frac{m}{8}\to i+\frac{m}{2}-1}\cup b_{i-\frac{m}{8}\to i+\frac{m}{2}-1}$
$\\{1,9,2\\}$ | $\\{c_{i}\\}\cup A\cup B$ | $\\{c_{i}\\}\cup A\cup B$
$\\{1,9,7\\}$ | $\\{c_{i}\\}\cup A\cup B$ | $\\{c_{i}\\}\cup A\cup B$
$\\{2,5,7\\}$ | $V$ | $V$
$\\{2,5,9\\}$ | $C\cup a_{i-\frac{m}{2}\to i-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$ | $C\cup a_{i-\frac{m}{2}\to i+\frac{m}{8}-1}\cup b_{i-\frac{m}{2}\to i+\frac{m}{8}-1}$
$\\{2,9,7\\}$ | $\\{c_{i}\\}\cup A\cup B$ | $\\{c_{i}\\}\cup A\cup B$
$\\{5,7,9\\}$ | $V$ | $V$

######  Remark 28.

In our construction of the graphs $G$ and $G^{\prime}$, we work with segments
that overlap for $1/8$th of the number of nodes. The critical reader will
remark that an overlap of a single node would already be sufficient. Our
choice for working with a larger overlap is indeed largely aesthetic.
Moreover, our proof still works for an extension of SHACL where shapes of the
form $|r\cap E|\geq n$ would be allowed. This extension allows us to write
shapes like $|\textsf{colleague}\cap\textsf{friend}|\geq 5$, stating that the
node has at least five colleagues that are also friends. Such an extension
then would still not be able to express full disjointness.

###  5.3. Further non-definability results

In Theorem 5, we showed that equality is primitive in
$\mathcal{L}(\mathit{disj},\mathit{closed})$, and similarly, that disjointness
is primitive in $\mathcal{L}(\mathit{eq},\mathit{closed})$. Can we strengthen
these results to $\mathcal{L}(\mathit{full\text{-}disj},\mathit{closed})$ and
$\mathcal{L}(\mathit{full\text{-}eq},\mathit{closed})$, respectively? This
turns out to be indeed possible.

That equality remains primitive in
$\mathcal{L}(\mathit{full\text{-}disj},\mathit{closed})$ already follows from
our given proof in Section 3.3. In effect, the attentive reader may have
noticed that we already cover full disjointness in that proof. In contrast,
our proof of primitivity of disjointness in
$\mathcal{L}(\mathit{eq},\mathit{closed})$ does not extend to full equality.
Nevertheless, we can reuse our proof of primitivity of _full_ disjointness as
follows. The graphs $G$ and $G^{\prime}$ from Proposition 27 are
indistinguishable in
$\mathcal{L}(\mathit{full\text{-}eq},\mathit{disj},\mathit{closed})$. Let $H$
and $H^{\prime}$ be the same graphs but with all directed edges reversed
(i.e., the graphs illustrated in Figure 4). Then the same proof shows that $H$
and $H^{\prime}$ are indistinguishable in
$\mathcal{L}(\mathit{full\text{-}eq},\mathit{closed})$. However, since $G$ and
$G^{\prime}$ are distinguishable by the inclusion statement $\exists
p^{-}.\top\subseteq\neg\mathit{disj}(p^{-},q^{-})$, also $H$ and $H^{\prime}$
are distinguishable by the inclusion statement $\exists
p.\top\subseteq\neg\mathit{disj}(p,q)$. Thus, the primitivity of disjointness
in $\mathcal{L}(\mathit{full\text{-}eq},\mathit{closed})$ is established.

##  6\. Extension to stratified recursion

Until now, we could do without shape names. We do need them, however, for
recursive shape schemas. Such schemas allow shapes to be defined using
recursive rules, much as in Datalog and logic programming. The rules have a
shape name in the head; in the body they have a shape that can refer to the
same or other shape names.

The following rule defines a shape, named $s$, recursively:

$s\leftarrow\\{c\\}\lor(\mathit{eq}(p,q)\land\exists r.s).$

A node $x$ will satisfy $s$ if there is a (possibly empty) path of $r$-edges
from $x$ to the constant $c$, so that all nodes along the path satisfy
$\mathit{eq}(p,q)$ (for two property names $p$ and $q$).

#### Rules and programs

We need to make a few extensions to our formalism and the semantics.

  * •

We assume an infinite supply $S$ of _shape names_. Again for simplicity of
notation only, we assume that $S$ is disjoint from $N$ and $P$.

  * •

The syntax of shapes is extended so that _every shape name is a shape_.

  * •

A vocabulary $\Sigma$ is now a subset of $N\cup P\cup S$; an interpretation
$I$ now additionally assigns a subset $\llbracket s\rrbracket^{I}$ of
$\Delta^{I}$ to every shape name $s$ in $\Sigma$.

Noting the obvious parallels with the field of logic programming, we propose
to use the following terminology from that field. A _rule_ is of the form
$s\leftarrow\phi$, where $s$ is a shape name and $\phi$ is a shape. A
_program_ is a finite set of rules. The shape names appearing as heads of
rules in a program are called the _intensional_ shape names of that program.

The following definitions of the semantics of programs are similar to
definitions well-known for Datalog. A program is _semipositive_ if for every
intensional shape name $s$, and every shape $\phi$ in the body of some rule,
$s$ occurs only positively in $\phi$. Let $\mathcal{P}$ be a semipositive
program over vocabulary $\Sigma$, with set of intensional shape names $D$. An
interpretation $J$ over $\Sigma\cup D$ is called a _model_ of $\mathcal{P}$ if
for every rule $s\leftarrow\phi$ of $\mathcal{P}$, the set
$\llbracket\phi\rrbracket^{J}$ is a subset of $\llbracket s\rrbracket^{J}$.
Given any interpretation $I$ over $\Sigma-D$, there exists a unique minimal
interpretation $J$ that expands $I$ to $\Sigma\cup D$ such that $J$ is a model
of $\mathcal{P}$ (Indeed, $J$ is the least fixpoint of the well-known
immediate consequence operator, which is a monotone operator since
$\mathcal{P}$ is semipositive [AHV95]). We call $J$ the result of applying
$\mathcal{P}$ to $I$, and denote $J$ by $\mathcal{P}(I)$.

Stratified programs are essentially sequences of semipositive programs.
Formally, a program $\mathcal{P}$ is called _stratified_ if it can be
partitioned into parts $\mathcal{P}_{1}$, …, $\mathcal{P}_{n}$ called _strata_
, such that (i) the strata have pairwise disjoint sets of intensional shape
names; (ii) each stratum is semipositive; and (iii) the strata are ordered in
such a way that when a shape name $s$ occurs in the body of a rule in some
stratum, $s$ is not intensional in any later stratum.

Let $\mathcal{P}$ be a stratified program with $n$ strata $\mathcal{P}_{1}$,
…, $\mathcal{P}_{n}$ and let again $I$ be an interpretation over a vocabulary
without the intensional shape names. We define $\mathcal{P}(I)$, the result of
applying $\mathcal{P}$ to $I$, to be the interpretation $J_{n}$, where
$J_{0}:=I$ and $J_{k+1}:=\mathcal{P}_{k+1}(J_{k})$ for $0\leq k<n$.

#### Stratified shape schemas

We are now ready to define a _stratified shape schema_ again as a set of
inclusions, but now paired with a stratified program. Formally, it is a pair
$(\mathcal{P},\mathcal{T})$, where:

  * •

$\mathcal{P}$ is a program that is stratified, and where every shape name
mentioned in the body of some rule is an intensional shape name in
$\mathcal{P}$.

  * •

$\mathcal{T}$ is a finite set of inclusion statements
$\phi_{1}\subseteq\phi_{2}$, where $\phi_{1}$ and $\phi_{2}$ mention only
shape names that are intensional in $\mathcal{P}$.

Now we define a graph $G$ to _conform_ to $(\mathcal{P},\mathcal{T})$ if
$\llbracket\phi_{1}\rrbracket^{\mathcal{P}(G)}$ is a subset of
$\llbracket\phi_{2}\rrbracket^{\mathcal{P}(G)}$, for every inclusion
$\phi_{1}\subseteq\phi_{2}$ in $\mathcal{T}$.

######  Remark 29.

The nonrecursive notion of shape schema, defined in Section 2, corresponds to
the special case where $\mathcal{P}$ is the empty program.

#### Extending Theorem 5

Theorem 5 extends to stratified shape schemas. Indeed, consider a stratified
shape schema $(\mathcal{P},\mathcal{T})$. Shapes not mentioning any shape
names are referred to as _elementary shapes_. We observe that for every
intensional shape name $s$ and every graph $H$, there exists an elementary
shape $\phi$ such that $\llbracket
s\rrbracket^{\mathcal{P}(H)}=\llbracket\phi\rrbracket^{H}$. Furthermore,
$\phi$ uses the same constants, quantifiers, and path expressions as
$\mathcal{P}$. For semipositive programs, this is shown using a fixpoint
characterization of the minimal model; for stratified programs, this argument
can then be applied repeatedly. The crux, however, is that graphs $G$ and
$G^{\prime}$ of Proposition 6 will have the same $\phi$. Indeed, by that
Proposition, the fixpoints of the different strata will be reached on $G$ and
on $G^{\prime}$ in the same stage. We effectively obtain an extension of
Proposition 6, which establishes the theorem for features $X$ other than
$\mathit{closed}$.

Also for $X=\mathit{closed}$, the reasoning, given after Lemma 15, extends in
the same way to stratified shape schemas, since the graphs $G$ and
$G^{\prime}$ used there again yield exactly the same evaluation for all shapes
that do not use $\mathit{closed}$.

#### Extending Theorem 18

Also Theorem 18 extends to stratified shape schemas. Thereto, Lemma 15 needs
to be reproven in the presence of a stratified program $\mathcal{P}$ defining
the intensional shape names. The extended Lemma 15 then states that
$\llbracket\phi\rrbracket^{\mathcal{P}(G)}=\llbracket\phi\rrbracket^{\mathcal{P}(G^{\prime})}$.
The proof of Theorem 18 then goes through unchanged.

#### Extending Theorem 23

Also Theorem 23 extends to stratified shape schemas for the same reasons given
above for Theorem 5.

##  7\. Concluding remarks

An obvious open question is whether our results extend further to
nonstratified programs, depending on various semantics that have been proposed
for Datalog with negation, notably well-founded or stable models [AHV95,
Tru18]. One must then deal with 3-valued models and, for stable models, choose
whether the TBox should hold in every stable model (skeptical), or in at least
one (credulous). For example, Andreşel et al. [ACO+20] adopt a credulous
approach. In the same vein, even for stratified programs, one may consider
_maximal_ models instead of minimal ones, as suggested for ShEx [BGP17].
Unified approaches developed for logic programming semantics can be naturally
applied to SHACL [BJ21].

Notably, Corman et al. [CRS18] have already suggested that disjointness is
redundant in a setting of recursive shape schemas with nonstratified negation.
Their expression is not correct, however [Reu21].555Their approach is to
postulate two shape names $s_{1}$ and $s_{2}$ that can be assigned arbitrary
sets of nodes, as long as the two sets form a partition of the domain. Then
for one node $x$ to satisfy the shape $\mathit{disj}(E,p)$, it is sufficient
that $E(x)$ is a subset of $s_{1}$ and $p(x)$ of $s_{2}$. This condition is
not necessary, however, as other nodes may require different partitions.

A general question surrounding SHACL, even standard nonrecursive SHACL, is to
understand better in which sense (if at all) this language is actually better
suited for expressing constraints on RDF graphs than, say, SPARQL ASK queries
[CFRS19, T+10, DMH+21]. Certainly, the affinity with description logics makes
it easy to carve out cases where higher reasoning tasks become decidable
[LS+20, PK+20]. It is also possible to show that nonrecursive SHACL is
strictly weaker in expressive power than SPARQL. But does SHACL conformance
checking really have a lower computational complexity? Can we think of novel
query processing strategies that apply to SHACL but not easily to SPARQL? Are
SHACL expressions typically shorter, or perhaps longer, than the equivalent
SPARQL ASK expression? How do the expression complexities [Var82] compare?

## Acknowledgement

We thank the anonymous referees for helpful comments that improved the
presentation of this paper. This research was supported by the Flanders AI
Research programme.

## References

  * [ACO+20] M. Andreşel, J. Corman, M. Ortiz, J.L. Reutter, O. Savkovic, and M. Simkus.  Stable model semantics for recursive SHACL.  In Y. Huang, I. King, T.-Y. Liu, and M. van Steen, editors, Proceedings WWW’20, pages 1570–1580. ACM, 2020.
  * [AGSS86] A.K. Aylamazyan, M.M. Gilula, A.P. Stolboushkin, and G.F. Schwartz.  Reduction of the relational model with infinite domains to the case of finite domains.  Doklady Akademii Nauk SSSR, 286(2):308–311, 1986.  In Russian.
  * [AHV95] S. Abiteboul, R. Hull, and V. Vianu.  Foundations of Databases.  Addison-Wesley, 1995.
  * [BGP17] I. Boneva, J.E.L. Gayo, and E.G. Prud’hommeaux.  Semantics and validation of shape schemas for RDF.  In C. d’Amato, M. Fernandez, V. Tamma, et al., editors, Proceedings 16th International Semantic Web Conference, volume 10587 of Lecture Notes in Computer Science, pages 104–120. Springer, 2017.
  * [BHLS17] F. Baader, I. Horrocks, C. Lutz, and U. Sattler.  An Introduction to Description Logic.  Cambridge University Press, 2017.
  * [BJ21] B. Bogaerts and M. Jakubowski.  Fixpoint semantics for recursive SHACL.  In Proceedings 37th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2021, Porto (virtual event), 20-27th September 2021, volume 345, pages 41–47, 2021\.  doi:10.4204/EPTCS.345.14.
  * [BJVdB22] B. Bogaerts, M. Jakubowski, and J. Van den Bussche.  Expressiveness of SHACL features.  In Dan Olteanu and Nils Vortmeier, editors, Proceedings of ICDT, volume 220, pages 15:1–15:16. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2022.
  * [CDGNL03] D. Calvanese, G. De Giacomo, D. Nardi, and M. Lenzerini.  Reasoning in expressive description logics.  In F. Baader, D. Calvanese, D. McGuiness, D. Nardi, and P. Patel-Schneider, editors, The Description Logic Handbook, chapter 23. Cambridge University Press, 2003.
  * [CFRS19] J. Corman, F. Florenzano, J.L. Reutter, and O. Savkovic.  Validating SHACL constraints over a SPARQL endpoint.  In C. Ghidini, O. Hartig, M. Maleshkova, V. Svátek, et al., editors, Proceedings 18th International Semantic Web Conference, volume 11778 of Lecture Notes in Computer Science, pages 145–163. Springer, 2019\.
  * [CRS18] J. Corman, J.L. Reutter, and O. Savkovic.  Semantics and validation of recursive SHACL.  In D. Vrandecic et al., editors, Proceedings 17th International Semantic Web Conference, volume 11136 of Lecture Notes in Computer Science, pages 318–336. Springer, 2018.  Extended version, technical report KRDB18-01, https://www.inf.unibz.it/krdb/tech-reports/.
  * [DMH+21] B. De Meester, P. Heyvaert, et al.  RDF graph validation using rule-based reasoning.  Semantic Web, 12(1):117–142, 2021.
  * [HS94] R. Hull and J. Su.  Domain independence and the relational calculus.  Acta Informatica, 31:513–524, 1994.
  * [Jak22] M. Jakubowski.  Extending SHACL, 2022.  URL: https://www.mjakubowski.info/posts/datashapes.html.
  * [Knu21] H. Knublauch.  Dash constraint components.  https://datashapes.org/constraints.html, 2021.
  * [LS+20] M. Leinberger, P. Seifer, et al.  Deciding SHACL shape containment through description logics reasoning.  In Pan et al. [P+20], pages 366–383.
  * [P+20] J.Z. Pan et al., editors.  Proceedings 19th International Semantic Web Conference, volume 12506 of Lecture Notes in Computer Science. Springer, 2020.
  * [PK+20] P. Pareti, G. Konstantinidis, et al.  SHACL satisfiability and containment.  In Pan et al. [P+20], pages 474–493.
  * [RDF14] RDF 1.1 primer.  W3C Working Group Note, June 2014.
  * [Reu21] J. Reutter.  Personal communication, 15 January 2021.
  * [SHA17] Shapes constraint language (SHACL).  W3C Recommendation, July 2017.
  * [T+10] J. Tao et al.  Integrity constraints in OWL.  In Proceedings 24th AAAI Conference on Artificial Intelligence, pages 1443–1448, 2010.
  * [Tru18] M. Truszczynski.  An introduction to the stable and well-founded semantics of logic programs.  In M. Kifer and Y.A. Liu, editors, Declarative Logic Programming: Theory, Systems, and Applications, pages 121–177. ACM and Morgan & Claypool, 2018.
  * [Var82] M. Vardi.  The complexity of relational query languages.  In Proceedings 14th ACM Symposium on the Theory of Computing, pages 137–146, 1982.

##  Appendix A Supplementary Proofs

### Proof of Lemma 9

We first state an auxiliary lemma:

######  Lemma 30.

Let $V$ be a finite set of $n$ elements, and let $R\subseteq V\times V$ be a
binary relation over $V$. We have $R^{*}=R^{0}\cup R^{1}\cup\dots\cup
R^{n-1}$.

######  Proof A.1.

$R^{*}$ is defined as $R^{0}\cup R^{1}\cup\dots$ however, we will show that if
$(a,b)\in R^{m}$, with $m\geq n$, then there exists a $k<m$ such that
$(a,b)\in R^{k}$.

We call a sequence of elements $x_{1},\dots,x_{h}$ an $R$-path if
$(x_{l},x_{l+1})\in R$ for $1\leq l\leq h$.

If $(a,b)\in R^{m}$, then there exists an $R$-path $x_{1},\dots,x_{m+1}$ with
$x_{1}=a$ and $x_{m+1}=b$. As there are only $n$ total elements, there exists
$i,j$ with $1\leq i<j\leq m+1$ such that $x_{i}=x_{j}$. Therefore,
$x_{1},\dots,x_{i-1},x_{j},\dots,x_{m+1}$ is also an $R$-path. We conclude
that $(a,b)\in R^{m-(j-i)}$, as desired.

######  Proof A.2 (Proof of Lemma 9.).

The proof is by induction on the structure of $E$. Clearly for the base case
$E=p$, we have the set $U=\\{p\\}$ and similarly for $E=p^{-}$ we have
$U=\\{p^{-}\\}$. When $E=\mathit{id}$, clearly $U=\\{\mathit{id}\\}$. Next, we
consider the inductive cases. When $E=E_{1}\cup E_{2}$, we know by induction
there exists a set of strings $U_{1}$ for $E_{1}$, and $U_{2}$ for $E_{2}$. We
then have $U=U_{1}\cup U_{2}$. When $E=E_{1}/E_{2}$, we again know by
induction there exists a set of strings $U_{1}$ for $E_{1}$, and $U_{2}$ for
$E_{2}$. We have $U=\\{s_{1}/s_{2}\mid s_{1}\in U_{1}\;\text{and}\;s_{2}\in
U_{2}\\}$. Finally, when $E=E^{\prime*}$, we know by induction there exists a
set of strings $U^{\prime}$ for $E^{\prime}$. Let $W$ be a set of strings, we
define $W^{1}:=W$, and for a natural number $m>1$, $W^{m}:=\\{s_{1}/s_{2}\mid
s_{1}\in W,s_{2}\in W^{m-1}\\}$. We also use the shorthand notation $E^{m}$,
with $m>0$ a natural number, to denote $m$ compositions of the path expression
$E$. For example, $E^{3}$ is $E/E/E$. By definition, $\llbracket
E^{\prime*}\rrbracket^{G}=\llbracket\mathit{id}\rrbracket^{G}\cup\llbracket
E^{\prime}\rrbracket^{G}\cup\llbracket E^{\prime 2}\rrbracket^{G}\cup\dots$.
By Lemma 30 we know that this is the same as $\llbracket
E^{\prime*}\rrbracket^{G}=\llbracket\mathit{id}\rrbracket^{G}\cup\llbracket
E^{\prime}\rrbracket^{G}\cup\llbracket E^{\prime
2}\rrbracket^{G}\cup\dots\cup\llbracket E^{\prime n-1}\rrbracket^{G}$ for
graphs with at most $n$ nodes. It then follows that $U=\\{\mathit{id}\\}\cup
U^{\prime}\cup U^{\prime 2}\cup\dots\cup U^{\prime n-1}$.

### Proof of Lemma 11

######  Proof A.3.

For $i=1,2,3,4$, define the _i-th blob of nodes_ to be the set
$X_{i}=\\{x_{i}^{1},\dots,x_{i}^{M}\\}$ (see Figure 2). We also use the
notations $\mathit{next}(1)=2$; $\mathit{next}(2)=3$; $\mathit{next}(3)=4$;
$\mathit{next}(4)=1$; $\mathit{prev}(4)=3$; $\mathit{prev}(3)=2$;
$\mathit{prev}(2)=1$; $\mathit{prev}(1)=4$. Thus $\mathit{next}(i)$ indicates
the next blob in the cycle, and $\mathit{prev}(i)$ the previous.

The proof is by induction on the structure of $E$. If $E$ is a property name,
$E$ is simple so the claim is trivial. If $E$ is of the form $p^{-}$, the
first claim is clear because $\llbracket
r^{-}\rrbracket^{G^{\prime}}\subseteq\llbracket E\rrbracket^{G^{\prime}}$, and
we only need to verify the second one. That holds because for any $i$, if
$v\in X_{i}$, then $\llbracket p^{-}\rrbracket^{G^{\prime}}(v)\supseteq
X_{\mathit{prev}(i)}$ and clearly $X_{\mathit{prev}(i)}-\llbracket
r\rrbracket^{G^{\prime}}(v)\neq\emptyset$. We next consider the inductive
cases.

First, assume $E$ is of the form $E_{1}\cup E_{2}$. When at least one of
$E_{1}$ and $E_{2}$ is not simple, the two claims immediately follow by
induction, since $\llbracket E\rrbracket^{G^{\prime}}\supseteq\llbracket
E_{1}\rrbracket^{G^{\prime}}$ and $\llbracket
E\rrbracket^{G^{\prime}}\supseteq\llbracket E_{2}\rrbracket^{G^{\prime}}$. If
$E_{1}$ and $E_{2}$ are simple, then $E$ is simple and the claim is trivial.

Next, assume $E$ is of the form $E_{1}^{*}$. If $E_{1}$ is not simple, the two
claims follow immediately by induction, since $\llbracket
E\rrbracket^{G^{\prime}}\supseteq\llbracket E_{1}\rrbracket^{G^{\prime}}$. If