Common Foundations for Recursive Shape Languages Shqiponja Ahmetaj1, Iovka Boneva2, Jan Hidders3, Maxime Jakubowski1, Jose-Emilio Labra-Gayo4, Wim Martens5, Fabio Mogavero6, Filip Murlak7, Cem Okulmus8, Ognjen Savković9, Mantas Šimkus1, Dominik Tomaszuk10 1 TU Wien, Austria 2 Univ. Lille, F-59000 Lille, France 3 Birkbeck, University of London, UK 4 University of Oviedo, Spain 5 University of Bayreuth, Germany 6 Universita di Napoli Federico II, Italy 7 University of Warsaw, Poland 8 Paderborn University, Germany 9 Free University of Bolzano, Italy 10 University of Białystok, Poland Abstract As schema languages for RDF data become more mature, we are seeing efforts to extend them with recursive semantics, applying diverse ideas from logic programming and description logics. While ShEx has an official recursive semantics based on greatest fixpoints (GFP), the discussion for SHACL is ongoing and seems to be converging towards least fixpoints (LFP). A practical study we perform shows that, indeed, ShEx validators implement GFP, whereas SHACL validators are more heterogeneous. This situation creates tension between ShEx and SHACL, as their semantic commitments appear to diverge, potentially undermining interoperability and predictability. We aim to clarify this design space by comparing the main semantic options in a principled yet accessible way, hoping to engage both theoreticians and practitioners, especially those involved in developing tools and standards. We present a unifying formal semantics that treats LFP, GFP, and supported model semantics (SMS), clarifying their relationships and highlighting a duality between LFP and GFP on stratified fragments. Next, we investigate to which extent the directions taken by SHACL and ShEx are compatible. We show that, although ShEx and SHACL seem to be going in different directions, they include large fragments with identical expressive power. Moreover, there is a strong correspondence between these fragments through the aforementioned principle of duality. Finally, we present a complete picture of the data and combined complexity of ShEx and SHACL validation under LFP, GFP, and SMS, showing that SMS comes at a higher computational cost under standard complexity-theoretic assumptions.
1
Introduction
Graph-based data representations are rapidly gaining importance due to the unprecedented growth of interconnected data and their increasing role in AI-driven systems (Sakr et al. 2021). Furthermore, their flexibility makes them an ideal tool for bridging the gap between structured data and machine learning tools in industrial applications (Anuradha et al. 2023; Mohamed et al. 2022). Since automatic processing of data (graph or otherwise) is significantly facilitated by the presence of a schema, we have seen various efforts to design schema languages for graph-based data representations, notably ShEx (Prud’hommeaux, Labra Gayo, and Solbrig 2014; Staworko et al. 2015; Prud’hommeaux et al. 2019), SHACL (Knublauch and Kontokostas 2017), and PGSchema (Angles et al. 2021; Angles et al. 2023). In this paper,
we zoom in on recursion as a foundational mechanism that directly shapes the semantics of cyclic schema dependencies. We therefore focus on ShEx and SHACL, the de facto standard schema languages for RDF, since PG-Schema does not use this kind of recursion. It is well-known that designing declarative languages with recursion and negation is non-trivial (Abiteboul, Hull, and Vianu 1995; Aref et al. 2025). SHACL and ShEx’s openworld nature (contrasting the typical database setting) does not make this task any easier. This might explain why the design of recursion is taking different directions in ShEx and SHACL. While ShEx has long had an official semantics based on greatest fixpoints (GFP) (Prud’hommeaux et al. 2019; Staworko et al. 2015; Boneva, Labra Gayo, and Prud’hommeaux 2017), the discussion for SHACL is ongoing. Proposals include a supported-model semantics (SMS) (Corman, Reutter, and Savković 2018), grounded in first-order logic, as well as alternatives inspired by fixpoint and logic-programming paradigms (Andresel et al. 2020; Okulmus and Šimkus 2024; Bogaerts and Jakubowski 2021; Ahmetaj et al. 2022b; Pareti, Konstantinidis, and Mogavero 2022). The academic discussion appears to be converging towards least fixpoints (LFP), but the issue remains to be addressed by the W3C working group.1 Our Contributions. (1) We shed light on this matter by proposing a unifying formal framework that is compatible with the work of Ahmetaj et al. (Ahmetaj et al. 2025). We define a simple shape language (SSL) with the three main options for recursion: LFP, GFP, and SMS (Section 2). The language SSL is carefully designed to be much simpler than ShEx and SHACL, yet sufficiently powerful to illustrate the fundamental tradeoffs between LFP, GFP, and SMS, and to test which semantics is used by validation engines. Despite its simplicity, it is still expressive: it corresponds to the alternation-free fragment of the modal µ-calculus (Kozen 1983) with nominals but without atomic propositions, which is an important yardstick. Using the duality principle of fixpoint theory, we observe that SSL with LFP is equally expressive as SSL with GFP, using a straightforward translation. This close relationship is good news for the compatibility between ShEx with GFP and SHACL with LFP. The 1
The W3C group charter explicitly states: “It should fix some unfinished issues in SHACL 1.0, such as recursion.” https://w3c. github.io/charter-drafts/2024/data-shapes
situation for SMS differs, see (4). (2) We experimentally explore whether existing SHACL and ShEx validators use LFP, GFP, or SMS (Section 3). Our tests reveal that current tools implicitly commit to different semantics, which leads to non-uniform behaviour across implementations. In a nutshell, ShEx validators seem to implement GFP, whereas SHACL validators are more heterogeneous. Once a semantics for recursion in SHACL is agreed upon, our tests can be added to the official test suite (Labra Gayo, Knublauch, and Kontokostas 2024). (3) We then move to the formal study of real schema languages. Though neat and relatively expressive, SSL is still a small part of real ShEx and SHACL. In Sections 4.1–4.2 (and accompanying appendices), we show translations between large fragments of ShEx (with GFP) and SHACL with LFP. Our translations show that these larger fragments have the same expressiveness and that the duality principle that we saw for SSL extends to real-world languages. (4) We provide a complete overview of the data and combined complexity of ShEx, SHACL, and SSL with LFP, GFP, and SMS (Section 4.3). In some cases the complexity has been known already (Andresel et al. 2020; Staworko et al. 2015; Bogaerts, Jakubowski, and Van den Bussche 2024; Bogaerts and Jakubowski 2021); we complete the picture by establishing tight bounds for the combined and data complexity for ShEx. The main conclusion from the complete set of results is that LFP and GFP allow polynomial-time data complexity for all languages, whereas SMS immediately leads to intractability, even for very simple languages like SSL. This means that LFP and GFP are much easier to deal with from an algorithmic perspective, and would be our recommendation for recursion in ShEx and/or SHACL. (5) As a group of authors including contributors to the design of both ShEx and SHACL, we reach a common understanding of the consequences of the choice of the semantics for recursion, and clarify that it is fine for SHACL to use LFP, while ShEx uses GFP. Full proofs can be found in the appendix. Related Work. The development of constraint languages for graph-based data has a rich history. SHACL (Knublauch and Kontokostas 2017) was designed taking the initial inspiration from SPIN Rules2 , whereas ShEx (Prud’hommeaux, Labra Gayo, and Solbrig 2014) draws more heavily on paradigms established in XML Schema and RELAX NG (Gao et al. 2012; Bray et al. 2008; Martens et al. 2017). Both languages aim to enable prescriptive validation of RDF, in contrast to the more descriptive nature of languages such as OWL (W3C OWL Working Group 2012). Nevertheless, they diverge in several key features, which poses challenges for tool interoperability and for users seeking to transition between the two frameworks. In our prior work (Ahmetaj et al. 2025), we take initial steps toward reconciling these differences by proposing a common framework for ShEx, SHACL, and PG-Schema, which was developed to provide similar schema capabilities in the context of the recent GQL standard (International Organization for Standardization 2024). The present work builds directly on that foundation, with a particular focus on recursion, a feature explicitly excluded 2
https://spinrdf.org/
from the earlier study. Before this, expressiveness and computational properties of (non-recursive) SHACL have been extensively studied (Bogaerts, Jakubowski, and den Bussche 2022; Bogaerts, Jakubowski, and Van den Bussche 2024; Pareti et al. 2020; Pareti, Konstantinidis, and Mogavero 2022). Similarly, the foundations of ShEx, including its formal semantics and complexity, have been explored in depth (Staworko et al. 2015; Boneva, Labra Gayo, and Prud’hommeaux 2017). Recursion in Shape Languages. The semantic challenges of recursion for shape languages, and particularly its interaction with negation, have been a significant topic of recent research. This is especially pronounced for SHACL, where the W3C recommendation (Knublauch and Kontokostas 2017) notably left the semantics of recursion undefined. The challenges of recursion were first formally addressed by Corman et al. (Corman, Reutter, and Savković 2018; Corman et al. 2019), who proposed a supported model semantics based on first-order logic. Subsequent work has explored various semantics mirroring established paradigms from fixpoint logics and logic programming (Andresel et al. 2020; Okulmus and Šimkus 2024; Bogaerts and Jakubowski 2021; Ahmetaj et al. 2022b; Pareti, Konstantinidis, and Mogavero 2022). In contrast to SHACL, the semantics of recursion in ShEx has been consistently defined via greatest fixpoints (Boneva, Labra Gayo, and Prud’hommeaux 2017; Staworko et al. 2015). This divergence in the formalization process lead to significant inconsistencies across validators. Validation in Practice. There is a growing body of work on the practical use of shape languages. This includes mining shapes from large knowledge graphs (Rabbani, Lissandrini, and Hose 2023; Lissandrini, Rabbani, and Hose 2024), validating real-world datasets such as Wikidata (Ferranti et al. 2024), and studying data provenance and explanations for validation outcomes (Delva et al. 2023; Ahmetaj et al. 2022a). The need to validate heterogeneous graph data has also motivated comparative studies of SHACL and ShEx (Labra Gayo et al. 2017; Labra Gayo et al. 2019; Tomaszuk 2017) as well as mappings between RDF and Property Graph paradigms (Angles, Thakkar, and Tomaszuk 2020; Hartig 2014). Further extensions of ShEx for different graph types have been proposed (Labra Gayo 2024; Labra Gayo 2022), alongside unifying graph data models such as OneGraph (Lassila and others 2023) and MillenniumDB’s Domain Graph Model (Vrgoč et al. 2023). Semantic ambiguities in recursive SHACL directly affect these practical efforts, since the outcome of validation can depend on the choice of validator and its implicit semantics. Connections to Description Logics and µ-calculus. Foundational work on SHACL has revealed strong connections to expressive Description Logics (DLs), the logics underlying OWL (Bogaerts, Jakubowski, and den Bussche 2022; Leinberger et al. 2020; Ahmetaj et al. 2021). The problem of defining coherent semantics for recursive shape languages closely parallels the classic issue of terminological cycles in DLs, extensively studied in the early 1990s. Terminologies with recursive definitions, where concept names may be defined directly or indirectly in terms of themselves, were recognized to require special semantic treatment to ensure meaningful interpretations. Initial studies (Baader 1990;
Baader 1996; Nebel 1991) identified three main approaches to interpreting such cycles: least fixpoint, greatest fixpoint, and descriptive (classical) semantics. It was observed that, for many cyclic definitions, the greatest-fixpoint semantics yields more satisfactory results by allowing maximal solutions consistent with their intended meaning, whereas for others, the least-fixpoint semantics is more suitable (Baader 1996; Giacomo and Lenzerini 1994). Further work argued that, instead of selecting a single semantics, better results are obtained by adopting a formalism that allows for the different semantics to coexist, where the correspondence with the modal µ-calculus was also established (Schild 1994; Giacomo and Lenzerini 1994). In our setting, we show that expressive yet tractable fragments of recursive SHACL and ShEx correspond to the alternation-free fragment of the modal µ-calculus (Kozen 1983).
Table 1: Semantics of shapes.
φ′ ⊥ ⊤ test(c) s ¬φ φ1 ∨ φ2 φ1 ∧ φ2 ∃p.φ ∀p.φ
The Multiple Semantics of Recursion
We now introduce the simple shape language, which is a core of both ShEx and SHACL, and formally define the three main modes of recursion that are being considered.
2.1
The RDF Data Model
An RDF graph is a finite set of triples in (IRIs ∪ Blanks) × (IRIs) × (IRIs ∪ Blanks ∪ Literals), where IRIs, Literals and Blanks are three countable sets of IRIs, literal data values, and blank nodes, respectively. If (u, p, v) is a triple of an RDF graph, then u is called its subject, p its predicate, and v its object. The set of nodes of an RDF graph G, denoted Nodes(G), is the set of IRIs, literals or blank nodes that appear in a subject or an object position in some triple of G. We sometimes use predicates to refer to the elements of IRIs when they are used in a predicate position of some triple. To illustrate, consider the RDF graph G: (ex:Alice, ex:knows, ex:Bob), G= . (ex:Bob, ex:age, 42) Here ex:Alice and ex:Bob are IRIs used as nodes, ex:knows and ex:age are IRIs used as predicates, and 42 is a literal value. In this case Nodes(G) = {ex:Alice, ex:Bob, 42}.
2.2
A Simple Shape Language
Consider a countable set Names of shape names. A shape φ is defined by the following syntax, where s ∈ Names is a shape name, p ∈ IRIs is a predicate, and c ∈ IRIs ∪ Literals is a constant. φ ::= ⊥ ⊤ test(c) s ¬φ φ ∨ φ φ ∧ φ ∃p.φ ∀p.φ . A simple shape language catalogue or SSL catalogue C is a partial function mapping shape names to shapes such that dom(C) is finite. We say that the shape name s is declared in C if C(s) is defined; that is, s ∈ dom(C). We require that every shape name that appears in a shape in (the range of) C is also declared in C. For convenience, we usually view C as the set of shape declarations of the form s : φ such that C(s) = φ. By Const(C) we denote the set of constants c such that test(c) appears in some shape in C.
∅ Nodes(G) ∪ Const(C) {c} α(s) (Nodes(G) ∪ Const(C)) \ JφKα G,C α Jφ1 Kα G,C ∪ Jφ2 KG,C α Jφ1 Kα G,C ∩ Jφ2 KG,C α G,C u for some (u, p, v) ∈ G, v ∈ JφK α u for all (u, p, v) ∈ G, v ∈ JφKG,C
p a
2
Jφ′ Kα G,C
q b
p
”d”
C = {s1 : test(”d”), s2 : ∃q.s1 , s3 : ∃p.s2 }
Figure 1: A graph G and a catalogue C with a, b, p, q ∈ IRIs, ”d” ∈ Literals, and s1 , s2 , s3 ∈ Names.
The semantics of a catalogue C on a graph G is defined in terms of shape assignments, which indicate which shape names hold in which nodes of G. A shape assignment for C and G is a relation α ⊆ dom(C) × (Nodes(G) ∪ Const(C)). We define the semantics of shape φ in catalogue C on graph G under assignment α inductively on the structure of φ as the set JφKα ∪ Const(C) in Table 1. We write G,C ⊆ Nodes(G) α(s) for the set u | (s, u) ∈ α . We call α correct if α(s) = JC(s)Kα G,C for every s ∈ dom(C).
Example 1. Consider the graph G and shape catalogue C in Fig. 1. Intuitively, the shape C(s1 ) captures the literal ”d”, C(s2 ) nodes having a q-edge to a node of shape s1 , and C(s3 ) nodes that have a p-edge to a node of shape s2 . The assignment α1 = {(s1 , ”d”), (s2 , b), (s3 , a)} is correct. The assignment α2 = {(s1 , ”d”), (s2 , b), (s3 , a), (s3 , b)} is not correct because of the pair (s3 , b). Indeed, under assignment α2 , only the node a has a p-edge to a node assigned to s2 . 2 That is, α2 (s3 ) = {a, b} ̸= {a} = JC(s3 )Kα G,C . Next, we consider an example of a recursive catalogue. Example 2. Consider graph G in Fig. 1 and catalogue C = {s : ∃p.s}. Then assignment α3 = {(s, a), (s, b)} is correct. Indeed, the catalogue C from Example 2 is recursive, because the shape in the declaration of s uses s again. In general, a catalogue C is recursive if there is a directed cycle in the graph with nodes dom(C) and having an edge (s, t) if and only if t occurs in C(s). SSL is intentionally simple, yet sufficient to illustrate how the choice of the semantics for recursion influences the expressive power of shape catalogues. As we will see later, the RDF schema languages ShEx and SHACL have more features, in particular for constraining the immediate neighbourhood of nodes (which in SSL is reduced to ∃p.φ and ∀p.φ for testing the existence of a predicate whose object satisfies a property). We discuss in Section 4 how our definition relates to real-world ShEx and SHACL.
2.3
Classic Recursive Semantics
We now describe three classic semantics for recursion: supported model semantics (SMS), greatest fixpoint (GFP), and least fixpoint (LFP). Each semantics specifies which shape assignments conform to the shape catalogue. The most permissive is SMS: it allows all correct shape assignments. Definition 1. A shape assignment α for catalogue C and graph G conforms to C under the supported model semantics SMS (SMS-conforms), if α is correct wrt. C. We write JCKG for the set of all such α. The downside of the supported model semantics is that it allows multiple conforming shape assignments, which can be counter-intuitive and computationally expensive. Example 3. Continuing Ex. 2 with catalogue C = {s : ∃p.s}, notice that in addition to α3 , also α4 = ∅ is correct. Arbitrarily choosing a single canonical shape assignment among the correct ones is problematic. Two natural ideas that come to mind are: be minimalistic and pick the smallest correct assignment (with respect to set inclusion), or be generous and pick the largest correct assignment. These ideas ultimately lead to two classical semantics, LFP and GFP, but getting there requires some work because in general there might be multiple smallest and multiple largest correct shape assignments, which we illustrate next. Example 4. Consider G in Fig. 1 with catalogue C = {s : ∃p. ¬s}. Both assignments α1 = {(s, a)} and α2 = {(s, b)} are correct, but neither β1 = ∅ nor β2 = {(s, a), (s, b)} are, showing that α1 and α2 are simultaneously smallest and largest at the same time. Single smallest and largest correct assignments are guaranteed in a special case: when the catalogue does not use negation.3 This follows from the monotonicity of an associated operator “7→”, mapping shape assignments to shape assignments, defined as α 7→ (s, v) ∈ dom(C) × NC | v ∈ JC(s)Kα G,C
where NC = Nodes(G) ∪ Const(C) . Indeed, it is not hard to see that a shape assignment α is correct iff it is a fixpoint of this operator, that is, if α 7→ α. When the catalogue does not use negation, the operator is monotone and, by the Knaster–Tarski theorem (Tarski 1955), it has unique least and greatest fixpoints. Moreover, by the Kleene fixpoint theorem (Tarski 1955), the least and greatest fixpoint can be computed by iterating the operator on, respectively, the empty shape assignment, ∅ 7→ α1 7→ α2 7→ . . . , and the “full” shape assignment Ω = dom(C)×(Nodes(G)∪ Const(C)), Ω 7→ α1 7→ α2 7→ . . . . This allows us to define the least and greatest fixpoint semantics for catalogues that do not use negation. Definition 2. Let C be a catalogue that does not use negation. A shape assignment α for catalogue C and graph G conforms to C under the LFP (resp. GFP) semantics, if α is the smallest (resp. largest) correct assignment w.r.t. C. We also say that α LFP-conforms (resp. GFP-conforms) to C. 3
There are also weaker sufficient conditions for monotonicity.
Examples 2 and 3 show that the LFP and GFP semantics of the same catalogue C can be different. There is a canonical way of extending any semantics from catalogues without negation to catalogues where negation is used in a controlled fashion. This approach is called stratification and we explain it next. Consider a catalogue C without negation and assume that we have a unique shape assignment that conforms to C (as is the case for the LFP and GFP semantics). That is, we know what each shape name in C means. We could now allow using these shape names in declarations of new shape names, both positively and negatively, and when defining the semantics of the new shape names, treat the semantics of the old ones as fixed (called frozen in the literature). Let us illustrate this with an example. Example 5. Under LFP, the shape assignment that conforms to the catalogue {r : test(a) ∨ ∃p.r} associates shape r to nodes that can reach node a using p-edges; for example, on graph G of Fig. 1, we get {(r, a), (r, b)}. Let us fix this meaning of r and extend the catalogue with declaration s : ¬r ∨ ∃q.s. If we now apply the LFP semantics, with the meaning of r frozen, as described above, the conforming assignment associates s to nodes that can reach via q-edges a node that is safe, in the sense that it cannot reach a via p-edges. On graph G in Fig. 1 we get {(r, a), (r, b), (s, b), (s, ”d”)}. Following this idea one can generalize the LFP and GFP semantics to stratified catalogues, defined below. Definition 3. A stratification for a catalogue C is a partitioning of dom(C) into sets Σ0 , Σ1 , . . . , Σn , called strata, such that for all i, declarations of shape names from stratum Σi only use shape names from Σ0 ∪ Σ1 ∪ · · · ∪ Σi , and are allowed to use negation only in expressions of the form ¬test(c) with c ∈ IRIs∪Literals and ¬s with s ∈ Σ0 ∪Σ1 ∪· · ·∪Σi−1 . A catalogue C is stratified if there is a stratification for C. In Example 5, we can take Σ0 = {r} and Σ1 = {s} for the extended catalogue. Given a stratification Σ0 , Σ1 , . . . , Σn for a catalogue C, we can define the conforming shape assignment inductively for shape names from Σi for i = 0, 1, . . . , n, at each level substituting shape names from lower levels with their already computed semantics. While stratifications are not unique, the resulting LFP and GFP semantics do not depend on their choice (see, e.g., (Apt, Blair, and Walker 1988)). Definition 4. Consider a graph G and a catalogue C with stratification Σ0 , Σ1 , . . . , Σn . Let Ci be obtained by restricting C to Σ0 ∪Σ1 ∪· · ·∪Σi ; that is, Ci consists of declarations from C for shape names from Σ0 ∪ Σ1 ∪ · · · ∪ Σi . Define αi ⊆ Σi × (Nodes(G) ∪ Const(C)) iteratively for i = 0, 1, . . . , n, as follows. Assuming that α0 , . . . , αi−1 are already known, let αi be the least shape assignment over Σi such that α0 ∪ α1 ∪ · · · ∪ αi is correct for Ci . We say an assignment α for G and C LFP-conforms to C if α = α0 ∪ α1 ∪ · · · ∪ αn . Notice that, by definition, α LFP is unique. We write this α as JCKG . The shape assignment GFP JCKG GFP-conforming to C is defined analogously, except that for αi we take the largest shape assignment over Σi s.t. α0 ∪ α1 ∪ · · · ∪ αi is correct for Ci .
Example 6. Shape assignments that GFP-conform to catalogue {s : ¬test(b) ∧ ∀p.s} associate shape s to nodes that cannot reach node b using p-edges. For G from Fig. 1, one gets {(s, ”d”)}. The LFP and GFP semantics are tightly connected by a fundamental principle of duality, which allows translations back and forth. For a stratified SSL catalogue C we define the dual catalogue Ce = s : φ e | (s : φ) ∈ C where the dual shape φ e is defined recursively as follows, relying on φ using ¬ only in expressions ¬test(c) and ¬s, ^ = ¬test(c) , ¬test(c) ^ = test(c) , e = ⊤, ⊤ e = ⊥ , test(c) ⊥ se = s , ¬ fs = ¬s , φ^ f1 ∨ φ f2 , 1 ∧ φ2 = φ g = ∀p.φ g = ∃p.φ φ^ f1 ∧ φ f2 , ∃p.φ e , ∀p.φ e. 1 ∨ φ2 = φ That is, φ e is obtained from φ by swapping ⊤ and ⊥, test(c) and ¬test(c), ∧ and ∨, as well as ∃ and ∀, but s and ¬s are not swapped. Example 7. Consider again the catalogue {s : ¬test(b) ∧ ∀p.s} from Ex. 6. Shape assignments that LFP-conform to its dual {s : test(b) ∨ ∃p.s} assign s to nodes that can reach b using p-edges. Proposition 1. Let G be a graph and C a stratified SSL catalogue. Then, for every shape assignment α for G and C, α LFP-conforms to C iff Ω \ α GFP-conforms to Ce for Ω = dom(C) × (Nodes(G) ∪ Const(C)). Proof. Suppose first that C has a single stratum; that is, it only uses ¬ in expressions of the form ¬test(c). Let us write 7→ for the operator associated with C and 7→ ˜ for the one e Both operators are monotone. From the associated with C. definition of Ce it follows that α 7→ α′ iff Ω \ α 7→ ˜ Ω \ α′ . Hence, ∅ 7→ α1 7→ α2 7→ . . . iff Ω 7→ Ω\α1 7→ ˜ Ω\α2 7→ ˜ .... By the Kleene Fixed-Point Theorem, α is the least fixpoint of 7→ iff Ω \ α is the greatest fixpoint of 7→ ˜. For a general stratified catalogue C, we note that a stratifie and cation Σ0 , Σ1 , . . . , Σn for C is also a stratification for C, proceed by straightforward induction following Def. 4. Using Proposition 1 one can show that SSL under both LFP and GFP corresponds precisely to the alternation-free fragment of the modal µ-calculus (Kozen 1983) with nominals but without atomic propositions, which means it has considerable expressive power.
2.4
Schemas, Conformance, and Validation
The real purpose of shape languages is specifying conformance of graphs to shape schemas, which ensures that graphs satisfy some specified constraints. The task of checking if a given graph conforms to a schema is called validation. To this end, both SHACL and ShEx have a mechanism to select nodes that need to satisfy some shape: SHACL has target declarations (Knublauch and Kontokostas 2017) and ShEx has shape maps (Prud’hommeaux and Baker 2017). We abstract them here as selector maps. Given a shape catalogue
C, a selector map sel for C is a finite set of selectors of the form s : τ with s ∈ dom(C) and τ is a shape that does not use shape names.4 A shape schema is then a tuple S = (C, sel ) with C a shape catalogue, and sel a selector map. Intuitively, every s : τ in sel expresses that every node u that has shape τ should also have shape s under shape assignment(s) conforming to C. In order to define the semantics precisely, we need to handle the nondeterminism of SMS and agree on the domain over which u ranges. A shape assignment for catalogue C and graph G associates shape names with elements of Nodes(G) ∪ Const(C), which does not necessarily include all constants mentioned in sel . We deal with this by incorporating the selector map into the catalogue as follows. We define Csel = C ∪ {ts,τ : τ ∧ ¬s | s : τ ∈ sel }, where every ts,τ is a fresh shape name that depends on s and τ . Then, for a correct shape assignment α for G and Csel , we say a graph G conforms to schema (C, sel ) under α if α(ts,τ ) = ∅ for every shape name ts,τ . Finally, we say that G LFP-conforms to (C, sel ) if G conforms to LFP (C, sel ) under α = JCsel KG , and analogously for GFP. We can define graph conformance under SMS similarly, but we need to decide what to do with the multiple conforming shape assignments a catalogue might admit. Two approaches have been considered, called the cautious and brave SMS semantics (Corman, Reutter, and Savković 2018; Andresel et al. 2020; Bogaerts and Jakubowski 2021). We say that G cautiously (resp. bravely) SMS-conforms to schema SMS (C, sel ) if G conforms to (C, sel ) under every α ∈ JCsel KG SMS (resp. some α ∈ JCsel KG ). We use brave semantics by default and say simply that G SMS-conforms to C. Example 8. Consider the graph G = {(a, p, a)} and the schema (C, sel ) where C = {s : ∃p.s} and sel = {s : test(a)}. Under LFP semantics, we would expect the shape assignment αl = ∅, while under GFP semantics, we get the shape assignment αg = {(s, a)}. Thus, G GFP-conforms to (C, sel ), but G does not LFP-conform to (C, sel ).
3
A Comparative Study of Implementations
We present an experimental study of real-world engines for SHACL and ShEx to compare how they treat recursive schemas. We want to understand, for each engine, is there a formal semantics for recursive shapes that explains its behaviour? The main challenge is that real-world systems only test whether a given graph conforms to a given schema, without giving access to the witnessing shape assignments. In order to detect which semantics is applied, we design test cases that aim to separate LFP, GFP, brave SMS, and cautious SMS. First, we run all test cases on all engines. If we observe inconsistent behaviour, we investigate the test results in more detail. If all answers are consistent with one of the three semantics, we interpret this as the answer to our question. To allow reproducibility, we make the source code of our tool, as well as the experimental results available in an anonymous repository.5 4
Both ShEx and SHACL impose additional restrictions on τ , essentially allowing only atomic shape expressions, and do not allow ⊤; see (Ahmetaj et al. 2025). 5 https://doi.org/10.5281/zenodo.17249933
We designed thirteen test cases, falling into two test categories: separation and feature tests. Separation tests attempt to distinguish whether an engine uses LFP, GFP, brave SMS, or cautious SMS. Feature tests do exactly what their name suggests. Each such test S = ⟨G, C, sel ⟩ consists of a graph G, a shape catalogue C, and a shape map sel . The intended use of S is to produce a ShEx or SHACL schema based on C and sel to check whether G conforms to (C, sel ). For each separation test we list all correct shape assignments. The unique conforming assignments under LFP and GFP appear as αLFP and αGFP , and the remaining ones as α1 , α2 . An assignment α is blue, if G conforms to (C, sel ) under α, and red, if it does not.
Feature tests These target more specific properties of the validator, as we will explain after introducing them.
Basic separation tests. These four tests are designed to distinguish a validator that employs LFP semantics from one that employs GFP, using minimal examples.
• cons1 (consistency): G = {(a, p, a)}, C = {s : ∃p.s′ , s′ : ¬s}, sel = {s : test(a), s′ : test(a)} Passing Condition: The validator rejects.
• bsep1: G = {(a, p, a)} , C = {s : ∃p.s} , sel = {s : test(a)} , αLFP = ∅ , αGFP = {(s, a)} . • bsep2: G = {(a, p, a), (b, p, b)}, C = {s : ∃p.s}, sel = {s : test(a), s : test(b)} , αLFP = ∅ , αGFP = {(s, a), (s, b)} , α1 = {(s, a)} , α2 = {(s, b)} . • bsep3: G = {(a, p, c), (b, p, c)}, C = {s : s′ ∧ ∃p, s′ : s ∧ ∃p}, sel = {s : test(a), s : test(b)} , αLFP = ∅ , αGFP = {(s, a), (s, b), (s′ , a), (s′ , b)} , α1 = {(s, a), (s′ , a)} , α2 = {(s, b), (s′ , b)} . • bsep4: G = {(a, p, a), (b, p, b)}, C = {s : ∃p.s, s′ : ¬s}, sel = {s : test(a), s : test(b)} , αLFP = {(s′ , a), (s′ , b)} , αGFP = {(s, a), (s, b)} , α1 = {(s, a), (s′ , b)} , α2 = {(s, b), (s′ , a)} .
Reachability separation tests. Then, we tested a classical recursive property of reachability and its dual property of safety by checking them on two dual shape names r and s, in four different scenarios. All scenarios use the same graph: : p-edge d c G: a b • reach1: C = {r : test(a) ∨ ∃p.r}, sel = {r : test(a), r : test(b), r : test(c), r : test(d)} , αLFP = {(r, a), (r, b)} , αGFP = {(r, a), (r, b), (r, c), (r, d)} . • reach2: C = {s : ¬test(a) ∧ ∀p.s, r : ¬s}, sel = {r : test(c), r : test(d)} , αLFP = {(r, a), (r, b), (r, c), (r, d)} , αGFP = {(r, a), (r, b), (s, c), (s, d)} . • safe1: C = {s : ¬test(a) ∧ ∀p.s}, sel = {s : test(c), s : test(d)} , αLFP = ∅ , αGFP = {(s, c)(s, d)} . • safe2: C = {r : test(a) ∨ ∃p.r, s : ¬r}, sel = {r : test(c), r : test(d)} , αLFP = {(r, a), (r, b), (s, c), (s, d)} , αGFP = {(r, a), (r, b), (r, c), (r, d)} .
• nstrat1 (non-stratified negation without cyclic data): G = {(a, p, b), (b, p, c), (c, p, d), (d, p, e)}, C = {s : ∃p.¬s}, sel = {s : test(a), s : test(b), s : test(c), s : test(d), s : test(e)} Passing Condition: Accept or reject the schema over Gn1 . • nstrat2 (non-stratified negation with cyclic data): G = {(a, p, b), (b, p, a)}, C = {s : ∃p.¬s}, sel = {s : test(a), s : test(b)} Passing Condition: Accept or reject the schema over G. • fresh (fresh constant support): G = {(a, p, b), (b, p, c), (c, p, a)}, C = {s : ⊤}, sel = {s : test(d)} Passing Condition: The validator accepts.
• cons2 (consistency): G as in nstrat2, C as in cons1, sel = {s : test(a), s′ : test(a), s : test(b), s′ : test(b)} Passing Condition: The validator rejects.
The tests nstrat1 and nstrat2 are for shape catalogues that do not permit a stratification as in Definition 3. While none of our semantics support this setting, we still aim to find out how real-world validators behave on such inputs. The test fresh has a shape catalogue with a shape assignment that is trivially satisfied, using the shape ⊤. In the shape map, we require that this shape is satisfied in a “fresh node”, that is, a node that is not featured in the graph. This reflects something that both SHACL and ShEx permit: selecting nodes outside the input graph. Finally, cons1 and cons2 check for logical consistency. We have a catalogue with two shapes, s and s′ , where s′ is defined as the negation of s. Then we ask in the shape map that both s and s′ be assigned to the same node. Since no such assignment is possible while being consistent with the catalogue’s semantics, this test requires that a validator rejects. Validation Engines Since the SHACL W3C Recommendation does not require SHACL validators to support recursive schemas, many validators reject them all or raise a warning indicating that recursion is not supported. We focus on those that do support recursive SHACL schemas or where we can ignore the warnings and perform the validation anyway, meaning that they accept a non-empty set of graphs when validating against a recursive SHACL schema. These are pySHACL (pySHACL 2025), SHACL-S (SHACL-S 2024), Jena SHACL (Apache Jena 2025), Topbraid (TopQuadrant SHACL 2025), and rudof (RuDoF Project 2025), which supports both SHACL and ShEx. For ShEx, we have ShEx-S (ShEx-s 2025), Jena ShEx (Apache Jena 2025), and rudof (RuDoF Project 2025). Discussion We see the results of our experiments in Table 2. For each of the separation tests (first eight rows), a validator can answer yes (•) or no (■), or fail (X) by reporting an error, crashing, or not terminating within 5 seconds.6 In the columns GFP, LFP, bSMS (brave SMS), and cSMS 6 Our test graphs have at most 5 nodes and edges, so the timeout is rather generous.
do Je f (S na hE Sh ShE x) Ex x -S py SH SH A A C Je CL L na To SH S p A ru bra CL do id f( G SHA F CL LF P ) bS P M cS S M S
ru
Te st
in s
ta nc e
Table 2: Results of comparative study of the semantics of SHACL and ShEx validators for recursive shape catalogues.
bsep1 bsep2 bsep3 bsep4 reach1 reach2 safe1 safe2
• • • • •
• • • • •
• • • • •
• • • • • •
■
■
• • • • • • • • • • X X • ■ X • • • • • • • • ■ • • • • • X • • • • X • • • ■ •
• ■ • ■ • ■ • ■ • ■ • ■ • ■ • ■ • ■ • ■ ■ • • ■ • ■ • ■ • ■ • ■
■
nstrat1 nstrat2 fresh cons1 cons2
✗* ✓ ✗* ✓ ✗ ✓ ✗* ✓ ✗* ✗
✗* ✗* ✓ ✗* ✗*
✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓
-
-
-
-
(cautious SMS), we indicate the answer prescribed by the respective semantics. For bsep1, for example, G does not conform to (C, sel ) under αLFP , so the correct answer under LFP is no (■). However, G does conform to (C, sel ) under αGFP , so the correct answer under GFP is yes (•). The answer yes is also correct under bSMS, because αGFP witnesses it. However, the answer no is correct under cSMS because αLFP witnesses it: it is a correct assignment that does not associate s to a as required by sel . An analogous reasoning applies for all values of yes (•) and no (■) in the last four columns. Therefore, using Table 2, we can immediately see which validators are consistent with which semantics. We see that the three ShEx validators, rudof, Jena ShEx and ShEx-S, are consistent with GFP, as prescribed by the official semantics (Prud’hommeaux et al. 2019). On the SHACL side, the picture is more varied. Four validators, namely pySHACL, SHACL-S, Jena SHACL and rudof, are consistent with bSMS, if we ignore the error cases. The behaviour of Topbraid stands out. It is not consistent with either GFP, LFP, bSMS, or cSMS, as can be seen. Topbraid thus seems to follow a unique semantics. For the five feature tests we have two outcomes, pass (✓) or fail (✗), since by design these tests interpret errors unrelated to validation as failing the test. We will nonetheless indicate failures due to these causes by an asterisk (✗*). The failures for the ShEx validators can be explained by the fact that all feature tests, except for fresh, use non-stratified negation, which is disallowed in ShEx. ShEx-S and rudof (ShEx) correctly reject such inputs. JenaShEx does not reject them and attempts validation. We see that it passes all tests, except for the second test for logical consistency. Perhaps this asymmetric behaviour of JenaShEx for two very similar tests can be attributed to a software bug. One notable result is that rudof does not pass fresh; indeed it is the only validation engine to fail it, and curiously, rudof itself, when targeting SHACL, does pass it. On the SHACL side, all validators pass all the feature tests. Note that our test results do not prove that any of the
validators follows a given semantics, as other tests might reveal inconsistencies. They do prove, however, that some validators do not follow a given semantics, and they give us hints as to how these real-world systems act. Claiming that their semantics follows GFP, LFP, bSMS, or cSMS requires knowledge of the algorithm each system implements, and a formal study of said algorithm.
4
Recursion in ShEx and SHACL
Building on the framework developed in Section 2, we now explore how the choice of semantics for recursion impacts the expressive power and complexity of ShEx and SHACL. We give semantics-preserving translations between core fragments of the two languages under GFP/LFP and establish tight complexity bounds exposing the cost of SMS.
4.1
The ShEx and SHACL Schema Languages
We instantiate our abstract framework with the standard RDF validation languages ShEx (Prud’hommeaux et al. 2019) and SHACL (Knublauch and Kontokostas 2017). We see them as variants of SSL that allow different kinds of shapes: most notably, SHACL shapes use complex path expressions to specify paths in terms of sequences of predicates, and ShEx shapes use triple expressions to specify neighbourhoods in terms of sets of triples. The notions of shape catalogues and shape assignments naturally extend to ShEx and SHACL. Below we present the syntaxes of these languages as they were presented in (Ahmetaj et al. 2025), to which we add recursion via references to shape names, as in SSL. Their semantics are combinations of the semantics of (non-recursive) shapes from (Ahmetaj et al. 2025) with the semantics of recursion we have defined for SSL. Both languages use value type constraints that are interpreted as sets of constants. Formally, T is a finite set of value types, and for every v ∈ T , its semantics is JvK ⊆ IRIs ∪ Literals ∪ Blanks. Throughout this subsection, we fix an RDF graph G. Definition 5 (SHACL syntax and semantics). SHACL shapes φ and path expressions π are given by the following grammar, with c ∈ IRIs∪Literals, v ∈ T , Q ⊆fin IRIs, p ∈ IRIs, n ∈ N, s ∈ Names: φ ::= ⊤ ⊥ test(c) test(v) s closed(Q) ¬φ φ ∧ φ φ ∨ φ eq(π, p) disj(π, p) ∃≥n π.φ ∃≤n π.φ . π ::= id p π − π · π π ∪ π π ∗ . The semantics JφKα G,C ⊆ Nodes(G) ∪ Const(C) of a SHACL shape φ in catalogue C on graph G under assignment α is defined by recursion on the structure of φ, by extending Table 1 with Jtest(v)Kα G,C = JvK, ≥n J∃ π.φKα # u ∈ JπKGv | u ∈ JφKα G,C = v G,C ≥ n , J∃≤n π.φKα # u ∈ JπKGv | u ∈ JφKα G,C = v G,C ≤ n , α G Jclosed(Q)KG,C = v JpKv = ∅ for all p ∈ IRIs \ Q , G G Jeq(π, p)Kα G,C = v JπKv = JpKv , G G Jdisj(π, p)Kα G,C = v JπKv ∩ JpKv = ∅ ,
where JπKGv is the set of nodes accessible in G from v by a sequence of edges whose predicates match the path expression π; that is, JπKGv = u (v, u) ∈ JπKG and JπKG is as in (Ahmetaj et al. 2025). Definition 6 (ShEx syntax and semantics). ShEx shapes φ, triple expressions e, and closed triple expressions f , are defined by the following grammar, with c ∈ IRIs ∪ Literals, v ∈ T , s ∈ Names, p ∈ IRIs, and R, Q ⊆fin IRIs: φ ::= test(c) test(v) s e φ ∧ φ φ ∨ φ ¬φ . e ::= f ;(¬R− )∗
Data complexity LFP/GFP SMS
Combined complexity LFP/GFP SMS
SSL P† NP ‡ P† NP ‡ SHACL P † NP ‡ P† NP ‡ ShEx P (Th. 2) NP (Th. 2) P NP (Th. 3) NP NP (Th. 3) †(Andresel et al. 2020) ‡(Corman, Reutter, and Savković 2018)
f ;(¬R− )∗ ;(¬Q)∗ .
f ::= ε p.φ p− .φ f ; f f | f f ∗ . The semantics JφKα G,C
⊆ Nodes(G) ∪ Const(C) of a ShEx shape φ in catalogue C on graph G under assignment α is defined by recursion on the structure of φ, by extending Table 1 with ± α J e Kα G,C = v NeighG (v) ∈ JeKG,C ,
′ where Neigh± G (v) collects edges (v, p, v ) ∈ G outgoing − ′ from v and inverses (v, p , v ) of edges (v ′ , p, v) ∈ G incoming to v, and JeKα G,C is the family of sets of edges and inverses of edges from G that match e, defined recursively as follows. Expression ε matches ∅. Expressions p.φ and p− .φ match singletons {(u, p, w)} and {(u, p− , w)} such that w ∈ JφKα G,C . Expression f1 | f2 matches sets matched by f1 and sets matched by f2 . Expression f1 ; f2 matches sets that can be expressed as a union of two disjoint sets F1 and F2 matched by f1 and f2 , respectively. Expression f ∗ matches sets that can be expressed as a union of arbitrarily many disjoint sets matching f . Expression (¬Q)∗ matches arbitrary sets of p-edges with p ∈ / Q and (¬R− )∗ matches − arbitrary sets of p -edges with p ∈ / R. Intuitively, a set of triples matched by a closed triple expression f may contain only triples explicitly mentioned in f . A closed expression cannot be used directly in a ShEx shape: it can only occur as a subexpression of an expression e which opens allowed set of triples to all p− -edges with p ∈ / R and possibly also to all p-edges with p ∈ / Q. Stratification for ShEx and SHACL is defined as for SSL. (Using auxiliary shape definitions, one can rewrite each schema so that it applies negation only to sub-expressions of the form test(c), test(v) and s.) Following standard ShEx, we assume GFP by default and say that a graph conforms to a ShEx schema if it GFP-conforms.
4.2
Table 3: Complexity of validation
Expressive Power
We now identify large equi-expressive syntactic fragments of ShEx (with GFP) and SHACL with LFP that have the same expressive power. In the case of ShEx, we forbid applying ‘*’ to triple expressions that contain ‘;’. Definition 7 (Restricted ShEx). Restricted ShEx is the syntactic fragment of ShEx obtained by replacing the rule for closed triple expressions f from Def. 6 with the following derivation rules: f ::= f ′ f ′∗ f ; f f | f . f ′ ::= ε p.φ p− .φ f ′ | f ′ .
In the case of SHACL, we restrict counting to single edges, while allowing existential quantification over arbitrary path expressions. Definition 8 (Restricted SHACL). Restricted SHACL is the syntactic fragment of SHACL defined by the grammar φ ::= ⊤ ⊥ test(c) test(v) s closed(Q) ¬φ φ ∧ φ φ ∨ φ ∃≥n p.φ ∃≥n p− .φ ∃≤n p.φ ∃≤n p− .φ ∃π.φ . Having defined the restricted fragments, we can formulate the equivalence result. Theorem 1. Restricted ShEx (with GFP) and restricted SHACL with LFP have the same expressive power and there are effective back-and-forth translations between them. The proof proceeds by normalizing both formalisms to even simpler fragments and applying the duality principle (see Appendix A).
4.3
Complexity
An overview of prior and new results on the complexity of validation is given in Table 3. Both the combined and data complexity have been known for SHACL under LFP and SMS (Andresel et al. 2020; Corman, Reutter, and Savković 2018). For GFP the complexity is the same, as it comes from iterating a polynomial number of times the same operator as for LFP. The upper bounds cover SSL, which is a fragment of SHACL. The NP lower bounds carry over too, because the SHACL schemas used in the proofs are readily expressible in SSL, but we found a much simpler proof (for a fixed schema), by a straightforward reduction from 3COLOURABILITY (see Appendix B). For ShEx it has only been known that combined complexity for the fragment without Boolean connectives is NP-complete under GFP (Staworko et al. 2015). We fill this gap by establishing tight bounds for full ShEx under all three semantics. Theorem 2 (Data complexity of ShEx). For a fixed ShEx schema S, the problem of deciding whether a given graph G conforms to S is in P for both LFP and GFP, and NPcomplete for SMS. The NP lower bound for SMS in Theorem 2 carries over from SSL which is subsumed by ShEx. Let us move to the upper bounds. The validation problem for all three semantics amounts to applying the operator over shape assignments that is associated with the shape catalogue: for SMS we apply the
operator to the guessed shape assignment to check if it is a fixpoint, and for LFP and GFP we iterate the operator over a suitable initial shape assignment until a fixpoint is reached, which is guaranteed to happen in a polynomial number of iterations. Applying the operator to a shape assignment α amounts to evaluating shape expressions in the catalogue, which is straightforward (following their syntactic structure) except for one subtask: checking whether the neighbourhood of a node in the graph matches a triple expression. Thus, in order to prove the upper bounds from Theorem 2, it suffices to show that this subtask is tractable. We do it in Proposition 2. By adding auxiliary declarations to the catalogue, we can assume that triple expressions are shallow, in the sense that the shape expression φ in atomic triple expressions p.φ and p− .φ must be a shape name. Proposition 2. Fix a catalogue C and a shallow triple expression e as in Def. 6 occurring in C. Given as input a graph G, a shape assignment α for G and C, and a node v, we can α decide in polynomial time whether Neigh± G (v) ∈ JeKG,C . Proof. In this proof, q stands for a predicate p or an inverse predicate p− . Let Πe be the set of predicates p used in e (including those in subexpressions ¬R− and ¬Q) and their inverses p− , and let other be a fresh predicate not used in e. Let Γe,q be the set of shape names s s.t. q.s occurs in e. An edge type for e is a pair (q, T ) where q ∈ Πe ∪ {other, other− } and T ⊆ Γe,q . Let Σe denote the set of all edge types for e. In particular, (other, ∅), (other− , ∅) ∈ Σe . Note that Σe might be exponential in the size of e, but this is fine as we consider e to be fixed. A triple (v, q, v ′ ) in Neigh± G (v) with q ∈ Πe has type (q, T ) under shape assignment α if v ′ ∈ α(s) for each s ∈ T and v ′ ̸∈ α(s) for each s ∈ Γe,q \ T . A triple (v, q, v ′ ) in Neigh± G (v) with q ̸∈ Πe has type (other, ∅) if q is a predicate, and (other− , ∅) if q is an inverse predicate. Note that each triple in Neigh± G (v) has exactly one type. We define Mα,e G,v as the multiset of types of triples in ± NeighG (v). That is, Mα,e G,v is a multiset over Σe and the multiplicity of (q, T ) in Mα,e G,v is equal to the number of triples (v, q, v ′ ) in Neigh± (v) that have type (q, T ). G Let M be a multiset over Σe . For (q, T ) ∈ Σe we write M (q, T ) for the multiplicity of (q, T ) in M . We call M the singleton of (q, T ) if M (q, T ) = 1 and M (q ′ , T ′ ) = 0 for all (q ′ , T ′ ) ∈ Σe \ {(q, T )}. We say M is split into multisets M1 and M2 over Σe if M1 (q, T ) + M2 (q, T ) = M (q, T ) for every (q, T ) ∈ Σ. Consider the nondeterministic Algorithm 1, which recursively splits Mα,e G,v while attempting to match subexpressions α of e. It is easy to see that Neigh± G (v) ∈ JeKG,C iff some run of Algorithm 1 on G, α, v, e returns true.
(†)
Due to the possible presence of ∗ in e, Algorithm 1 need not terminate. Yet, condition (†) can be effectively checked. In fact, it can be checked in polynomial time when e is assumed to be fixed and only the size of G, α, v may grow. Indeed, the recursive subroutine RecMatch can be seen as an alternating procedure that requires only logarithmic space. Indeed, storing the multisets M, M1 , M2 used in the RecMatch requires
Algorithm 1: Matching Triple Expressions Input: graph G, shape assignment α, node v, shallow triple expression e = f0 ;(¬R− )∗ or e = f0 ;(¬R− )∗ ;(¬Q)∗ α Output: true iff Neigh± G (v) ∈ JeKG,C α,e 1 M0 := MG,v ; // extract multiset from Neigh± G (v) 2 return RecMatch(M0 , e) 3 Function RecMatch(M, f ): 4 if f = f1 ; f2 then 5 Nondeterministically split M into M1 and M2 ; 6 return RecMatch(M1 , f1 ) && RecMatch(M2 , f2 ) 7 8 9 10 11 12 13
14 15 16
if f = u∗ then Nondeterministically split M into M1 and M2 ; return RecMatch(M1 , u) && RecMatch(M2 , f ) if f = f1 | f2 then return RecMatch(M, f1 ) || RecMatch(M, f2 ) if f = q.s and M is the singleton of (q, T ) with s ∈ T then return true ; if f = ¬Q and M is the singleton of (p, T ) with p ̸∈ Q then return true ; if f = ¬R− and M is the singleton of (p− , T ) with p ̸∈ R then return true ; if f = ε and M is empty then return true ; return false
only logarithmic space: for each multiset we only need |Σe | counters that count up to the number of nodes in G. Hence, the problem of checking (†) is in AL OG S PACE and hence in P since AL OG S PACE = P. For the combined complexity the upper bounds are straightforward, and the lower bounds use reductions from suitable variants of the SAT problem (see Appendix C). Theorem 3 (Combined complexity of ShEx). The problem of deciding whether a given graph G conforms to a given ShEx schema is P NP -complete for LFP and GFP, and NP NP complete for SMS.
5
Conclusion
The behaviour of SHACL validators on recursive schemas is unpredictable, which is only natural since its language design does not settle how to deal with recursion. Indeed, while ShEx systems consistently behave in line with GFP, SHACL validators mostly appear to be aligned with brave SMS, but some fail on simple schemas and others appear to mix behaviours depending on structural properties of the schema. This heterogeneity explains long-standing interoperability glitches and motivates standardizing an explicit, implementation-independent recursion contract.
References Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of Databases. Addison-Wesley. Ahmetaj, S.; David, R.; Ortiz, M.; Polleres, A.; Shehu, B.; and Simkus, M. 2021. Reasoning about explanations for non-validation in SHACL. In Principles of Knowledge Representation and Reasoning (KR).
Ahmetaj, S.; David, R.; Polleres, A.; and Simkus, M. 2022a. Repairing SHACL constraint violations using answer set programming. In International Semantic Web Conference (ISWC), 375–391. Ahmetaj, S.; Löhnert, B.; Ortiz, M.; and Simkus, M. 2022b. Magic shapes for SHACL validation. Proc. VLDB Endow. 15(10):2284–2296. Ahmetaj, S.; Boneva, I.; Hidders, J.; Hose, K.; Jakubowski, M.; Gayo, J. E. L.; Martens, W.; Mogavero, F.; Murlak, F.; Okulmus, C.; Polleres, A.; Savkovic, O.; Simkus, M.; and Tomaszuk, D. 2025. Common foundations for SHACL, ShEx, and PG-Schema. In The Web Conference (WWW), 8–21. Andresel, M.; Corman, J.; Ortiz, M.; Reutter, J. L.; Savkovic, O.; and Šimkus, M. 2020. Stable model semantics for recursive SHACL. In The Web Conference (WWW), 1570– 1580. Angles, R.; Bonifati, A.; Dumbrava, S.; Fletcher, G.; Hare, K. W.; Hidders, J.; Lee, V. E.; Li, B.; Libkin, L.; Martens, W.; Murlak, F.; Perryman, J.; Savković, O.; Schmidt, M.; Sequeda, J.; Staworko, S.; and Tomaszuk, D. 2021. In International Conference on Management of Data (SIGMOD), 2423—-2436. Angles, R.; Bonifati, A.; Dumbrava, S.; Fletcher, G.; Green, A.; Hidders, J.; Li, B.; Libkin, L.; Marsault, V.; Martens, W.; Murlak, F.; Plantikow, S.; Savkovic, O.; Schmidt, M.; Sequeda, J.; Staworko, S.; Tomaszuk, D.; Voigt, H.; Vrgoc, D.; Wu, M.; and Zivkovic, D. 2023. PG-Schema: Schemas for property graphs. Proc. ACM Manag. Data 1(2). Angles, R.; Thakkar, H.; and Tomaszuk, D. 2020. Mapping RDF databases to property graph databases. IEEE Access 8:86091–86110. Anuradha, R.; Swathi, B.; Nagpal, A.; Chaturvedi, P.; Kalra, R.; and Alwan, A. A. 2023. Deep learning for anomaly detection in large-scale industrial data. In UPCON, 1551– 1556. Apache Jena. 2025. Apache Jena. https://jena.apache.org/. Accessed: 2025-10-04. Apt, K. R.; Blair, H. A.; and Walker, A. 1988. Towards a theory of declarative knowledge. Morgan Kaufmann Publishers Inc. 89–148. Aref, M.; Guagliardo, P.; Kastrinis, G.; Libkin, L.; Marsault, V.; Martens, W.; McGrath, M.; Murlak, F.; Nystrom, N.; Peterfreund, L.; Rogers, A.; Sirangelo, C.; Vrgoč, D.; Zhao, D.; and Zreika, A. 2025. Rel: A programming language for relational data. In International Conference on Management of Data (SIGMOD), 283–296. Baader, F. 1990. Terminological cycles in KL-ONE-based knowledge representation languages. In AAAI, 621–626. Baader, F. 1996. Using automata theory for characterizing the semantics of terminological cycles. Ann. Math. Artif. Intell. 18(2-4):175–219. Bogaerts, B., and Jakubowski, M. 2021. Fixpoint semantics for recursive SHACL. In ICLP, 41–47. Bogaerts, B.; Jakubowski, M.; and den Bussche, J. V. 2022. SHACL: A description logic in disguise. In LPNMR, 75–88.
Bogaerts, B.; Jakubowski, M.; and Van den Bussche, J. 2024. Expressiveness of SHACL Features and Extensions for Full Equality and Disjointness Tests. Logical Methods in Computer Science 20(1). Boneva, I.; Labra Gayo, J. E.; and Prud’hommeaux, E. G. 2017. Semantics and validation of shapes schemas for RDF. In ISWC, 104–120. Bray, T.; Paoli, J.; Sperberg-McQueen, C. M.; Maler, E.; and Yergeau, F. 2008. Extensible markup language (XML) 1.0 (fifth edition). Technical report, World Wide Web Consortium. Corman, J.; Florenzano, F.; Reutter, J. L.; and Savkovic, O. 2019. Validating SHACL constraints over a SPARQL endpoint. In ISWC, 145–163. Corman, J.; Reutter, J. L.; and Savković, O. 2018. Semantics and validation of recursive SHACL. In ISWC, 318–336. Delva, T.; Dimou, A.; Jakubowski, M.; and Van den Bussche, J. 2023. Data provenance for SHACL. In EDBT, 285–297. Eiter, T.; Faber, W.; Fink, M.; and Woltran, S. 2007. Complexity results for answer set programming with bounded predicate arities and implications. Ann. Math. Artif. Intell. 51(2-4):123–165. Ferranti, N.; de Souza, J. F.; Ahmetaj, S.; and Polleres, A. 2024. Formalizing and validating Wikidata’s property constraints using SHACL and SPARQL. Semantic Web. Gao, S. S.; Sperberg-McQueen, C. M.; Thompson, H. S.; Mendelsohn, N.; Beech, D.; and Maloney, M. 2012. W3C XML Schema Definition Language (XSD) 1.1 Part 1: Structures. Technical report, World Wide Web Consortium. Giacomo, G. D., and Lenzerini, M. 1994. Concept language with number restrictions and fixpoints, and its relationship with mu-calculus. In ECAI, 411–415. John Wiley and Sons, Chichester. Hartig, O. 2014. Reconciliation of RDF* and property graphs. CoRR. International Organization for Standardization. 2024. ISO/IEC 39075:2024 Information technology – Database languages – GQL. Technical report. Knublauch, H., and Kontokostas, D. 2017. Shapes Constraint Language (SHACL). W3C Recommendation, W3C. https: //www.w3.org/TR/shacl/. Kozen, D. 1983. Results on the propositional µ-calculus. Theoretical Computer Science 27(3):333–354. Labra Gayo, J. E.; Prud’hommeaux, E.; Boneva, I.; and Kontokostas, D. 2017. Validating RDF Data. Synthesis Lectures on the Semantic Web: Theory and Technology. Morgan & Claypool Publishers. Labra Gayo, J. E.; Garcı́a-González, H.; Fernández-Alvarez, D.; and Prud’hommeaux, E. 2019. Challenges in RDF validation. In Current Trends in Semantic Web Technologies: Theory and Practice. 121–151. Labra Gayo, J. E.; Knublauch, H.; and Kontokostas, D. 2024. SHACL Test Suite and Implementation Report. W3C Document. https://w3c.github.io/data-shapes/ data-shapes-test-suite/. Labra Gayo, J. E. 2022. WShEx: A language to describe and validate wikibase entities. In Wikidata Workshop.
Labra Gayo, J. E. 2024. Extending shape expressions for different types of knowledge graphs. In Data Quality meets Machine Learning and Knowledge Graphs (DQMLKG). Lassila, O., et al. 2023. The OneGraph vision: Challenges of breaking the graph model lock-in 1. Semantic Web 14(1):125– 134. Leinberger, M.; Seifer, P.; Rienstra, T.; Lämmel, R.; and Staab, S. 2020. Deciding SHACL shape containment through description logics reasoning. In International Semantic Web Conference (ISWC), 366–383. Lissandrini, M.; Rabbani, K.; and Hose, K. 2024. Mining validating shape for large knowledge graphs via dynamic reservoir sampling. In Symposium of Advanced Database Systems, 25–34. Martens, W.; Neven, F.; Niewerth, M.; and Schwentick, T. 2017. BonXai: Combining the simplicity of DTD with the expressiveness of XML schema. ACM Trans. Database Syst. 42(3):15:1–15:42. Mohamed, A.; Abuoda, G.; Ghanem, A.; Kaoudi, Z.; and Aboulnaga, A. 2022. RDFFrames: knowledge graph access for machine learning tools. The VLDB Journal 31(2):321– 346. Nebel, B. 1991. Terminological reasoning is inherently intractable. In Artificial Intelligence, volume 43, 235–249. Okulmus, C., and Šimkus, M. 2024. SHACL validation under the well-founded semantics. In KR, 553–562. Oudshoorn, A.; Ortiz, M.; and ǐmkus, M. 2024. Reasoning with the core chase: the case of SHACL validation over ELHI knowledge bases. In Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings. Bergen, Norway: CEURWS.org. Pareti, P.; Konstantinidis, G.; Mogavero, F.; and Norman, T. 2020. SHACL Satisfiability and Containment. In ISWC20, LNCS 12506, 474–493. Springer. Pareti, P.; Konstantinidis, G.; and Mogavero, F. 2022. Satisfiability and Containment of Recursive SHACL. JWS 74:100721:1–24. Prud’hommeaux, E., and Baker, T. 2017. ShapeMap Structure and Language. W3C draft community group report, W3C. http://shex.io/shape-map/. Prud’hommeaux, E.; Boneva, I.; Labra Gayo, J. E.; and Kellogg, G. 2019. Shape expressions language 2.1. W3C community group report, W3C. http://shex.io/shex-semantics/. Prud’hommeaux, E.; Labra Gayo, J. E.; and Solbrig, H. 2014. Shape expressions: an RDF validation and transformation language. In International Conference on Semantic Systems (SEM), 32–40. ACM. pySHACL. 2025. pyshacl: Python validator for SHACL. https://github.com/RDFLib/pySHACL. Accessed: 2025-1004. Rabbani, K.; Lissandrini, M.; and Hose, K. 2023. Extraction of validating shapes from very large knowledge graphs. PVLDB 16(5):1023–1032. RuDoF Project. 2025. Rudof project. https://github.com/ rudof-project/rudof. Accessed: 2025-10-04.
Sakr, S.; Bonifati, A.; Voigt, H.; Iosup, A.; Ammar, K.; Angles, R.; Aref, W. G.; Arenas, M.; Besta, M.; Boncz, P. A.; Daudjee, K.; Valle, E. D.; Dumbrava, S.; Hartig, O.; Haslhofer, B.; Hegeman, T.; Hidders, J.; Hose, K.; Iamnitchi, A.; Kalavri, V.; Kapp, H.; Martens, W.; Özsu, M. T.; Peukert, E.; Plantikow, S.; Ragab, M.; Ripeanu, M.; Salihoglu, S.; Schulz, C.; Selmer, P.; Sequeda, J. F.; Shinavier, J.; Szárnyas, G.; Tommasini, R.; Tumeo, A.; Uta, A.; Varbanescu, A. L.; Wu, H.; Yakovets, N.; Yan, D.; and Yoneki, E. 2021. The future is big graphs: a community view on graph processing systems. Commun. ACM 64(9):62–71. Schild, K. 1994. Terminological cycles and the propositional µ-calculus. In In KR 1994, 509–520. Morgan Kaufmann. SHACL-S. 2024. SHACL-s. https://github.com/weso/ shacl-s. ShEx-s. 2025. Shex-s. https://github.com/weso/shex-s. Accessed: 2025-10-04. Staworko, S.; Boneva, I.; Labra Gayo, J. E.; Hym, S.; Prud’hommeaux, E.; and Solbrig, H. 2015. Complexity and expressiveness of ShEx for RDF. In International Conference on Database Theory (ICDT), 195–211. Tarski, A. 1955. A Lattice-Theoretical Fixpoint Theorem and its Applications. PJM 5(2):285–309. Tomaszuk, D. 2017. RDF validation: A brief survey. In International Conference Beyond Databases, Architectures and Structures (BDAS), 344–355. Springer. TopQuadrant SHACL. 2025. TopQuadrant SHACL. https: //github.com/TopQuadrant/shacl. Accessed: 2025-10-04. Vrgoč, D.; Rojas, C.; Angles, R.; Arenas, M.; Arroyuelo, D.; Buil-Aranda, C.; Hogan, A.; Navarro, G.; Riveros, C.; and Romero, J. 2023. MillenniumDB: An Open-Source Graph Database System. Data Intelligence 1–39. W3C OWL Working Group. 2012. OWL 2 Web Ontology Language Document Overview (Second Edition). W3C recommendation, W3C. https://www.w3.org/TR/2012/RECowl2-overview-20121211/.
A
Proof of Theorem 1
The proof follows these steps. In Section A.1 we define two smaller fragments ShEx0 of ShEx and SHACL0 of SHACL and show that they are equally expressive for the LFP semantics for SHACL0 . Then, in Section A.2 we show that restricted ShEx can be normalised to ShEx0 , and in Section A.3 that restricted SHACL can be normalised to SHACL0 . We say that x1 and x2 are equivalent, written x1 ≡ x2 , if for all graphs G, catalogues C, and assignments α ⊆ dom(C) × (Nodes(G) ∪ Const(C)), it holds Jx1 Kα G,C = . Above, each of x , x can be a ShEx or a SHACL Jx2 Kα 1 2 G,C shape, or a ShEx triple expression.
A.1
ShEx0 and SHACL0
Definition 9 (ShEx0 ). Let ⊤ = ε ;(¬∅− )∗ ;(¬∅)∗ . ShEx0 is given by the grammar φ ::= test(c) test(v) s ¬φ φ ∧ φ φ ∨ φ g h . p.φn ; ⊤ p− .φn ; ⊤ . ∗ h ::= ε ;(¬∅− )∗ p. ε ; ⊤ ; h . g ::= ε ; ⊤
where p.φn is a syntactic shortcut for p.φ ; · · · ; p.φ repeated n times. ShEx0 allows two kinds of limited triple expressions. Expressions g are always completely open (i.e. (¬R− )∗ ;(¬Q)∗ from Def. 6 is always ⊤, obtained for R = Q = ∅) and are otherwise limited to p.φn or p− .φn . Expressions h are necessary to capture closed ShEx expressions and the closed construct of SHACL. Note that in Def. 9, the occurrences of ε are necessary to ensure that ShEx0 is a syntactic fragment of ShEx. We will omit them in the sequel, as ε is a neutral element for the ‘;’ operator. Definition 10 (SHACL0 ). SHACL0 is given by the grammar
The set of triple constraints of a shallow triple expression e, denoted tc(e), is the set of e’s sub-expressions of the form p.φ or p− .φ or (¬Q) or (¬R− ). We let preds(e) = {p | p.φ ∈ tc(e)} be the set of predicates that appear in e. For every p ∈ preds(e), and we let shapes(e, p) = {φ | p.φ ∈ tc(e)} be the shapes that appear in e with predicate p. Following (Staworko et al. 2015), triple expressions can be seen as regular expressions with commutative concatenation over an alphabet of triple constraints, where ‘;’ plays the role of concatenation. It is then easy to show that the following equivalences hold for all closed triple expressions f1 , f2 , f3 and for op = (¬R− )∗ ;(¬Q)∗ or op = (¬R− )∗ for some R, Q ⊆ IRIs:
φ ::= ⊤ ⊥ test(c) test(v) s closed(Q) ¬φ φ ∧ φ
(f1 ; f2 ) | f3 ≡ (f1 ; f3 ) |(f2 ; f3 ) , (f1 | f2 )∗ ≡ f1∗ ; f2∗ , (f1 | f2 ) ; op ≡ f1 ; op ∨ f2 ; op .
φ ∨ φ∃≥k p.φ ∃≥k p− .φ ∃≤k p.φ ∃≤k p− .φ . SHACL0 forbids the disj and eq constructs, as well as paths different from a single predicate. Proposition 3. (a) For every ShEx0 schema S = (C, sel ), there exists a SHACL0 schema S ′ = (C ′ , sel ) s.t. a graph G conforms to S iff G GFP-conforms to S ′ . Conversely, (b) for every SHACL0 schema S = (C, sel ), there exists a ShEx0 schema S ′ = (C ′ , sel ) s.t. a graph G GFP-conforms to S iff G conforms to S ′ .
Additionally, every triple expression f ;(¬R− )∗ ;(¬Q)∗ is equivalent to one in which preds(e) ⊆ R ∪ Q, and similarly for expressions without the (¬Q)∗ component, thanks to these equivalences:
These equivalences directly lead to an effective translation from ShEx0 shapes to equivalent SHACL0 shapes, and viceversa.
Now, for every triple constraint p.φ of e, we define
Using duality of least and greatest fixed points (Prop. 1), and the fact that ∃≥n p.φ is the dual of ∃≤n p.φ thanks to the equivalence ∃≤n π.φ ≡ ¬(∃≥n+1 π.φ), it easily follows that Corollary 1. SHACL0 under LFP semantics is equally expressive to ShEx0 .
Then det(e) is obtained by replacing in e every triple constraint p.φ by det(e, p.φ). The fact that det(e) is deterministic follows from preds(e) ⊆ R ∪ Q and from the definition of the Φe,p,X . Showing that e ≡ det(e) is not hard using the parallel between triple expressions and regular expressions with commutative concatenation.
A.2
Assume a fixed Restricted ShEx catalogue C and a fixed graph G. For every Restricted ShEx shape, we construct an equivalent ShEx0shape. The only non-trivial case is for shapes of the form e′ . We start by computing det(e′ ). Note that if e′ is a Restricted ShEx triple expression, then so is det(e′ ). In the sequel, let det(e′ ) = e = f ; op with op = (¬R− )∗ ;(¬Q)∗ for some R, Q ⊆ IRIs. The case without (¬Q)∗ is similar. Using the properties of ShEx from Sect. A.2 and the fact that e is Restricted ShEx, we can push the ‘;’ and ‘∗’ operators
f ;(¬R− )∗ ≡ f ; p− .{⊤}∗ ; (¬(R ∪ {p})− )∗ f ;(¬R− )∗ ;(¬Q)∗ ≡ f ; p.{⊤}∗ ; (¬R− )∗ ;(¬(Q ∪ {p}))∗
Normalisation In the sequel we show how Restricted ShEx shapes can be translated to ShEx0 shapes. Proof. We show how ShEx0 shapes can be translated to A triple expression e is called deterministic if for all assignequivalent SHACL0 shapes, and conversely. Then, for the ments α, graphs G, catalogues C, and triples (v, p, u) ∈ G, ′ ′ (a) direction of the proposition, we define C = {s : φ | s ∈ e contains at most one triple constraint t s.t. {(v, p, u)} ∈ dom(C) and φ′ ≡ φ} where φ is a ShEx shape and φ′ is a JtKα G,C , and contains at most one inverse triple constraint t SHACL shape, and conversely for the (b) direction. s.t. {(v, p− , u)} ∈ JtKα G,C . Every triple expression e can The following equivalences hold between ShEx0 shapes be effectively transformed into an equivalent deterministic (left-hand side) and SHACL0 shapes (right-hand side), asone det(e) as follows. Let e = f ;(¬R− )∗ ;(¬Q)∗ ; the case suming that the ShEx0 shape φ is equivalent to the SHACL0 where e = f ;(¬R− )∗ is similar. W.l.o.g. we assume that shape φ′ : preds(e) ⊆ R ∪ Q (see Sect. A.2). For every p ∈ preds(e) test(c) ≡ test(c) , test(v) ≡ test(v) , s ≡ s , ⊤ ≡ ⊤ , and every X ⊆ shapes(e, p), define the shape Φe,p,X : ∗ ∗ ^ ^ p1 . ⊤ ; · · · ; pn . ⊤ ;(¬∅− )∗ ≡ closed({p1 , . . . , pn }) , Φ = φ ∧ ¬φ e,p,X k − k p.φ ; ⊤ ≡ ∃≥k p.φ′ , p .φ ; ⊤ ≡ ∃≥k p− .φ′ . φ∈X φ∈shapes(e,p)\X
Normalisation of Restricted ShEx
Preliminaries on ShEx We start with a few definitions and properties regarding ShEx that are used in several proofs. A ShEx triple expression is called shallow if its sub-expressions of the form p.φ or p− .φ are such that φ is a Boolean combinations of shape names and expressions of the form test(c) and test(v) only. By adding a polynomial number of new shape definitions to its catalogue, every ShEx schema can be transformed into an equivalent one using only shallow triple expressions.
det(e, p.φ) =
—
X⊆shapes(e,p)|φ∈X
p.Φe,p,X .
under the ‘|’, then transform the top-level ‘|’ into disjunction. Thus, e ≡ F1 ; op ∨ · · · ∨ Fn′ ; op (1) with n′ ≥ 1 and where every Fj is a ‘;’ combination of triple constraints of the form p1 .Φ1 ; · · · ; pm .Φm ; pm+1 .Φ∗m+1 ; · · · ; pk .Φ∗k ,
(2)
for 0 ≤ m ≤ k (k = 0 means that the sequence is empty, thus reduces to ε). Let F be the triple expression (2). For every p.Φ triple constraint of F , let #(F, p.Φ) be the number of times p.Φ is repeated in F without a star (i.e. we do not count occurrences of p.Φ∗ ). Lemma 1. Let e = f ;(¬R− )∗ ;(¬Q)∗ be a deterministic triple expression with (for some 0 ≤ m ≤ k), where f is the expression (2) above. Then e is equivalent to the conjunction shape ^ Ψ= p.Φ#(f,p.Φ) ; ⊤ (3) p.Φ∈tc(f )
^
∧
¬ p.Φ1+#(f,p.Φ) ; ⊤
(4)
p.Φ∈tc(f ) s.t. p.Φ∗ ̸∈tc(f )
∧
^
¬ p.Φf,p,∅ ; ⊤
(5)
p∈preds(f )
∧
^
¬ p− . ⊤ ; ⊤
(6)
¬ p. ⊤ ; ⊤
(7)
p∈R\preds(f )
∧
^
Proof (sketch). Let (C, sel ) be a Restricted SHACL Schema. We only need to show how to eliminate expressions of the form ∃π.φ. We perform the following steps for all ∃π.φ that appear in C. 1. Take two fresh shape names s∃π.φ and sφ . 2. Add the shape declaration sφ : φ to C. 3. Replace each occurrence of ∃π.φ in C with s∃π.φ . 4. Construct a non-deterministic finite automaton A that accepts the language of π. For every state q of A, take a fresh shape name sq and add the following declarations to C: (a) s∃π.φ : sq0 ∨ · · · ∨ sqn where q0 , . . . , qn are the initial states of A, (b) sq : sφ for each accepting state q of A, and (c) sq : ∃r.sq′ for each transition (q, r, q ′ ) of A. The resulting set of shape declarations is denoted C ′ . It is straightforward to check that (C ′ , sel ) is a SHACL0 schema equivalent to (C, sel ). We can also note that the construction of C ′ takes only polynomial time in the size of C.
B
p∈Q\preds(f )
Proof. Let v be a node in G, and let N ′ be its neighbourhood. Because e is deterministic, it is not hard to seeUthat if N ′ ∈ ′ ′ JeKα G,v,C , then N is a disjoint union N = T ∈tc(f ) ET where, for every T ∈ tc(f ), ET is the set of triples from N ′ that match the triple constraint T . Additionally, |ET | = #(e, T ) if T ∗ does not appear in e, and |ET | ≥ #(e, T ) otherwise. Assume now that N ′ ∈ JΨKα G,C , and for every T ∈ tc(e), let ET′ ⊆ N ′ be the set of triples from N ′ that match the triple constraint T , and let E0′ ⊆ N ′ be the set of triples from N ′ that match none of the triple constraints ofUe. Because e is deterministic, we deduce that N ′ = E0 ⊎ T ∈tc(e) ET′ . The conjuncts (5), (6) and (7) guarantee that E0′ = ∅. The conjuncts (3) and (5) guarantee that |ET′ | ≥ #(e, T ), and together with the conjuncts (4) they guarantee that if T is not starred in e, then |ET′ | = #(e, T ). From these observations ′ α it easily follows that N ′ ∈ JeKα G,C iff N ∈ JΨKG,C . Note that the formula Ψ in Lemma 1 is ShEx0 . Therefore, we have shown Proposition 4. Every Restricted ShEx schema is equivalent to a ShEx0 schema.
A.3
additional shape declarations, thus obtaining a schema matching Def. 10. See Proposition 7 in (Oudshoorn, Ortiz, and ǐmkus 2024) for a similar approach. Proposition 5. Under the LFP semantics, every Restricted SHACL schema is equivalent to a SHACL0 schema.
Normalisation of Restricted SHACL
In this section, we relate Def. 8 and Def. 10. Specifically, we argue that, under the LFP semantics, complex path expressions as allowed in Def. 8 can be eliminated by adding
NP-Hardness of SMS for stratified SSL
We provide an alternative proof of NP-hardness of validation under SMS for a fixed stratified SSL schema (and thus also for a fixed stratified SHACL schema). We reduce from 3COLOURABILITY. For a directed graph H, we construct an RDF graph GH and a stratified SSL catalogue C (independent from H) such that H is 3-colourable iff GH SMS-conforms to the schema (C, {Ok : test(s)}). We first describe GH . We use predicate edge to represent the edges of H: for every edge (u, v) of H, we add to GH the triple (u, edge, v). We use predicate self for self-loops, which are used to generate arbitrary colourings of H: for each node v of H, we add to GI the triple (v, self, v). Finally, we add a fresh apex node s that serves as a spy-point, observing all nodes of H via predicate spy: for each node v of H, we add to GH the triple (s, spy, v). The catalogue C contains the following declarations: Colour i : ∃self.Colour i , Error :
3 ^
¬Colour i ∨
i=1
1≤i≤3 3 _
Colour i ∧ ∃edge.Colour i
i=1
Ok : ¬∃spy.Error . To see that the reduction is correct, observe that in a correct shape assignment, shape name Colour i can be assigned to an arbitrary subset of nodes of H, which is how we guess a colouring of H. An error is detected in a node if it gets no colour or it has the same colour as one of its neighbours. Finally, Ok can be assigned to the spy point s iff no error is detected in any of the spied nodes.
C
Proof of Theorem 3 NP
that encodes a valuation satisfying φ. The reduction is inspired in the P NP -hardness proof for stratified logic programs under bounded predicates arities (Eiter et al. 2007). Let φ be a satisfiable 3CNF formula with clauses c1 , . . . , ck over ordered variables x1 , . . . , xn . We shall construct an instance of the validation problem that will simulate an algorithm that solves our P NP -complete problem by iteratively computing values of variables in the lexicographically maximal valuation satisfying φ using satisfiability tests. In iteration 1 we check if φ is satisfiable with x1 = 1, and store the outcome in t1 . In iteration i we check if φ is satisfiable with x1 = t1 , . . . , xi−1 = ti−1 , xi = 1, and store the outcome in ti . After iteration n, t1 , . . . , tn store the lexicographically maximal valuation satisfying φ. It suffices to check tn . The reduction is similar to the one for SMS, but this time there are no variables y1 , . . . , ym , and the values of x1 , . . . , xn are iteratively determined, rather than guessed. We use predicates c1 , . . . , ck and x1 , . . . , xn , like before, and shape names t1 , . . . , tn and s1 , . . . , sn , corresponding to subsequent iterations. The shape catalogue contains the following declarations, for i = 1, 2, . . . , n:
We begin with SMS. For the NP upper bound we guess a shape assignment and verify that it is correct and witnesses conformance. These checks can be done easily in P, when given access to an oracle that answers if the neighbourhood of a given node matches a given triple expression. This we can assume in NP NP , because the subproblem can be solved in NP by guessing an ordering of edges in the neighbourhood into a sequence, and feeding it to the nondeterministic automaton constructed (in P) from the triple expression. For the lower bound we use the following variant of the standard NP NP -complete problem, ∃∀SAT: Given an CNF propositional formula over variables x̄ and ȳ, decide if there is a valuation of x̄ such that for each valuation of ȳ the formula is false. Let us fix a CNF formula with clauses c1 , c2 , . . . , cn over variables x1 , x2 , . . . , xk and y1 , y2 , . . . , yℓ . We will be using c1 , c2 , . . . , cn and x1 , x2 , . . . , xk as predicates (edge labels). The input graph is a (k + n)-pointed star with self-loops: it consists of a central node a with an outgoing ci -edge for i = 1, 2, . . . , n and an outgoing xi -edge for i = 1, 2, . . . , k; the target of each xi -edge has a self-loop with label p. ti : x1 .si ; ex1 | x1 .¬si ; e¬x1 ; The catalogue consists of two declarations, s : {p.s ; ⊤} . . . ; xi−1 .si ; exi−1 | xi−1 .¬si ; e¬xi−1 ; and xi .{⊤} ; exi ; t : ¬ x1 .s ; ex1 | x1 .¬s ; e¬x1 ; . . . ; xk .s ; exk | xk .¬s ; e¬xk ; xi+1 .{⊤} ; exi+1 | e¬xi+1 ; . . . ; xn .{⊤} ; exn | e¬xn − ey1 | e¬y1 ; . . . ; eyℓ | e¬yℓ − si : x1 .t1 | . . . | xi−1 .ti−1
where the triple expression eL for literal L is obtained by combining with ‘;’ all expressions ci .{⊤}∗ such that ci contains literal L. The schema has a single selector t : test(a). In a correct shape assignment, the shape name s is associated with any subset of xi -successors of a, thereby fixing a valuation of x1 , x2 , . . . , xk . In order to check if the neighbourhood of a matches the triple expression e in the declaration of t, we guess the left or right argument of | in each parenthesis. This corresponds to guessing a valuation of all variables. However, once a correct assignment α is fixed, in expressions of the form (xi .s ; exi | xi .¬s ; e¬xi ) we have to follow the choice dictated by α, and we have actual choice only for variables y1 , y2 , . . . , yℓ . Once all choices are made, the neighbourhood matches the resulting triple expression e′ if e′ mentions each ci .{⊤}∗ at least once (we interpret all but one occurrence as ε). Hence, the graph is valid if there exists a valuation of x1 , x2 , . . . , xk such that for all valuations of y1 , y2 , . . . , yℓ , at least one ci .{⊤}∗ is not mentioned in the triple expression e′ induced by the valuations. By the definition of eL , the latter holds iff the formula is false. Let us move to LFP and GFP. For the P NP upper bound we iterate the suitable operator as explained in the proof of Theorem 2, except that we use an NP oracle for testing if the neighbourhood of a given node matches a given triple expression. For the lower bound we use the following P NP -complete problem: given a satisfiable 3CNF formula φ over ordered variables x1 , . . . , xn , decide if xn = 1 in the lexicographically maximal valuation that satisfies φ. In other words, we need to check if 1 is the last bit of the maximal n-bit number
Note that the catalogue is non-recursive, so the LFP and GFP semantics coincide (Proposition 6). The graph is a (k + n)-pointed star: it consists of a central node a with an outgoing xi -edge for i = 1, 2, . . . n and an outgoing ci edge for i = 1, 2, . . . k. The schema has a single selector tn : test(a). One can verify that φ is a positive instance of the problem iff the graph LFP/GFP-conforms to the schema. Proposition 6. For non-recursive catalogues LFP, GFP, bSMS, and cSMS semantics coincide. Proof sketch. For such schemas, the initial shape assignment is effectively irrelevant, since you can rewrite the schema into an equivalent one where no shape depends on another. This is done by substituting shape names used in shapes with their declared definitions. In consequence, there is only one correct shape assignment.