arXiv CSopen access

Transforming Shape Schemas with Composable Property-Graph Queries (Extended Version)

Transforming Shape Schemas with Composable Property-Graph Queries (Extended Version) Philipp Seifer1 , Daniel Hernández2 , Ralf Lämmel1 , and Steffen Staab2,3

arXiv:2606.14309v1 [cs.DB] 12 Jun 2026

1

The Software Languages Team, University of Koblenz, Germany, {pseifer, laemmel}@uni-koblenz.de 2 Institute for Artificial Intelligence, University of Stuttgart, Germany, {daniel.hernandez,steffen.staab}@ki.uni-stuttgart.de 3 University of Southampton, UK June 15, 2026 Abstract

Property graphs may be constrained by schemas that inform both query engines and human users about the shape of valid data, enforcing a contract between data provider and consumer. Composable property-graph queries transform input graphs into output graphs. Then, the question arises of which schema can be expected after one (or several) transformation steps. We investigate how schema constraints can be inferred given an input schema and a transforming query. Specifically, we propose a reasoning procedure that, given an input schema in ProGS and a query in G-CORE infers an output schema. Since graph updates will happen frequently, our inference procedure does not rely on graph instances, such that the computed output schema applies to all graphs originating from any input graph complying with the input schema. Related work has addressed this problem for SPARQL CONSTRUCT queries, encoding it in Description Logics (DLs) so that the output schema is entailed by axioms inferred from input schema and queries. Property graphs and their queries, however, complicate the matter, as property graphs feature label and property annotations as well as first-class edges. Thus, reification has to be used in one way or another, though available DLs lack the means to encode such features directly. We approach this novel challenge via a family of mappings for i) property graphs reified in RDF, aligned with ii) a mapping from ProGS to SHACL and iii) a mapping from G-CORE to SPARQL CONSTRUCT queries. In this manner, schema inference for property graphs becomes manageable, as we break apart the problem through the extra mapping layer and utilize efficient DL reasoners. We develop the metatheory regarding the soundness of inferred schema constraints and the semantic equivalence of mapped schemas and queries.

1

Introduction

Composable property-graph queries transform graphs into graphs. In this paper, we are interested in schema inference for the results of such composable queries. For RDF graphs, the W3C proposes a composable query language, namely SPARQL [18] with its CONSTRUCT [27] clause. For property graphs (PGs), which we aim at in this paper, the recent GQL [21] standard is not composable (as yet [23]). Accordingly, we leverage G-CORE [3], an earlier composable query language for property graphs that inspired GQL. Property-graph schemas are used to constrain PGs; the constraints can be enforced by validation. There are schema languages, sometimes also called shape languages, for PGs, such as the Property Graph Shapes Language (ProGS) [44] or PG-Schema [4]. As far as schema constraints of the inference approach in this paper are concerned, both ProGS and PG-Schema are viable candidates. Pragmatically, we commit to ProGS, as it is more directly aligned with the established schema language for RDF, i.e. SHACL [26], which is readily covered by the foundation we rely on. In particular, the correspondence between SHACL and description logics (DL) is well understood [40, 8]. Thus, we can leverage efficient reasoner implementations for inference. We follow the terminology of ProGS and SHACL and refer to schemas as shapes. We refer to shapes validating all possible result graphs of a query as output shapes. Similarly, we use the term input shapes to refer to the set of shapes over the input graphs of a query. The inference of output shapes is a challenging aspect of the composable query notion: input shapes do not carry over directly to the output but do indeed impact it. Additionally, to obtain sound shapes for all possible query results, inference must rely on the input shapes and the query as inputs rather than individual result graphs. Access to these statically inferred shapes facilitates numerous use cases, even when considering compositions of multiple queries: they enable tools such as type systems for language-embedded queries (compare [30]) among others (e.g., [50, 35]) that rely on shapes. For query pipelines that are executed repeatedly, such shapes need only be inferred once, which is particularly useful in cases where some level of manual review or selection of shapes is desired. Finally, even in data transformation or integration use cases, where result graphs are stored in databases, they complement shapes inferred from graph instances and can provide insights to developers without query execution. ProGS Sin

PG G1i . . . Gni

G-CORE q

PG G1o . . . Gno

ProGS Sout

k Figure 1 Schematic overview of the problem: Input shapes Sin validate a (possibly infinite) set of input graphs G1i . . . Gn i which are valid inputs for the query q. The query produces, as its result, a set of corresponding result graphs G1o . . . Gn o . Just as Sin validates all input graphs, Sout validates all output graphs. The set of Sout is constructed from some formalization k, which is derived from Sin and q.

Figure 1 shows the input (shapes Sin and query q) and the output (shapes Sout ) of shape inference, with the respective languages annotated in blue. For these languages, we will later define the relevant subsets we consider in this work. The figure also hints in gray at the set of input graphs (conforming to shapes Sin , indicated by gray double lines) and corresponding output graphs (conforming to Sout ), with black arrows representing input and output of query execution. These graphs are included in the figure only for the sake of clarity; our approach does not depend on any concrete graphs. Our approach is rendered using blue arrows: we encode in k the information that allows us to deduce which shapes are in Sout . 2

To introduce k, we establish a common language that can express the constraints of the input shapes Sin and how inputs and outputs relate to each other over the query q. Given such a language, we then define an algorithm for constructing k from both Sin and the query q and for inferring the new shapes in Sout from k. ProGS Sin

PG G1i . . . Gni

PG G1o . . . Gno

G-CORE q k1 DL

ProGS Sout

k2 DL

Figure 2 Schematic overview of a possible solution where constraints are encoded in description logics.

One possibility for encoding these constraints is description logics (DL). Figure 2 indicates where DL is used with red arrows: we first encode the input shapes Sin as a set of DL axioms and then combine them with a second set of axioms inferred from the query q. This approach benefits from relying on an existing formalism and, in practical applications, from established and efficient reasoners for implementing the required decision procedures. In prior work [40], we also relied on a DL to solve a similar inference problem for RDF graphs and SPARQL CONSTRUCT queries. However, there is a drawback: Common DLs do not support properties with key-value annotations. Thus, we would have to either define a new variant — for which no efficient reasoners exist — or we have to use some form of reification to encode properties in an existing DL. Since the first option is not desirable, we choose the second. However, instead of encoding reification directly in DL, we introduce an intermediate RDF layer. This provides the following benefits: foremost, it clearly separates the reification from the DL encoding and inference steps of our solution, making each part easier to formalize, prove, and implement. Secondly, we can build on the aforementioned prior work for the encoding and inference step; we still need to modify and extend the algorithm. Finally, a mapping between the involved shape and query languages has not been formally explored, which we achieve in this work. ProGS Sin

PG G1i . . . Gni k1 DL

′ Sin SHACL

1

G′i . . . G′i RDF

n

PG G1o . . . Gno

G-CORE q

ProGS Sout

k2 DL q′ SPARQL

1

G′o . . . G′o RDF

n

′ Sout SHACL

Figure 3 Schematic overview of the involved languages, mappings, and algorithms. The upper PG layer is mapped to the bottom RDF layer, where individual mappings are indicated using dotted lines. Inference and reasoning exclusively operate on RDF. The blue arrows show how mappings are utilized.

Figure 3 shows the full solution we propose. Utilizing reification (indicated with dotted lines) at all levels allows us to step down from a PG-based language family (upper half of Figure 3) to an RDF-based one (lower half of Figure 3). We use RDF for representing the data by reifying firstclass edges with identities and properties in PG as ordinary RDF triples. We use SHACL as the shape language, accounting for this reification. This allows us to rely on DL for the formalization and implementation of shape inference, since round tripping between DL axioms and SHACL shapes is possible (cf. [40, 8]). Finally, we use SPARQL CONSTRUCT as the composable query 3

language to which we map. Here, the definition of a sound mapping is more complex, since in addition to the reification, we must also account for the differences in query language semantics: where labels and properties are copied by default in G-CORE and explicitly removed, SPARQL relies on explicit triple patterns and filters. The data reification, shape-to-DL mapping, and shape inference approaches have been studied [24, 4, 40], whereas the query mapping has not. We build on and extend our existing algorithm [40] that infers SHACL shapes for results of SPARQL CONSTRUCT queries on RDF graphs by constructing a DL knowledge base entailing valid output shapes. To define our query mapping, we must extend the SPARQL fragment considered in [40] with more generic triple patterns where variables extend over concept or role names to capture the semantic properties of G-CORE. This leads to a number of required adaptations of the method presented in this work, since the knowledge base must encode the potential presence of previously unexpected concept or role names. The dataflow of the extension to [40] is indicated by red arrows in Figure 3. It is important to note that our mapping approach serves the formalization and implementation of schema inference; whether the queries are executed on a PG database or an RDF store is a separate question.

1.1

Contributions

In summary, the contributions of this paper are as follows: 1. We determine the impact of PG-specific expressiveness when it comes to shape inference for composable graph queries. Thus, we handle edges that have identities, as well as nodes and edges annotated with labels and key-value properties that persist, implicitly, in results. 2. Despite common DLs lacking the corresponding language constructs, we resolve the mismatch through reification, which carries over to structures of shapes and queries. 3. Instead of reification at the DL level, we define an intermediate layer, introducing mappings from ProGS to SHACL and G-CORE to SPARQL CONSTRUCT over PGs reified in RDF. 4. We develop the metatheory regarding the soundness of inferred shapes and the semantic equivalence of mapped shapes and queries.

1.2

Roadmap of the Paper

Section 2 introduces the underlying formalisms, as well as our running examples. In Section 3, we formalize the essential problem addressed in this work. Section 4 and Section 5 solve the problem in two steps: first, we develop a family of mappings from property graph abstractions to RDF graph abstractions (Section 4). On these grounds, we develop an inference method, which is an extension of [40] (Section 5). Section 6 develops the corresponding metatheory. In Section 7, we briefly outline our prototype implementation of this approach. Finally, Section 8 discusses related work while Section 9 concludes the paper. Several appendices are referenced by the paper for additional details, such as extended examples and full proofs.

2

Foundations

We first introduce the graph data models, query languages, and shape-based validation languages relevant to our work; they can be separated into two groups, namely PG-related languages and RDF-related languages pertaining to the upper and lower layers of Figure 3. 4

2.1

RDF Graphs

We define RDF graphs based on the W3C specification [13], excluding blank nodes and literals; we consider the latter as ordinary IRIs to simplify the formalization of the data model. We assume four pairwise disjoint, finite1 but arbitrary, and sufficiently large sets of IRIs, namely concept names C, individual names I, role names R, and the special role name {rdf:type}. For the sake of consistency, we use description-logic terminology throughout all abstractions (e.g., concept name instead of class). Commonly, RDF uses so-called prefixes to abbreviate (parts of) IRIs. In formal definitions, we express most IRIs through ordinary symbols, with a few exceptions, such as rdf:type. In examples, we also omit prefixes for the example domain; that is, we simply write Agent instead of ex:Agent. Similarly, we sometimes write a instead of rdf:type. Definition 1 (Simple RDF Graph). An RDF graph G is a finite set of triples of the form (a, p, b) or (a, rdf:type, A) where a, b ∈ I, A ∈ C, and p ∈ R. Example 2. Consider the following set of triples as an example RDF graph Grdf = 1 {(s, a, Agent), (s, name, Smith), (p, a, Person), (s, obs, p)}. 2.1.1

Agent

a

s

obs

p

a

Person

name

Smith

SPARQL Queries

We define a subset of SPARQL queries referred to as Extended Conjunctive CONSTRUCT Queries (ECCQ) in analogy to Simple Conjunctive CONSTRUCT Queries (as defined in [40]) in Definition 3. We choose this conjunctive fragment, as is commonly done, to keep the scope of our algorithms manageable; we extend2 the fragment of SPARQL chosen in [40] with the language features required for our intended mappings. To this end, we introduce generic patterns such as x : y, written ?x a ?y in concrete SPARQL syntax, where both x and y are variables. Here, we need to introduce an additional syntactic restriction for generic variables, as we will discuss in more depth later: if the query includes the atomic query pattern x : y, then y must not occur again in another atomic query pattern. That is, we can copy all concept names of x generically but cannot introduce restrictions on this meta level; for example, a query with patterns {x : y, z : y} is not allowed, since it would constrain the bindings of x and z through y. Thus, we write x : xC to indicate that the generic variable xC is syntactically dependent on x in this way. We also introduce certain filter expressions for only these generic variables written xC , filtering certain concept or role names from their bindings. Definition 3 (Syntax of ECCQ). We define atomic patterns t and filter expressions f as follows: t ::= x : A | (x, y) : p | (x, a) : p | x : xC | (x, xI ) : xR

f ::= xC ̸= A | xR ̸= p

with A ∈ C, a ∈ I, p ∈ R, and variables x, y, xC , xR , xI ∈ V. Let the function vars denote the set of all variables that occur in a set of atomic patterns or filter expressions. An ECCQ q is defined as H ← (P, F ) where template H and pattern P consist of finite sets of atomic patterns t and the filters F of a finite set of filter expressions f such that vars(F ) ⊆ vars(P ). For each 1 This is not a restriction to the problem, since the sets are arbitrary, but it simplifies a few definitions. 2 ECCQ is not a true extension of the language presented in [40], since we omit certain patterns, e.g., a : C. While they could be easily included, making ECCQ a true extension of this language, they are not required for the remainder of this work.

5

atomic pattern x : xC (and similarly (x, xI ) : xR ), there is a unique variable xC (similarly xR and xI ) per ordinary variable x, which does not occur again in the query, except in filter conditions. If a generic atomic pattern of this form occurs in H, the same pattern must also occur in P . To formalize the semantics of ECCQ in Definition 4, we define valuations µ : V → I ∪ C ∪ R as mappings from variables to individual, concept, and role names. Note that the syntactic restrictions on xC and xR ensure that the respective types of these bindings cannot be mixed up, since these variables can only occur in the correct context. Two valuations µ1 and µ2 are compatible, denoted µ1 ∼ µ2 , if for every variable x occurring in both µ1 and µ2 , µ1 (x) = µ2 (x). A finite set of valuations is denoted Ω. We define the join of two sets of valuations Ω1 and Ω2 as Ω1 ▷◁ Ω2 = {µ1 ∪ µ2 | µ1 ∈ Ω1 , µ2 ∈ Ω2 , µ1 ∼ µ2 }. Note that in Definition 3 we do not include the usual syntactic restriction vars(H) ⊆ vars(P ). We therefore need the final clause in Definition 4 about variables from atomic patterns t ∈ H that do not occur in vars(P ). Here, we assume the generation of fresh IRIs for such variables, which will be required by our mappings later. While this is a deviation from ordinary SPARQL semantics3 , our variant simplifies the formalization by avoiding the need to represent blank nodes in our RDF graph model and throughout the paper. In practical implementations, ordinary blank nodes should be used to comply with standard SPARQL semantics; indeed, our implementation generates SPARQL queries featuring blank node identifiers in their templates as well. Definition 4 (Semantics of ECCQ). The result of evaluating an ECCQ H ← (P, F ) over an RDF graph G is the RDF graph denoted JH ← (P, F )Keccq and defined as G , t ∈ H} = {µ(t) | µ ∈ JP, F Keccq-p JH ← (P, F )Keccq G G

where JP, F Keccq-p = {µ | µ ∈ ▷◁t∈P JtKeccq-a , for all f ∈ F : µ ⊢ f } and JtKeccq-a = {µ | µ(t) ∈ G G G G}. f is a filter condition such that µ ⊢ (xC ̸= A) is true iff µ(xC ) is not A, and µ ⊢ (xR ̸= p) is true iff µ(xR ) is not p. In a slight abuse of notation, we write µ(t) to mean µ(u : A) = (µ(u), rdf:type, A), and similarly for the remaining cases. If a variable x in t ∈ H does not occur in vars(P ), then µ(x) produces a fresh IRI. This IRI is unique for each variable x and each unique mapping µ. Example 5. Consider the ECCQ q1eccq = {x : Agent, y : POI} ← ({(x, y) : obs}, {}), selecting pairs of observers and observed before constructing a new graph labeling observers as Agent and observed as POI. When evaluating this query on graph Grdf from Example 2, 1 written Jq1eccq KGrdf , we first match the pattern P on the graph, re1 sulting in the single mapping µ where µ(x) = s and µ(y) = p. Thus, the template H is instantiated only once, namely for µ, resulting in the graph {(s, a, Agent), (p, a, POI)}. Using generic patterns, we could, in this particular case, rewrite the query as {x : xC , y : POI} ← ({x : xC , (x, y) : obs}, {}), copying all concepts for bindings for x instead of explicitly adding Agent. Since s has only the concept Agent in q1eccq , evaluation would yield the same result graph. 2.1.2

s

a

Agent

p

a

POI

SHACL Shapes

SHACL is a validation language for RDF graphs, where a shape consists of two components: the target query selecting a subset of nodes and a constraint these nodes must conform to. We 3 Usually, SPARQL CONSTRUCT templates can feature blank node identifiers (https://www.w3.org/TR/ sparql12-query/#templatesWithBNodes) to this effect.

6

present here the Seifer et al. [40] definition of SHACL shapes, utilizing description logics to define the semantics of target queries and constraints based on work by Bogaerts et al. [8]. According to this definition, SHACL shapes are ALCHOI axioms, i.e. target query subsumed by the constraint, both encoded as concept descriptions (definition 6), and their semantics can be reduced to checking consistency with a validation knowledge base constructed for a given RDF graph G by its unique-name, closed-world, and domain-closure assumptions. We refer to [7] for the definition of the semantics of ALCHOI. We give here the syntax of ALCHOI axioms, which can express a subset of SHACL, and the core idea of the validation semantics introduced in [40]; we refer to that paper for the full derivation and proofs. Definition 6 (ALCHOI Axioms). Concept descriptions are defined as follows: C ::= ⊤ | ⊥ | A | {a} | C ⊓ C | C ⊔ C | ¬C | ∃ρ.C | ∀ρ.C ρ ::= p | p− where A, a, and p stand for concept names, individual names, and role names, respectively, and ⊤ and ⊥ are two special concept names. Given two concept descriptions C and D, and two role descriptions ρ1 and ρ2 , C ⊑ D and ρ1 ⊑ ρ2 are ALCHOI axioms, which we also call shapes. The left-hand side (C and ρ1 ) we also call the target and the right-hand side (D and ρ2 ) the constraint of the shape. Semantically, SHACL shapes target specific nodes of a graph, relying on constraints to validate these selected nodes. A consistency check for the subsumption axioms defined in Definition 6 with the validation knowledge base constructed for a given RDF graph G (Definition 7) encodes these semantics. Example 8 demonstrates the intuition. Definition 7 (Validation Semantics (Adapted from [40])). The axioms of a simple RDF graph G, denoted TG , are the TBox consisting of the following ALCHOI axioms: F 1. Domain Closure Assumption (DCA): ⊤ ≡ a∈I {a}. 2. Unique Name Assumption (UNA): {a} ⊓ {b} ≡ ⊥, for each pair of distinct individual names a, b ∈ I. 3. Closed-World Assumption (CWA): F • A ≡ a : A∈G {a}, for each concept name A ∈ C, F • ∃p.{a} ≡ (b,a) : p∈G {b}, and F • ∃p− .{a} ≡ (a,b) : p∈G {b}, for each role name p ∈ R and each individual name a ∈ I. (TG , G) is the validation knowledge base of G. A graph G is proof-valid according to a set Σ of ALCHOI axioms if and only if Σ is consistent with the validation knowledge base of G, i.e. the knowledge base (TG ∪ Σ, G) admits a model. We write valid(G, S) to indicate that G is proof-valid regarding the set of shapes S and valid(G, s) to indicate that G is proof-valid regarding a single shape s. We use S and Σ interchangeably. In Example 8 we give an example shape and outline both the intuitive reason why this shape validates the running example graph and the formal reason considering the validation knowledge base.

7

Example 8. Consider sshacl = Agent ⊑ ∃obs.Person as an example. Intuitively, the shape 1 (Example 2) is valid expresses that all agents must observe at least one person. The graph Grdf 1 regarding sshacl since all targets, i.e. s, which is an instance of Agent, conform to the constraint, 1 given both (s, obs, p) ∈ Grdf and (p, a, Person) ∈ Grdf 1 1 . The validation knowledge base, constructed from the closed-world (Agent ≡ {s}, Person ≡ {p}, ∃obs.{p} ≡ {s}, and ∃obs− .{s} ≡ {p}), domain-closure ({s} ⊔ {p} ≡ ⊤), and unique-name assumptions ({s}⊓{p} ≡ ⊥) for Grdf is consistent with this subsumption axiom, too: essentially, 1 there is the concept {s} which is equal to Agent, and also the range of obs; in turn, the domain of obs is {p}, which is also equal to Person.

2.2

Property Graphs

Property graphs (Definition 9) differ from RDF graphs in that edges have identities, and both nodes and edges can be annotated with sets of labels and sets of key-value pairs, the so-called properties. There are various notions of property graphs; we base our work largely on [3], that is, the graph model used for G-CORE, which is very similar to the graph model used in the context of Cypher4 as well. We do not include first-class paths, however. We define a set of labels L = LN ∪ LE where LN is a finite set of node labels and LE a finite set of edge labels; a finite set of property names (or keys) K = KN ∪ KE where KN is a finite set of node keys and KE a finite set of edge keys; and a finite set of literal values V . Without loss of generality, we assume that literal values are strings. Finally, let FS(s) denote all finite subsets of a set s, including the empty set. See Example 10 for the running example PG. Definition 9 (Property Graph). A property graph (PG) is a tuple G = (N, E, ρ, λ, σ). N and E denote two disjoint, finite sets of node and edge identifiers, respectively. We write n ∈ N , e ∈ E, and u ∈ N ∪E. ρ : E → (N ×N ) is a total function assigning edges to nodes; λ : (N ∪E) → FS(L) is a total function assigning labels to nodes or edges; and σ : (N ∪ E) × K → FS(V ) is a total function assigning properties to nodes or edges and for which a set of tuples (x, k) ∈ (N ∪ E) × K exists such that σ(x, k) ̸= ∅. Example 10. Consider Gpg 1 = (N1 , E1 , ρ1 , λ1 , σ1 ), where N1 = {1, 2} and E1 = {10} are the sets of node and edge IDs. A single edge is defined as ρ1 (10) = (1, 2). Labels are defined as λ1 (1) = {Agent }, λ1 (2) = {Person }, and λ1 (10) = {obs }. Finally, we give the non-empty cases for the property function as σ1 (1, name) = {"Smith"} and σ1 (10, since) = {"2002"}. Compare this graph to the RDF graph Grdf in Example 2: RDF 1 graphs do not support properties on edges; thus, there is no direct equivalent for σ1 (10, since) = {"2002"} in RDF. Otherwise, the graphs are equivalent. 2.2.1

1 :Agent name: "Smith" 10 :obs since: "2002" 2 :Person

Property Graph Queries

Composable property graph queries return graphs and function similarly to ECCQ queries. We define Simple G-CORE Queries (SGCQ) as a subset of G-CORE [3]. Our conjunctive fragment (definition 11) supports matching multiple atomic patterns, including the most common constraints on labels and properties, and constructing a new graph from multiple atomic patterns 4 https://opencypher.org/

8

while explicitly adding or removing labels and properties. In short, the fragment allows for selecting a subgraph, reshaping it, and adding constant elements. It does not support whole-graph operations, such as the union of a constructed graph with the original graph. The basic semantics of SGCQ are similar to ECCQ: a pattern Γ defines variables and constrains their bindings through clauses ξ. These bindings are used to construct a new graph, specified in the template B, together with set (⊕) and remove (⊖) clauses for explicitly adding or removing labels and properties. Unlike in the case of ECCQ, labels and properties persist in the result graph by default. We give here in short the syntax and semantics of SGCQ adapted from [3], with the following change: since we allow only for a subset of filter expressions, we push these filters into the node (or edge) pattern. This is equivalent to the concrete syntax of G-CORE where we would write, e.g., (x:Person) to filter all nodes x for the label Person. Definition 11 (Syntax of SGCQ). A SGCQ B ⇐ Γ consists of a set Γ of atomic components γ ( pattern) and a set B of atomic components β ( template), defined by the following grammar: γ ::= (xn , ξ) | (xn , xn ):(xe , ξ)

β ::= (xn , S) | (xn , xn ):(xe , S)

Here, xn is a node variable, and xe is an edge variable. ξ is a set of expressions of the form :l, .k, or .k = v, where l ∈ L is a label, k ∈ K is a property name, and v ∈ V is a property value. S is a set of assignments for setting (⊕l and ⊕k = v) or removing (⊖l and ⊖k) labels or property names. We also write SL for referring to operations involving labels and SP for referring to operations involving properties. Furthermore, we write, e.g., ⊖x l ∈ B to indicate that (x, S) ∈ B and ⊖l ∈ S. As an additional syntactical constraint of the template, edge variables that occur in the pattern may only occur when their associated node variables also occur in the template. For the semantics of SGCQ, we again consider valuations µ on node or edge variables xn or xe , so that µ(xn ) ∈ N and µ(xe ) ∈ E, and similar definitions for compatibility ∼ and the join operation ▷◁ as for ECCQ. We also define the union of two PGs G1 ∪ G2 as (N1 ∪ N2 , E1 ∪ E2 , ρ, λ, σ) where ∀e ∈ E1 ∪ E2 : ρ(e) = ρ1 (e) if e ∈ E1 else ρ2 (e), ∀x ∈ N1 ∪ N2 ∪ E1 ∪ E2 , k ∈ K : λ(x) = λ1 (x) ∪ λ2 (x), and σ(x, k) = σ1 (x, k) ∪ σ2 (x, k). The semantics for evaluating G-CORE queries is given in Definition 12, with the intuition outlined in Example 15. Definition 12 (Semantics of SGCQ). The result of evaluating a SGCQ g = B ⇐ Γ over a PG G is defined as the PG constructed by JqKsgcq = JBKsgcq-t where Ω = JΓKsgcq-p . G Ω,G G That is, similarly to ECCQ queries, sets of bindings Ω are constructed from the pattern and fill out the template. JΓKsgcq-p and JBKsgcq-t are specified in Definition 13 and Definition 14 based G Ω,G on [3], respectively. Definition 13 (SGCQ Pattern Semantics). The set of bindings Ω resulting from evaluation of a SGCQ pattern Γ over a graph G, written JΓKsgcq-p , is defined by the following cases: G J(x, ξ)Ksgcq-p = {µ | µ(x) ∈ N, G

∀ξi ∈ ξ : Jξi Ksgcq-e µ(x),G = ⊤}

J(x, y):(z, ξ)Ksgcq-p = {µ | µ(x), µ(y) ∈ N, µ(z) ∈ E, G ρ(µ(z)) = (µ(x), µ(y)),

∀ξi ∈ ξ : Jξi Ksgcq-e µ(z),G = ⊤}

JΓKsgcq-p = ▷◁γ∈Γ JγKsgcq-p G G

9

J :lKsgcq-e = ⊤ iff l ∈ λ(u) u,G

J .kKsgcq-e = ⊤ iff σ(u, k) ̸= ∅ u,G

J .k = vKsgcq-e = ⊤ iff v ∈ σ(u, k) u,G

Definition 14 (SGCQ Template Semantics). Evaluation of a SGCQ template B over a graph G, with bindings Ω, written JBKsgcq-t Ω,G , is defined by the following cases: sgcq-s J(x, S)Ksgcq-t = {{v}, ∅, ∅, JSL Ksgcq-s µ,G v,G , JSP Kv,G }

sgcq-s J(x, y):(z, S)Ksgcq-t = {{v, u}, {e}, {e→ (v, u)}, JSL Ksgcq-s e,G , JSP Ke,G } µ,G sgcq-t JBKsgcq-t Ω,G = ∪β∈B,µ∈Ω JβKµ,G

where v = µ(x), u = µ(y), and e = µ(z) if the variables are in the domain of µ, or fresh identities otherwise. Evaluation of set and remove clauses is defined as JSL Ksgcq-s oN ,G = (λoN ∪ {oN→ lN | ⊕lN ∈ SL })\{oN→ lN | ⊖lN ∈ SL }

′ JSP Ksgcq-s oN ,G = (σ ∪ σ⊕ )\σ⊖

where σ ′ = {(oN , kN )→ v | (oN , kN )→ v ∈ σ ∧ (oN , kN )→ v ′ ̸∈ σ⊕ } σ⊕ = {(oN , kN )→ v | ⊕kN = v ∈ SP } σ⊖ = {(oN , kN )→ v | (oN , kN )→ v ∈ σ ∧ ⊖kN ∈ SP } Example 15. Recall the ECCQ q1eccq from Example 5. A seemingly similar SGCQ could be defined as q0sgcq = {(x, {⊕Agent}), (y, {⊕POI})} ⇐ {(x, y):(e, { :obs})} Evaluating Jq0sgcq Ksgcq (cf. Example 10) produces first the single mapping Gpg 1 µ with µ(x) = 1, µ(y) = 2, and µ(e) = 10; then, the template constructs the graph Gpg 0 = ({1, 2}, ∅, ∅, λ0 , σ0 ) with λ0 (1) = {Agent}, λ0 (2) = {Person, POI}, and σ0 (1, name) = {"Smith"}. That is, all labels and properties persist in the output graph. The following update to q0sgcq has equivalent semantics to the ECCQ query:

1 :Agent

2 :POI

q1sgcq = {(x, {⊖name}), (y, {⊕POI, ⊖Person})} ⇐ {(x, y):(e, { :obs})} Evaluation produces the graph ({1, 2}, ∅, ∅, λ1 , ∅) with λ1 (1) = {Agent} and λ1 (2) = {POI}, as we would expect (cf. Example 5). 2.2.2

Simple Property Graph Shapes (sProGS)

We define the syntax and semantics of a subset of the Property Graphs Shapes Language [44] (ProGS) we call Simple Property Graph Shapes Language (sProGS). The shape language is heavily inspired by SHACL and adapted for property graphs by differentiating between node and edge shapes, introducing constraints for property annotations, and for constraining the nodes (or edges, respectively) reachable from edges (or nodes, respectively). We omit named shapes, simplifying shape semantics by avoiding recursive shapes (nonrecursive named shapes are merely syntactic sugar), as well as some other features such as qualified number restrictions or complex path expressions. A sProGS shape is either a node shape N ⟨qN , ϕN ⟩ or an edge shape E ⟨qE , ϕE ⟩, where qN and qE are the target queries, and ϕN and ϕE are the respective constraints (see Definition 16 and Definition 17). Each node (or edge, respectively) of the graph that matches the target must satisfy the constraint. 10

JnKpro-q = {n} G

JeKpro-q = {e} G

JlN Kpro-q = {n | n ∈ N ∧ lN ∈ λ(n)} G

JlE Kpro-q = {e | e ∈ E ∧ lE ∈ λ(e)} G

JkN Kpro-q = {n | n ∈ N ∧ σ(n, kN ) ̸= ∅} G

JkE Kpro-q = {e | e ∈ E ∧ σ(e, kE ) ̸= ∅} G

Figure 4 Evaluation of target node and target edge queries.

Definition 16 (Node and Edge Targets). Given target node or edge IDs n or e, node or edge labels lN or lE , and node or edge properties kN or kE , node or edge targets are defined as qN ::= n | lN | kN qE ::= e | lE | kE Definition 17 (Node and Edge Constraints). Node and edge constraints are defined by ϕN ::= ⊤ | n | lN | ¬ϕN | ϕN ∧ ϕN | ∃kN .(= v) | ∃kN .⊤ | ∃→ ϕE | ∃← ϕE ϕE ::= ⊤ | e | lE | ¬ϕE | ϕE ∧ ϕE | ∃kE .(= v) | ∃kE .⊤ | ⇒ ϕN | ⇐ ϕN where in particular ∃kN .(= v) and ∃kN .⊤ require properties with certain (v) or any (⊤) values, ∃→ ϕE requires an outgoing edge conforming to ϕE , and ⇒ ϕN requires the target node to conform to ϕN . The remaining cases are similar. Definition 18 introduces the validation semantics for a PG under a set of sProGS shapes. Figure 4 defines the semantics of target node and target edge queries. Figure 5 defines the evaluation semantics of node and edge constraints. These definitions differ from [44], using direct evaluation of constraints on target nodes instead of a semantics of faithful assignments, which is not needed since we omit recursion. Definition 18 (sProGS Validation). A PG G is valid regarding a set of sProGS shapes S if it is valid regarding all shapes s ∈ S; validity regarding a single shape s = N ⟨qN , ϕN ⟩ (or s = E ⟨qE , ϕE ⟩, respectively), denoted valid(G, s), is defined as follows: : JϕN Kpro-n valid(G, N ⟨qN , ϕN ⟩) = ∀n ∈ JqN Kpro-q n,G = true G

valid(G, E ⟨qE , ϕE ⟩) = ∀e ∈ JqE Kpro-q : JϕE Kpro-e G e,G = true

In a slight abuse of notation, we also write valid(G, S) to indicate that G is valid regarding each s ∈ S. Example 19 shows two example shapes. Example 19. Recall sshacl from Example 8. We can express an equivalent shape using sProGS 1 → with spro = ⟨Agent, ∃ (obs ∧ ⇒ Person)⟩. This is a node shape that targets all nodes with N 1 the node label Agent; it requires for validity that these nodes have an outgoing edge (∃→ ϕE ) where the constraint ϕE — an edge constraint — must validate at least one edge. For this edge, we require the edge label obs, and then, expressed with ⇒ ϕN , that the corresponding destination node conforms to ϕN , i.e., has the node label Person. = E ⟨obs, ⇐ Agent ∧ ⇒ Person⟩, We can also express shapes that target edges, such as spro 2 which states that edges labeled with obs must have an origin node labeled Agent (⇐ Agent) and the destination node labeled Person (⇒ Person). The example graph Gpg 1 introduced in pro Example 10 is valid regarding both spro and s . 1 2 11

J⊤Kpro-n n,G = true

′ Jn′ Kpro-n n,G = true if n = n

JlN Kpro-n n,G = true if lN ∈ λ(n)

pro-n J¬ϕN Kpro-n n,G = true if not JϕN Kn,G

1 pro-n 2 pro-n Jϕ1N ∧ ϕ2N Kpro-n n,G = true if JϕN Kn,G and JϕN Kn,G

J∃k.(= v)Kpro-n = true if v ∈ σ(n, k) n,G

J∃k.⊤Kpro-n = true if σ(n, k) ̸= ∅ n,G

J∃→ ϕE Kpro-n = true if ∃e ∈ E, n′ ∈ N such that ρ(e) = (n, n′ ) and JϕE Kpro-e n,G e,G J∃← ϕE Kpro-n = true if ∃e ∈ E, n′ ∈ N such that ρ(e) = (n′ , n) and JϕE Kpro-e n,G e,G J⇒ ϕN Kpro-e = JϕN Kpro-n e,G n2 ,G where (n1 , n2 ) = ρ(e)

J⇐ ϕN Kpro-e = JϕN Kpro-n e,G n1 ,G where (n1 , n2 ) = ρ(e)

Figure 5 Evaluation of node and edge constraints over a property graph G, omitting some cases for edges that are analogous to the node variants.

3

Formalizing the Problem

The essential problem statement of this work is formalized in the signature of Algorithm 1: We aim to decide, given a sProGS shape s, whether all possible output graphs of a SGCQ query q are valid regarding this shape. The set of possible output graphs is defined as the set of graphs produced by q from any graph that is valid regarding a given set of sProGS shapes Sin , which we call the input shapes of our problem. With this decision procedure, we can find the set of all shapes characterizing the possible output graphs by enumerating a finite set of candidates and testing each candidate. We refer to our prior work [40] for a detailed discussion on when such a finite set exists or how to deal with cases where it does not exist. In short, for restricted classes of shapes, the set of relevant candidates that need to be considered can be shown to be finite (e.g., ALCHOI-based shapes); for other cases, heuristics can be employed. Note how this allows our approach to work for compositions of queries: the output of a prior step becomes the input of the next5 . Algorithm 1 High-level pseudocode outlining our core approach. Input A finite set of shapes sProGS Sin , a SGCQ q = B ⇐ Γ, and a sProGS shape s. Output Does valid(JqKGin , s) hold for every graph Gin where valid(Gin , Sin )? 1: s′ ← pro7→shacl (s) ′ 2: Sin ← {pro7→shacl (si ) | si ∈ Sin } ′ 3: q ← sgcq7→eccq (q) ′ 4: Σ ← infer(Sin , q′ ) 5: return if test(Σ, s′ ) then yes else unknown 5 Indeed, since, as we will later explore in detail, the input shapes are encoded as ALCHOI axioms, compositions of multiple queries do not require full exploration of the explicit set of output shapes but can rely on the inferred axioms directly.

12

As motivated in the introduction (Figure 3), we solve this problem by first mapping all components (that is, graphs, shapes, and queries) to an intermediate RDF layer and then utilizing an extended version of our algorithm presented in [40]. In Algorithm 1, we outline this approach in pseudocode: here, the functions pro7→shacl (s) and sgcq7→eccq (q) are the mapping functions for encoding sProGS shapes and SGCQ queries in SHACL and ECCQ, respectively. A final function for mapping the graphs themselves is not actually utilized — since our approach does not depend on concrete graph instances — but is required for the sake of formalizing the remaining mappings. The functions infer and test refer to the extension of [40]: the function infer takes the RDFmapped query and shapes, producing a set of DL axioms Σ; this step extends the algorithm from [40], accounting for the additional features included in ECCQ (cf. Definition 3). The function test takes these axioms and checks whether it can be concluded that s′ is guaranteed to hold for all possible output graphs; this step utilizes entailment. Based on this formal problem signature, we define Theorem 20. We will construct the missing components of Algorithm 1 in the following two sections (the family of mappings in Section 4 and the extended inference approach in Section 5). Finally, in Section 6, we will show that the theorem holds. Theorem 20 (Soundness of Algorithm 1). Given a finite set of shapes Sin , a SGCQ q = B ⇐ Γ, and a shape s, then valid(JqKGin , s) holds for every graph Gin where valid(Gin , Sin ) if test(infer({pro7→shacl (si ) | si ∈ Sin }, sgcq7→eccq (q)), pro7→shacl (s)).

4

A Family of Mappings on Reified Property Graphs

As outlined in Figure 3 and the previous section, we introduce a family of mappings: we map PGs G to RDF graphs pg7→rdf (G), utilizing reification for first-class edges (Section 4.1); this mapping is not directly utilized by our approach but instead comprises the formal basis on which the remaining mappings are defined. We map sProGS shapes s to ALCHOI-encoded SHACL shapes pro7→shacl (s), accounting for the reification introduced with the graph mapping (Section 4.2). And finally, we map SGCQ q to ECCQ sgcq7→eccq (q), accounting for both reification and various semantic differences between the languages (Section 4.3).

4.1

PG to RDF Mapping

We first assume a utility function _ b that maps the individual elements of PGs to unique IRIs. The details of this function are left abstract; however, in real-world implementations, such a function could, for example, utilize prefixes to differentiate between PG constructs, including node and edge IDs, labels, properties, and values. We also introduce m:nte (node-to-edge) and m:etn (edge-to-node) as role names, and m:node and m:edge as special concept names distinct from C. The former are used for reification of first-class edges, the latter for differentiating nodes and edges explicitly6 . The straightforward mapping pg7→rdf (G) is specified in Definition 21 and demonstrated in Example 22. It retains all information and can be reversed by simply inverting the presented mapping function. It utilizes _ b to map all nodes and edges, including their associated labels and properties, to RDF triples; IRIs for both PG nodes and PG edges are derived from their IDs. Edges are reified using two triples and the special role names m:nte and m:etn. 6 For the sake of readability, we assign concrete names, using m to hint at some unique meta prefix that could be used in practice; they can be arbitrary but unique names.

13

Agent

a

m:node

m:edge

m:node

a

a

a

1

m:etn

a

name

Smith

10

m:nte

1 :Agent name: "Smith" 10 :obs a

2

Person

since: "2002"

since

obs

2002

2 :Person

pg Figure 6 The reified RDF encoding pg7→rdf (Gpg 1 ) (left) and the original graph G1 (right). Note how the edge with ID 10 (right) becomes a normal RDF node via reification (left).

Definition 21 (Mapping from PG to RDF Graph). The corresponding RDF graph for a PG G = (N, E, ρ, λ, σ) is the graph constructed by edge node pg7→rdf (G) := {pg7→rdf (n) | n ∈ N } ∪ {pg7→rdf (e) | e ∈ E}

where pg7→rdf for nodes is defined as node n, pg7→rdf (n) := {(b

rdf:type, lc N ) | lN ∈ λ(n)}

∪ {(b n, kc b) | kN ∈ KN , v ∈ σ(n, kN )} N, v ∪ {(b n, rdf:type, m:node)} and for edges (with ρ(e) = (n1 , n2 )) as edge n1 , pg7→rdf (e) := {(c

m:nte, eb), (b e, m:etn, n c2 )}

∪ {(b e, rdf:type, lbE ) | lE ∈ λ(e)} ∪ {(b e, kc b) | kE ∈ KE , v ∈ σ(e, kE )} E, v ∪ {(b n, rdf:type, m:edge)}. Example 22. We map the graph Gpg 1 from Example 10 to RDF, assuming a reasonable definition for _ b and omitting the display of any prefixes, to obtain the following set of triples for pg pg7→rdf (G1 ), as visualized side-by-side in Figure 6: {(1, a, m:node), (1, a, Agent), (1, name, Smith), (2, a, m:node), (2, a, Person), (10, a, m:edge), (10, a, obs), (10, since, 2002), (1, m:nte, 10), (10, m:etn, 2)}.

4.2

sProGS to SHACL (ALCHOI) Mapping

We define a function pro7→shacl for mapping sProGS shapes to SHACL shapes. Since we follow our prior work [40] in representing SHACL shapes as ALCHOI axioms, we map to ALCHOI directly. That is, we map both target queries and constraints to concept descriptions and shapes to subsumption axioms (Definition 23).

14

sProGS

ntarget pro7→shacl (n) ntarget pro7→shacl (lN ) ntarget pro7→shacl (kN )

ALCHOI {b n} c lN ∃ kc N . ⊤

Figure 7 Mapping for node target queries.

sProGS

etarget pro7→shacl (e) etarget pro7→shacl (lE ) etarget pro7→shacl (kE )

ALCHOI {b e} lbE ∃ kc E . ⊤

Figure 8 Mapping for edge target queries.

sProGS nconstr pro7→shacl (⊤) nconstr pro7→shacl (n) nconstr pro7→shacl (lN ) nconstr pro7→shacl (¬ϕN ) nconstr 1 2 pro7→shacl (ϕN ∧ ϕN ) nconstr pro7→shacl (∃kN .(= v)) nconstr pro7→shacl (∃kN .⊤) nconstr ← pro7→shacl (∃ ϕE ) nconstr → pro7→shacl (∃ ϕE )

...

econstr pro7→shacl (⇒ ϕN ) econstr pro7→shacl (⇐ ϕN )

ALCHOI ⊤ n b lc N ¬nconstr pro7→shacl (ϕN ) nconstr 1 nconstr 2 pro7→shacl (ϕN ) ⊓ pro7→shacl (ϕN ) ∃ kc N . v c ∃ kN . ⊤ ∃ m:etn− . econstr pro7→shacl (ϕE ) ∃ m:nte . econstr pro7→shacl (ϕE ) ... ∃ m:etn . nconstr pro7→shacl (ϕN ) − nconstr ∃ m:nte . pro7→shacl (ϕN )

Figure 9 Mapping sProGS node and edge constraints to ALCHOI. We omit some cases for edge constraints that are equivalent to node constraint cases.

Definition 23 (Mapping sProGS to ALCHOI). A node shape N ⟨qN , ϕN ⟩ is mapped to the axiom ntarget ntarget nconstr nconstr pro7→shacl (N ⟨qN , ϕN ⟩) = pro7→shacl (qN ) ⊑ pro7→shacl (ϕN ), where pro7→shacl (qN ) and pro7→shacl (ϕN ) are defined in Figure 7 and Figure 9, respectively. With equivalent definitions (Figure 8 and econstr Figure 9), we can map edge shapes as pro7→shacl (E ⟨qE , ϕE ⟩) = etarget pro7→shacl (qE ) ⊑ pro7→shacl (ϕE ). We write pro7→shacl (S) as a shorthand for mapping each s ∈ S. Most constructs from the syntax of sProGS translate directly to ALCHOI, similarly to how SHACL is defined in terms of ALCHOI in [40]. Interesting cases include the constraint ⇒ ϕN , which maps to ∃ m:etn . nconstr pro7→shacl (ϕN ). This node constraint requires the special role name m:etn according to the reification defined for PGs, since the original sProGS constraint refers to the target node of an edge. Given that this edge is an ordinary node in the RDF encoding, we must invoke ∃m:etn to navigate to the node representing that target and then use the mapped constraint ϕN . Similarly, ∃→ ϕE is mapped to ∃ m:nte . econstr pro7→shacl (ϕE ). Example 24 shows the full mappings for the running example. Example 24. We map the shapes spro and spro from Example 19 to equivalent ALCHOI 1 2 subsumption axioms. For the node shape spro , this results in the following shape: 1 pro → pro7→shacl (s1 ) = pro7→shacl (N ⟨Agent, ∃ (obs ∧

⇒ Person)⟩)

= Agent ⊑ ∃m:nte.(obs ⊓ ∃m:etn.Person) Note how the reification is expressed as two nested existential quantifications: we first navigate to the reified edge (node) via m:nte, where not only a label (obs) but also a particular node constraint holds, to which we navigate via m:etn; we ensure 1:Agent →m:nte 10:obs →m:etn 2:Person (cf. Figure 6). Similarly, for the edge shape spro we want 1:Agent ←m:nte 10:obs →m:etn 2:Person, 2 but from the perspective of all reified edges, instead of nodes, such that in pro pro7→shacl (s2 ) = pro7→shacl (E ⟨obs, −

⇐ Agent ∧ ⇒ Person⟩)

= obs ⊑ ∃m:nte .Agent ⊓ ∃m:etn.Person

we target an edge to navigate back to the origin (inverse m:nte) as well as the destination via m:etn, requiring the node labels Agent and Person, respectively. 15

4.3

SGCQ to ECCQ Mapping

Finally, we map SGCQ to ECCQ. The principal challenge for this mapping — aside from accounting for reification — is that in SGCQ the semantics for constructing labels and properties are different from ECCQ in that all properties and labels are kept for constructed nodes or edges unless there are remove clauses. In ECCQ, on the other hand, all triples in the result graph must be explicitly constructed by atomic patterns in the query template. We solve this issue by utilizing generic concept and role variables with appropriate filter conditions to define a mapping sgcq7→eccq (q) for a SGCQ q (Definition 25). To this end, we introduce an intermediate representation referred to as IQL (Intermediate Query Language) in Definition 26 that aligns with the two types of patterns of SGCQ, i.e. matching nodes or edges, on the SGCQ side with full query patterns or templates on the ECCQ side. This aligns parts of queries on both sides that compose naturally. Note how the decision to syntactically include where clauses in node or edge patterns of SGCQ aids this composability. Via this intermediate layer, we associate SGCQ variables with generic copy patterns expressed in ECCQ that explicitly construct the required labels and properties. Set clauses translate to explicit construction in ECCQ, while remove clauses translate to filter conditions on generic variables in the pattern of ECCQ queries, removing the offending labels from the bindings for these generic variables. We demonstrate this mapping in Example 27. Definition 25 (Mapping SGCQ to ECCQ). Given a SGCQ q, we define the mapping function sgcq7→eccq (q) by introducing the intermediate query language IQL (Definition 26) and several utility functions for mapping to and from IQL, as sgcq7→eccq (q) := iql7→eccq (sgcq7→iql (q))

where the following utility functions (defined in Figure 10) are utilized: [ template [ pattern sgcq7→iql (B ⇐ Γ) = sgcq7→iql (β, vars(Γ)) ∪ sgcq7→iql (γ) γ∈Γ

β∈B iql7→eccq (IT ← IP ) =

[ template

[ pattern

t∈IT

p∈IP

iql7→eccq (t) ∪

iql7→eccq (p)

Definition 26 (Intermediate Query Language). We define the syntax of the intermediate query language (IQL) as follows: q := IT ← IP p := MN (xn , WL , WK , WV , RL , RK ) | ME (xn , xn , xe , WL , WK , WV , RL , RK ) t := CN (xn , AL , AK , V ) | CE (xn , xn , xe , AL , AK , V ) where WL is a set of label patterns :l, WK is a set of key patterns .k, and WV is a set of patterns .k = v. Similarly, AL is a set of set label patterns ⊕l, AK is a set of set key-value patterns ⊕k = v, and V is a set of variables. Finally, RL is a set of remove label patterns ⊖l, and RK is a set of remove key patterns ⊖k. The semantics of IQL are implicitly defined through the mappings in Figure 10. Example 27. The example SGCQ q2sgcq in Figure 11 (left) includes the major SGCQ features, such as matching on an edge pattern, setting and removing labels, and restricting results with constraints. The resulting ECCQ sgcq7→eccq (q2sgcq ) is shown in Figure 11 (right). The query is suitable for application to Gpg 1 from Example 10. We focus here on the single variable y, which occurs in two atomic patterns: (y, :Person) (in Γ) and (y, {⊕POI, ⊖Person}) (in B). 16

pattern sgcq7→iql ((x, ξ)) := MN (x, { :l |

:l ∈ ξ}, { .k | .k ∈ ξ},

{ .k = v | .k = v ∈ ξ}, {⊖l | ⊖l ∈ Sx }, {⊖k | ⊖k ∈ Sx }) pattern sgcq7→iql (((x, y):z, ξ)) := ME (x, y, z, { :l |

:l ∈ ξ}, { .k | .k ∈ ξ},

{ .k = v | .k = v ∈ ξ}{⊖l | ⊖l ∈ Sz }, {⊖k | ⊖k ∈ Sz }) template sgcq7→iql ((x, S), V) := CN (x, {⊕l | ⊕l ∈ S}, {⊕k = v | ⊕k = v ∈ S}, V ) template sgcq7→iql (((x, y):z, S), V ) := CE (x, y, z, {⊕l | ⊕l ∈ S}, {⊕k = v | ⊕k = v ∈ S}, V )

pattern C I R iql7→eccq (MN (. . .)) :=({x : x , (x, x ) : x , x : m:node} ∪

{x : b l | :l ∈ WL }

∪ {(x, ox,k ) : b k | .k ∈ WK } ∪ {(x, vb) : b k | .k = v ∈ WV }, R C {x ̸= m:nte} ∪ {x ̸= b l | ⊖l ∈ RL } ∪ {xR ̸= b k | ⊖k ∈ RK }) pattern C I R iql7→eccq (ME (. . .)) :=({(x, z) : m:nte, (z, y) : m:etn, z : z , (z, z ) : z , z : m:edge}

∪ {z : b l | :l ∈ WL } ∪ {(z, oz,k ) : b k | .k ∈ WK } ∪ {(z, vb) : b k | .k = v ∈ WV }, l | ⊖l ∈ RL } ∪ {z R ̸= b k | ⊖k ∈ RK }) {z R ̸= m:etn} ∪ {z C ̸= b template C I R iql7→eccq (CN (. . .)) :={x : m:node} ∪ ({x : x , (x, x ) : x } if x ∈ V

else {})

∪ {x : b l | ⊕l ∈ AL } ∪ {(x, vb) : b k | ⊕k = v ∈ AK } template iql7→eccq (CE (. . .)) :={(x, z) : m:nte, (z, y) : m:etn, z : m:edge} C I R

∪ ({z : z , (z, z ) : z } if z ∈ V else {}) ∪ {x : b l | ⊕l ∈ AL } ∪ {(x, vb) : b k | ⊕k = v ∈ AK }

Figure 10 Component-wise mappings from SGCQ to IQL and IQL to ECCQ, both for query templates and patterns. We write Sx to refer to the union of all sets of add or remove patterns S, such that (x, S) ∈ B or (x1 , x2 ):(x, S) ∈ B.

17

{(x, ∅),

{x : m:node, x : xC , (x, xI ) : xR ,

(x, y):(e, ∅),

e : m:edge, e : eC , (e, eI ) : eR , (x, e) : m:nte, (e, y) : m:etn,

(y, {⊕POI, ⊖Person})}

y : m:node, y : yC , (y, yI ) : yR , y : POI}

⇐

←

{(x, { .name = "Smith"}), (x, y):(e, { :obs}), (y, { :Person})}

({x : m:node, x : xC , (x, xI ) : xR , (x, Smith) : name, e : m:edge, e : eC , (e, eI ) : eR , e : obs, (x, e) : m:nte, (e, y) : m:etn, y : m:node, y : yC , (y, yI ) : yR , y : Person}, {yC ̸= Person, xR ̸= m:nte, eR ̸= m:etn, yR ̸= m:nte})

Figure 11 SGCQ q2sgcq on the left, and ECCQ sgcq7→eccq (q2sgcq ) on the right. Note how we visually align the lines of the left and right columns for their common variables, hinting at the IQL rules, e.g., the POI set label and respective triple pattern (blue). The only exception is the inclusion of yC ̸= Person (yellow) in the filter patterns of the ECCQ (right column), highlighting why the IQL pattern MN needs the remove clauses as part of their arguments: remove clauses from the template of SGCQ affect the pattern (filters) of ECCQ.

MN (y, {: Person}, ∅, ∅, {⊖Person}, ∅}) and CN (y, {⊕POI}, ∅, {x, y, e}) are the corresponding IQL terms. The former maps to the ECCQ pattern including the generic pattern y : yC , copying all labels for y, the explicit pattern y : Person selecting instances of Person, but also the filter yC ̸= Person, which prevents bindings, and thus also the construction, for label Person for the generic variable yC , included because of the remove term in the original SGCQ query. The ECCQ template includes, along with the generic patterns, the explicit construction of y : POI.

5

Shape Inference for ECCQ

As introduced in the formalization of our core problem in Section 3, we aim to infer a set of ALCHOI axioms Σ from an ECCQ q and a set of shapes Sin (written Σ = infer(Sin , q)), such that Σ |= so (test(Σ, so ) in Section 3) implies that so is a shape validating all possible output graphs of q, under the precondition that the input graphs of q are guaranteed to be valid regarding Sin .

5.1

Encoding Constraints in DL

We build on and extend [40], which essentially approximates axioms of the closed-world assumption from sub-expressions of the query and joins them with the input shapes and a few additional axioms. To this end, three namespaces need to be distinguished: those of the input graphs, of the subgraphs matched by the query, and of the new output graphs constructed as a result. The extensions of concepts involved clearly differ between these three namespaces; thus, we follow [40] in renaming any concept name A in the input namespaces as Ȧ and Ä in the matched and output namespaces. We do the same for each role name p (with ṗ and p̈). Query variables can be represented with variable concepts, that is, fresh concept names Vx for each variable x. The extensions of these concepts are equal to the set of all of their bindings. Thus, variable concepts remain the same in all namespaces and are not subject to any renaming. 18

a A, B b E, A

a Vx

a Ä, B̈

a Ä, B̈

c A

b Vy

b Ë

b Ë, Ä

(a) An example input graph.

(b) Variable concepts.

(c) Output graph of q.

(d) Output graph of q ′ .

Figure 12 Example for graphs involved in constructing the validation knowledge base (cf. [40]) for the query q with P = H = {x : A, x : B, y : E} from Example 28. This case demonstrates the potential issue arising when adding the atomic pattern y : y C in q ′ , since variable y matches b which is an instance of A; this violates the assumptions about the relationship of Ä and B̈ in the output graph. Colors visualize different namespaces, while floating labels indicate concept names (e.g., a is both A and B).

They are constrained by the basic graph patterns of the query pattern P they occur in and therefore play a key role in encoding the input-output relationship of queries. The essential extension of our SPARQL subset ECCQ over the subset considered in [40] are generic copy operations through variables for concepts and properties and certain filter expressions on these variables. The minimal Example 28 shows how this invalidates the axioms inferred by [40], while also giving the intuition of this method. Example 28. Assume a query q with P = H = {x : A, x : B, y : E} and no input shapes. The axioms inferred by [40] would include {Vx ≡ A⊓B, Vy ≡ E, Ä ≡ Vx , B̈ ≡ Vx , Ë ≡ Vy }. We demonstrate these for an example input graph (Figure 12a) in Figure 12. That is, we define the variable concept Vx (visualized as a graph in Figure 12b) in terms of its bindings, namely the intersection of A and B, and the new concept names in the output namespace Ä and B̈ in terms of these Vx . Since these axioms entail, e.g., Ä ⊑ B̈, just as in the example Figure 12c, we can conclude that the shape A ⊑ B holds on all output graphs. If we were to extend query q as q ′ by adding {y : yC } to both P and H, the axiom Ä ⊑ B̈ should no longer be entailed; indeed, variable y might now also include — such as in Figure 12d — bindings that are of type A exclusive or B and modify Ä or B̈ through the generic pattern y : yC , thereby invalidating this subsumption. We can remedy this broken inference introduced in Example 28 by including components of all variables that have generic copy operations in the definition of concepts like Ä. Such components are defined in Definition 30 and included in axioms constructed by the adapted method outlined in Definition 31. We write vcg(q) (variable connectivity graph) to mean a graph where variables var(q) are nodes and there exists an edge between two variables if and only if they both occur in a pattern (e.g., x and y in (x, y) : p) in sgcq7→eccq (q). Example 28 can therefore be fixed by using this extension as shown in Example 29. We demonstrate a full example of the algorithm in Section 5.3. Example 29. With the extended method, we infer the set of axioms including {Vx ≡ A ⊓ B, Vy ≡ E A B E E, Ä ≡ Vx ⊔ VAy ⊔ VAx , B̈ ≡ Vx ⊔ VBx ⊔ VBy , Ë ≡ Vy ⊔ VE x ⊔ Vy } where Vy ≡ Vy ⊓ A, Vy ≡ Vy ⊓ B, Vy ≡ Vy ⊓ E and VAx ≡ VBx ≡ VE x ≡ ⊥. Here, the axioms defined for the output namespace (e.g., Ä ≡ Vx ⊔ VAx ⊔ VAy ) include additional component concepts (e.g., VAy ) for all variables in the query. Thus, we ensure that the possibility of atomic pattern y : yC constructing instances of Ä in output graphs is accounted for. As a result, we can no longer erroneously infer A ⊑ B without additional knowledge in terms of input shapes about the relationship of A, B, and E. 19

Definition 30 (Concept Components). We define the concept components Cc(q) of an ECCQ q = H ← (P, F ) as the set of axioms including: 1. For all x ∈ var(P ) and A ∈ V, if x : xC ∈ P ∩ H and (xC ̸= A) ̸∈ F , then VxA ≡ Vx ⊓ A. Otherwise, VxA ≡ ⊥. 2. For all x, y ∈ var(P ) and p ∈ V, if (x, xI ) : xR ∈ P ∩ H, (xR ̸= p) ̸∈ F and (x, y) : p ̸∈ P , then Vxp ≡ Vx ⊓ ∃p.Vxp,o . Otherwise, Vxp ≡ ⊥ and Vxp,o ≡ ⊥. Here, V = voc(q) ∪ voc(Sin ) is the vocabulary of all concept, role, and individual names that occur in the query or in input shapes. Definition 31 (Axiom Encoding). The axiom encoding of an ECCQ q and a set of ALCHOI shapes Sin , denoted infer(Sin , q), is the minimal set of ALCHOI axioms that include Cc(q) (Definition 30) as well as the following axioms: 1. The set of input shapes Sin . 2. For each variable x in var(q), the axiom l l Vx ⊑ A⊓ x : A∈P

∃p. Cu ⊓

(x,u) : p∈P

l

∃p− . Cu ,

(u,x) : p∈P

and if vcg(P ∪ H) is acyclic regarding x, then also the axiom l l l Vx ⊒ A⊓ ∃p. Cu ⊓ ∃p− . Cu . x : A∈P

(x,u) : p∈P

3. For each concept name A in voc(H), Ä ≡

F

(u,x) : p∈P u : A∈H Cu ⊔

F

A x∈var(H) Vx .

4. For each p in voc(H) F

(u,v) : p∈H Cu ⊑ ∃p̈. Cv ,

∃p̈. Cv ⊑

F

∃p̈.⊤ ≡

F

∃p̈− . Cu ⊑

F

∃p̈− .⊤ ≡

F

(u,v) : p∈H Cu ⊔

F

(x,xI ) : xR ∈H Vx ,

(u,v) : p∈H (Cu ⊓∃p̈. Cv ) ⊔ F − (u,v) : p∈H Cv ⊑ ∃p̈ . Cu ,

F

p x∈var(H) Vx ,

p,o (x,xI ) : xR ∈H Vx , − (u,v) : p∈P (Cv ⊓∃p̈ . Cu ). (u,v) : p∈H Cv ⊔

F

5. For each p ∈ P , ṗ ⊑ p. 6. For each p ∈ P , p ⊑ ṗ if all atomic patterns including p in P have the form (x, y) : p where x, y occur in no other atomic pattern in P and x ̸= y. 7. For each pair p, r with (x, y) : p ∈ P and (x, y) : r ∈ H or (y, x) : r ∈ H (a) ṗ ⊑ r̈ (if (x, y) : r ∈ H) or ṗ ⊑ r̈− (if (y, x) : r ∈ H) — if P does not contain any other atomic patterns with p, and (b) r̈ ⊑ ṗ (if (x, y) : r ∈ H) or r̈− ⊑ ṗ (if (y, x) : r ∈ H) — if H does not contain any other atomic patterns with r. Cases 1, 2, and 5-7 are taken from, and 3 and 4 are adapted from [40]. 20

5.2

Enriching the Query

Generic copy operations can invalidate output shapes in certain cases, as shown in Example 29. On the other hand, they enable means of semantically enriching the ECCQ query, leading to additional shapes that can be shown to hold. To this end, we define the extension rules in Definition 32 that essentially copy constraints from the query pattern to the template in cases where this is allowed by generic patterns. We include an example in Section 5.3. Definition 32 (Extension of ECCQ). The semantics-preserving extension of a ECCQ q = H ← (P, F ), written Ext(q), is defined by inserting the following atomic patterns to the template H: 1. If x : xC ∈ P ∩ H, then for each x : A ∈ P such that (xC ̸= A) ̸∈ F , we include the atomic pattern x : A in H, and 2. if (x, xI ) : xR ∈ P ∩ H, then for each (x, a) : p ∈ P such that (xR ̸= p) ̸∈ F , we include the atomic pattern (x, a) : p in H.

5.3

Example

pro We now demonstrate some axioms in Σ constructed for the problem inputs S1pro = {spro 1 , s2 } sgcq (Example 19) and q2 (Example 27). Again, we will focus on axioms related to concept names, as they are more intuitive, yet in principle very similar to axioms related to role names. As a first step, we need to map the query to ECCQ as shown in Example 27 and then extend the mapped query to obtain the ECCQ input as q2eccq = Ext(sgcq7→eccq (q2sgcq )). The extended query template includes the atomic patterns {e : obs, (x, "Smith") : name} in addition to the atomic patterns that are shown in Figure 11, which are copied from the query pattern due to the presence of generic patterns for x and e. On the other hand, since the only constraining atomic pattern for y, namely y : Person, is also included in the filter yC ̸= Person, there is no template extension for variable y, even though there are generic patterns (cf. Definition 32). According to Definition 31.1 we need to include the input shapes in Σ after mapping them to ALCHOI axioms via pro7→shacl (S1pro ). These axioms encode constraints that are known to hold on the input graph by definition, since we only consider valid input graphs (cf. Example 24). According to Definition 31.2 we next define variable concepts encoding known constraints for the bindings of all query variables. We include the following axioms in Σ:

Ve ≡ ∃m:etn.Vy ⊓ ∃m:nte− .Vx ⊓ obs Vx ≡ ∃name.Smith ⊓ ∃m:nte.Ve Vy ≡ ∃m:etn− .Ve ⊓ Person These variable concepts are almost direct translations of the query pattern; for example, variable x occurs in (x, Smith) : name and (x, e) : m:nte (Example 27), which translates to the intersection of ∃name.Smith and ∃m:nte.Ve in the definition of Vx . Note how reification again plays a role here, with the presence of the role name m:nte. Constraints related to concept names that explicitly occur in the query template are defined according to Definition 31.3 in terms of these variable concepts, including the concept components that were introduced in Definition 30. In the following set, we also include one axiom inferred

21

¨ from the rules for properties, namely Ve ⊑ ∃m:etn.V y. ¨ ≡ Ve ⊔ Vobs obs e Agent ¨ Agent ≡ Vx ⊔ VAgent y

POI ¨ ≡ Vy ⊔ VPOI POI x ⊔ Vy

VPOI ≡ Vx ⊓ POI x

VAgent ≡ Vx ⊓ Agent x

VPOI ≡ Vy ⊓ POI y

VAgent ≡ Vy ⊓ Agent y

¨ Ve ⊑ ∃m:etn.V y

Vobs ≡ Ve e ¨ (defined with dots, There are a few noteworthy aspects to these axioms: firstly, note how POI since it differs from the concept POI, which may occur in input graphs) is defined in terms of Vy , because it exclusively occurs in the atomic pattern y : POI of the query template, and Vy encodes the bindings of variable y. Furthermore, we must include the concept components VPOI (and also x ¨ VPOI , though this is redundant in this case) in the definition of POI since variable x occurs with y C ¨ the generic pattern x : x , meaning that the new concept POI may extend over some bindings for ¨ similarly, with the difference that there is no actual construct pattern x, too. We treat Agent featuring Agent; thus, its definition consists only of concept components. ¨ ⊑ ∃m:etn. ¨ Therefore, we know that ¨ POI. The complete set of inferred axioms entails, e.g., obs obs ⊑ ∃m:etn.POI validates all output graphs of the query. For the final shapes, we drop the namespace distinction, since it is not part of our (or any regular) query semantics.

6

Metatheory

To encode our inference task in ALCHOI, we first map shapes and queries to ALCHOI and ECCQ then infer a set of axioms Σ from these mapped queries and shapes (cf. Algorithm 1). Therefore, we need to prove that any mapped shape C ⊑ D holds on all output graphs of the query if Σ |= C̈ ⊑ D̈. That is, if our inferred set of axioms Σ entails the respective axiom (i.e. encoded shape) in the output graph namespace annotated with two dots. The primary outcome of the following considerations is the soundness of Algorithm 1, as expressed in Theorem 20. To this end, we first prove the semantic equivalence for our mappings in Proposition 33 and Proposition 34. Full proofs are available in the appendix. Proposition 33 (Soundness of Shape Mapping). Given a PG G and a set of sProGS shapes S, the graph G is valid regarding each shape s ∈ S if and only if the mapped graph pg7→rdf (G) is valid regarding the mapped shapes pro7→shacl (s). Proof Sketch. We prove the proposition in two steps. First, we show that given a sProGS shape s, the targets of s in G correspond to the set of targets of pro7→shacl (s) in pg7→rdf (G). Then, we show that for any node (or edge) in G, it conforms to the constraint of a shape s if and only if the mapped node in pg7→rdf (G) conforms to the constraint of pro7→shacl (s). Proposition 34 (Soundness of Query Mapping). Given a PG G and a SGCQ q, the following holds: JqKsgcq = pg7→rdf −1 (Jsgcq7→eccq (q)Keccq ), where pg7→rdf −1 is the inverse mapping of G pg7→rdf (G) pg7→rdf . That is, evaluating the query q is the same as evaluating the mapped query on the mapped graph and then mapping the result graph back. Proof Sketch. We separate the matching and constructing parts of queries for this proof. To this end, we rely on the composable intermediate query language (IQL), making individual node or edge patterns compose neatly with full ECCQ patterns (or templates). We define an equivalence relation between sets of bindings Ω for queries expressed as both SGCQ and ECCQ, which is not 22

straightforward, given that SGCQ queries bind only nodes and edges (while labels and properties are implicit), but the corresponding reified labels and properties in ECCQ are explicitly bound as variables. We prove that both SGCQ and mapped ECCQ produce equivalent bindings. In the second part of the proof, we show that — given sets of equivalent bindings — the constructed graphs are again the same, modulo the mapping relation. It remains to show that shapes entailed by the axioms Σ constructed according to Definition 31 are guaranteed to validate output graphs of the query, modulo renaming in the appropriate namespace. Proposition 35. Given an ECCQ q and a set of ALCHOI shapes Sin it holds for all RDF graphs G with valid(G, Sin ) that infer(Sin , q) |= s̈ implies valid(JqKeccq G , s). Proof Sketch. For this proof we first formalize the different conceptual graphs involved (according to the namespaces separated with one or two dots) as joined extended graphs and then show for the axioms constructed by the rules of Definition 31 that all extended graphs are indeed valid regarding these axioms. From this, we then follow (utilizing some auxiliary lemmas) that any other entailed shapes, when renamed accordingly, validate all possible output graphs of the query. This proof builds on the proofs in [40]. Finally, we show that extending the ECCQ preserves query semantics. Proposition 36. For any ECCQ q and RDF graph G, JqKeccq = JExt(q)Keccq G G .

Proof Sketch. This proposition follows directly from the specified semantics of ECCQ since all concept or role names explicitly added to the template of q by rules for Ext(q) (Definition 32) are also constructed by the respective generic patterns x : xC and (x, xI ) : xR , except those that occur in filter conditions, which are excluded in the definition of Ext(q). With these propositions, we can finally address the main claim of this paper. We rewrite the theorem initially introduced as Theorem 20 in Theorem 37, replacing the function test with concrete entailment and including the family of mappings. The proof follows directly from the propositions discussed in this section. Theorem 37. (Reformulation of Theorem 20) Given a finite set of sProGS shapes Sin , a SGCQ q = B ⇐ Γ, and a sProGS shape s, then valid(JqKGin , s) holds for every graph Gin where valid(Gin , Sin ) if infer(pro7→shacl (Sin ), sgcq7→eccq (q)) ⊢ pro7→shacl (s̈). Proof Sketch. This follows directly from the propositions introduced in this section.

7

Implementation and Evaluation

We implemented the algorithm described in this paper, including both the mapping and inference components, in Scala. To this end, we built on our previous implementation of [40] (see [42]), which is available under a free software license. Our fork of this implementation is available on GitHub7 [43] as well. We implemented parsers, as well as our formally specified mappings, for both G-CORE to SPARQL CONSTRUCT and ProGS to SHACL; modified the inference algorithm of the implementation [42] with our extended variant as specified, constructing different sets of description logic axioms that are then passed to the HermiT [28] reasoner for inference; implemented unit and end-to-end test cases that cover G-CORE and the extended SPARQL features; and validated the algorithm based on query execution over randomly generated graphs. 7 https://github.com/softlang/s2s

23

7.1

Experimental Setup and Results

To validate the correctness of our implementation and gather empirical evidence, in addition to the proofs provided by this work, on the correctness of our method, we generated random problem instances, consisting of a set of input shapes and queries. We generated random queries first and then sampled shapes based on their vocabularies, extended with additional random components that do not occur in queries. For each sample input, we applied our algorithm to obtain a set of output shapes; to this end, we generated a set of candidate shapes and checked each for entailment. We only kept samples that produced at least one valid output shape. We covered four different scenarios labelled corresponding to the nature of the shapes involved. While small and large mainly refer to the number of shapes, the wide sample includes conjunction and disjunction, whereas the deep sample includes more deeply nested shapes. Figure 13 shows the distribution of a few key properties across the experiments we performed, including the basic structure of queries and shapes, as well as the candidate shapes that were considered. For additional details, we refer to our extended version or the documentation of the implementation itself. The upper half of the tables describes queries, while the lower half corresponds to shapes. For both wide and large we report only data on shapes, since the queries are mostly identical to the deep scenario. Regarding queries, we indicate the number of basic node or edge atomic clauses in the pattern and template, the number of set, remove, or where clauses, and the distinct number of labels and keys. Regarding shapes, we include the number of sampled input shapes, their structure (number of basic components and clauses in conjunction or disjunction), the number of candidates over the vocabulary tested as potential output shapes, and the inferred set of output shapes, i.e., the subset of candidates that is entailed by the constructed knowledge base. Our scenarios were designed to cover various interactions of query structures and shapes and facilitate our validation approach (random sample graphs), not necessarily to correspond to real-world data, where a baseline is also not available. Our validation framework operates fully on the mapped SHACL and SPARQL level, taking the input SHACL shapes mapped from ProGS as the basis for generating a random RDF graph valid regarding these shapes. The generation approach is rather brute force, to not bias the sample graphs with additional information from shapes or queries, taking only information from the vocabulary of the problem instance while removing any parts that violate input shapes. We next applied the (mapped-from G-CORE) SPARQL CONSTRUCT query to this sample graph to obtain the corresponding output graph. Finally, we validated the output graph with the inferred output shapes. For each sample, we report either the class of a generation-related issue (leading to vacuous satisfaction of output shapes), output graph validation failure (shape violations), or success (non-vacuously valid graphs). In 100, 000 samples we observed no validation failures, providing evidence towards the correctness of our method and implementation. A total of 37, 959 samples were full successes, meaning that the output graph was not only valid regarding the output shapes but also included all their targets. In 12, 858 cases, the output graph only included a subset of the targets present in output shapes, while in 266 cases, the input graph included only a subset of all input shape targets; we consider these partial successes. The remainder (48, 917 samples) were other structural issues, where in most cases result graphs were either entirely empty (26, 591) or did not include any of the required target nodes (15, 560), while in fewer cases we were unable to produce a suitable input graph (6, 622), or the query exceeded the allowed execution time of 60 seconds (144). These results did not vary significantly between the different classes. Note that in all of these cases, modulo the few timeouts where we do not know the result, the output shapes were still vacuously satisfied. Since our validation attempts each sample generation up to 100 times, we hypothesize that the reason for these cases mostly lies in the structure of the

24

Type

Avg.

Med.

Type

Avg.

Med.

MATCH CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys

1.00 1.00 3.15 1.59 0.99 3.67 1.31

1.00 1.00 3.00 2.00 1.00 4.00 1.00

MATCH CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys

1.21 2.21 3.20 1.57 0.99 3.64 1.33

1.00 2.00 3.00 2.00 1.00 4.00 1.00

1.00 2.16 1.00 256.24 7.54

1.00 2.00 1.00 240.00 2.00

2.63 2.96 1.00 408.25 7.53

3.00 3.00 1.00 370.00 2.00

Input Shapes Components Clauses Candidates Output Shapes

Input Shapes Components Clauses Candidates Output Shapes

(a) Sample small (25,000)

Type Input Shapes Components Clauses Candidates Output Shapes

(b) Sample deep (25,000)

Avg.

Med.

Type

2.61 4.95 1.86 510.25 9.85

3.00 5.00 2.00 468.00 2.00

Input Shapes Components Clauses Candidates Output Shapes

(c) Sample wide (25,000)

Avg.

Med.

5.07 2.16 1.00 610.32 11.18

5.00 2.00 1.00 576.00 2.00

(d) Sample large (25,000)

Figure 13 Overview of statistical measures across different generator configurations.

sample itself: in these cases, graphs conforming to input shapes are unlikely to be matched by the query, since both do not align well. Again, we decided against optimizing for these scenarios to avoid overfitting generated samples to preferred cases, which could bias results. We validated the implementation of the validation itself with 1, 000 samples over the same four classes, where output shapes (7 per sample) were drawn randomly from the set of candidate shapes instead of utilizing the inference procedure; here, we obtain 76.7% validation failures and only 0.2% complete successes, indicating a very high probability for detecting failures. Our complete results, including additional metadata for each sample, results for the individual classes of samples, all details regarding the structure and generation of samples, and the tools to replicate these and similar experiments, are provided with our implementation.

7.2

Runtime Performance

While the original project, on which our implementation is based, includes tooling to demonstrate feasibility in terms of runtime performance (cf. [40]), the results would be difficult to compare between the different classes of queries and shapes used in our implementation. Additionally, we lack datasets for realistic properties of G-CORE or ProGS queries and shapes. Instead, we therefore report only a preliminary indication of the feasibility of runtime performance, within the same order of magnitude as the prior results, by measuring the inference time (testing all shape candidates reported in Figure 13) for all 100, 000 samples generated for the correctness validation 25

above. Here, we observe average (median) inference times per sample of 13.94ms (11.00ms) for small, 34.81ms (25.00ms) for deep, 42.23ms (29.50ms) for wide, and 51.68ms (36.00ms) for large samples on commodity hardware (Ryzen 7 9700X), without any dedicated Scala optimization.

8

Related Work

Mappings between query languages and related (graph) data models have been considered for various languages (cf. [31]), including mappings among graph query languages (e.g., [48]) as well as between graph query languages and SQL (e.g., [39, 12, 46]). Closely related to our mapping problem, SPARQL SELECT queries have been mapped to Cypher [52, 2]. However, in this direction, the divide between RDF and PG is less challenging, given that PG can directly represent RDF graphs. Reification of PG as RDF (e.g., [33, 51]) has been discussed under consideration of querying performance [24], though only under manually defined, ad hoc reformulation of Cypher queries in SPARQL SELECT. At the data model level, the lack of interoperability between RDF and PG is a known issue [5], and mappings from RDF to PG have been considered as well, e.g., [6]. In [37], the authors consider both RDF graphs and SHACL shapes, transforming them to PG and PG-Schema, respectively. RDF-star [19] is an extension to RDF for the representation of metadata as nested triples, allowing for similar features as PG, thus working towards bridging the formal gap between these data models. Indeed, both PG mappings to RDF-star [20, 24], and the reverse [1] have been defined. In particular, this also includes execution of SPARQL-star queries over PG [20]. In contrast, in our work, we leverage reification in pure RDF for the sake of utilizing DL via SHACL, and we are concerned with bridging the semantic differences between graph construction in G-CORE, with its implicit labels and properties, and SPARQL CONSTRUCT, with its explicit triple construction, which are not addressed in previous work. Inference of shapes or schemas can be approached essentially in two ways: Option 1 — inference from instance data, e.g., concrete graphs or tables; Option 2 — inference from queries and other functions constructing data. The first option has been considered for RDF using various algorithms based on logical, statistical, or ML-driven inference for constructing SHACL or ShEx [36] shapes from sample graph instances [45, 16, 38, 32, 34, 17, 9]. Similar approaches have been considered recently for PG and their schema languages [29, 11, 17]. In our work, we follow the second option and do not consider any instance data but instead infer shapes valid in the context of any possible graph that queries might operate on in the future. However, inference from concrete graphs may complement our approach when initial input shapes for queries should be determined. Our approach leverages a prior method [40], as discussed throughout the paper, but we cover PG and G-CORE through mappings; in due course, we also extend the subset of SPARQL considered in [40] with generic copy patterns. Related work on the inference of SHACL shapes from direct mappings [49] and RML rules [14] also follows the second option, but these approaches lack the arbitrary construction through query patterns we support, in addition to explicit input constraints. Views over relational databases can be considered equivalent mechanisms to composable graph queries; SQL schemas have been inferred for such views in [25, 15, 47, 22] though suffer from infeasibility of first-order formulas (as compared to DL) or restricted semantics of functional or join dependencies, which are orthogonal to constructs supported by ProGS in our case. [10] solves a similar problem, focusing on basic cardinality constraints (as graph schemas) and formally defined graph transformations (conjunctive path queries) over a concrete query language. They, too, rely on description logics as an encoding mechanism.

26

9

Conclusion

In this paper, we have presented an algorithm for inferring ProGS shapes validating all possible property graphs constructed by queries specified in a subset of G-CORE. Our algorithm encodes constraints inferred from the underlying query, as well as any known shapes that hold on the inputs of the query. Internally, we rely on the description logic ALCHOI by constructing a knowledge base that entails a sound set of shapes validating all output graphs of this query. Since this DL encoding requires a reification step for first-class edges with labels and properties, we choose a clean, intermediate abstraction layer between property graphs and ALCHOI, namely the SPARQL CONSTRUCT query language and SHACL shapes, over property graphs reified in RDF. This also allows us to reuse an underlying algorithm defined for these languages, which we must extend to support a larger subset of SPARQL, including the features required by our mapping. We prove the soundness of this shape inference approach and the semantic equivalence of the shapes and queries constructed by our mappings. As future work, a larger, non-conjunctive subset of G-CORE could be supported by extending both the mapping and the capabilities of the underlying inference approach on SPARQL queries, supporting operators such as UNION in SPARQL. Such extensions may approach a limit when considering additional generic or type-level query constructs. For example, while we support a specific set of generic patterns in SPARQL, arbitrary constraints on type-level variables (i.e. variables that bind concepts) cannot be easily encoded in DL. The query mapping itself also poses interesting questions: While in our work, we do not intend to execute the SPARQL CONSTRUCT queries, the mappings could inform implementations of G-CORE over SPARQL triple stores. To this end, the RDF reification would have to be investigated empirically regarding runtime and space performance and possibly adapted, given that our mapping favors a formal ease of use over efficiency concerns.

References [1] Ghadeer Abuoda, Daniele Dell’Aglio, Arthur Keen, and Katja Hose. Transforming rdfstar to property graphs: A preliminary analysis of transformation approaches. In Proceedings of the QuWeDa 2022: 6th Workshop on Storing, Querying and Benchmarking Knowledge Graphs co-located with 21st International Semantic Web Conference (ISWC 2022), Hangzhou, China, 23-27 October 2022, volume 3279 of CEUR Workshop Proceedings, pages 17–32. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3279/paper2.pdf. [2] Lakshya A. Agrawal, Nikunj Singhal, and Raghava Mutharaju. A SPARQL to cypher transpiler: Proposal and initial results. In CODS-COMAD 2022: 5th Joint International Conference on Data Science & Management of Data (9th ACM IKDD CODS and 27th COMAD), Bangalore, India, January 8 - 10, 2022, pages 312–313. ACM, 2022. doi:10. 1145/3493700.3493757. [3] Renzo Angles, Marcelo Arenas, Pablo Barceló, Peter A. Boncz, George H. L. Fletcher, Claudio Gutierrez, Tobias Lindaaker, Marcus Paradies, Stefan Plantikow, Juan F. Sequeda, Oskar van Rest, and Hannes Voigt. G-CORE: A core for future graph query languages. In Proc. of SIGMOD, pages 1421–1432. ACM, 2018. doi:10.1145/3183713.3190654. [4] Renzo Angles, Angela Bonifati, Stefania Dumbrava, George Fletcher, Alastair Green, Jan Hidders, Bei Li, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Stefan Plantikow, Ognjen Savkovic, Michael Schmidt, Juan Sequeda, Slawek Staworko, Dominik Tomaszuk, Hannes Voigt, Domagoj Vrgoc, Mingxi Wu, and Dusan Zivkovic. Pg27

schema: Schemas for property graphs. Proc. ACM Manag. Data, 1(2):198:1–198:25, 2023. doi:10.1145/3589778. [5] Renzo Angles, Harsh Thakkar, and Dominik Tomaszuk. RDF and property graphs interoperability: Status and issues. In Proceedings of the 13th Alberto Mendelzon International Workshop on Foundations of Data Management, Asunción, Paraguay, June 3-7, 2019, volume 2369 of CEUR Workshop Proceedings. CEUR-WS.org, 2019. URL: https://ceur-ws.org/Vol-2369/paper01.pdf. [6] Renzo Angles, Harsh Thakkar, and Dominik Tomaszuk. Mapping RDF databases to property graph databases. IEEE Access, 8:86091–86110, 2020. doi:10.1109/ACCESS.2020. 2993117. [7] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. PatelSchneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. [8] Bart Bogaerts, Maxime Jakubowski, and Jan Van den Bussche. SHACL: A description logic in disguise. In Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings, volume 13416 of Lecture Notes in Computer Science, pages 75–88. Springer, 2022. doi: 10.1007/978-3-031-15707-3\_7. [9] Iovka Boneva, Jérémie Dusart, Daniel Fernández-Álvarez, and José Emilio Labra Gayo. Shape designer for shex and SHACL constraints. In Proc. of the ISWC 2019 Satellite Tracks co-located with ISWC 2019, volume 2456 of CEUR Workshop Proceedings, pages 269–272. CEUR-WS.org, 2019. URL: https://ceur-ws.org/Vol-2456/paper70.pdf. [10] Iovka Boneva, Benoît Groz, Jan Hidders, Filip Murlak, and Slawek Staworko. Static analysis of graph database transformations. In Floris Geerts, Hung Q. Ngo, and Stavros Sintos, editors, Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2023, Seattle, WA, USA, June 18-23, 2023, pages 251–261. ACM, 2023. doi:10.1145/3584372.3588654. [11] Angela Bonifati, Stefania Dumbrava, and Nicolas Mir. Hierarchical clustering for property graph schema discovery. In Proceedings of the 25th International Conference on Extending Database Technology, EDBT 2022, Edinburgh, UK, March 29 - April 1, 2022, pages 2:449– 2:453. OpenProceedings.org, 2022. doi:10.48786/EDBT.2022.39. [12] Artem Chebotko, Shiyong Lu, and Farshad Fotouhi. Semantics preserving SPARQL-to-SQL translation. Data Knowl. Eng., 68(10):973–1000, 2009. doi:10.1016/J.DATAK.2009.04. 001. [13] Richard Cyganiak, David Wood, Markus Lanthaler, Graham Klyne, Jeremy J. Carroll, and Brian McBride. RDF concepts and abstract syntax, 2014. URL: https://www.w3.org/TR/ rdf11-concepts/. [14] Thomas Delva, Birte De Smedt, Sitt Min Oo, Dylan Van Assche, Sven Lieber, and Anastasia Dimou. RML2SHACL: RDF generation taking shape. In Proc. of Knowledge Capture Conference, pages 153–160. ACM, 2021. doi:10.1145/3460210.3493562. [15] Wenfei Fan, Shuai Ma, Yanli Hu, Jie Liu, and Yinghui Wu. Propagating functional dependencies with conditions. Proc. VLDB Endow., 1(1):391–407, 2008. URL: http: //www.vldb.org/pvldb/vol1/1453901.pdf, doi:10.14778/1453856.1453901. 28

[16] Daniel Fernández-Álvarez, José Emilio Labra Gayo, and Daniel Gayo-Avello. Automatic extraction of shapes using shexer. Knowledge-Based Systems, 238:107975, 2022. doi:10. 1016/J.KNOSYS.2021.107975. [17] Benoît Groz, Aurélien Lemay, Slawek Staworko, and Piotr Wieczorek. Inference of shape graphs for graph databases. In ICDT, volume 220 of LIPIcs, pages 14:1–14:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.ICDT.2022.14. [18] Steve Harris, Andy Seaborne, and Eric Prud’hommeaux. SPARQL 1.1 query language, 2013. URL: https://www.w3.org/TR/sparql11-query/. [19] Olaf Hartig. Foundations of RDF* and SPARQL* (an alternative approach to statementlevel metadata in RDF). In Proceedings of the 11th Alberto Mendelzon International Workshop on Foundations of Data Management and the Web, Montevideo, Uruguay, June 7-9, 2017, volume 1912 of CEUR Workshop Proceedings. CEUR-WS.org, 2017. URL: https://ceur-ws.org/Vol-1912/paper12.pdf. [20] Olaf Hartig. Foundations to query labeled property graphs using SPARQL. In Joint Proceedings of the 1st International Workshop On Semantics For Transport and the 1st International Workshop on Approaches for Making Data Interoperable co-located with 15th Semantics Conference (SEMANTiCS 2019), Karlsruhe, Germany, September 9, 2019, volume 2447 of CEUR Workshop Proceedings. CEUR-WS.org, 2019. URL: https://ceur-ws. org/Vol-2447/paper3.pdf. [21] ISO. Information technology — Database languages — GQL. Standard, International Organization for Standardization, Geneva, CH, 2024. [22] Barry E. Jacobs, Alan R. Aronson, and Anthony C. Klug. On interpretations of relational languages and solutions to the implied constraint problem. ACM Trans. Database Syst., 7(2):291–315, 1982. doi:10.1145/319702.319730. [23] JTC1. GQL Database Language, gql-database-language.

2024.

URL: https://jtc1info.org/slug/

[24] Shahrzad Khayatbashi, Sebastián Ferrada, and Olaf Hartig. Converting property graphs to RDF: a preliminary study of the practical impact of different mappings. In GRADES-NDA ’22, pages 10:1–10:9. ACM, 2022. doi:10.1145/3534540.3534695. [25] Anthony C. Klug and Rod Price. Determining view dependencies using tableaux. ACM Trans. Database Syst., 7(3):361–380, 1982. doi:10.1145/319732.319738. [26] Holger Knublauch and Dimitris Kontokostas. Shapes Constraint Language (SHACL), 2017. URL: https://www.w3.org/TR/shacl/. [27] Egor V. Kostylev, Juan L. Reutter, and Martín Ugarte. CONSTRUCT queries in SPARQL. In Proc. of International Conference on Database Theory, ICDT, volume 31 of LIPIcs, pages 212–229. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs. ICDT.2015.212. [28] KRR Group at University of Oxford. Hermit OWL reasoner, 2008. URL: http://www. hermit-reasoner.com/.

29

[29] Hanâ Lbath, Angela Bonifati, and Russ Harmer. Schema inference for property graphs. In Proceedings of the 24th International Conference on Extending Database Technology, EDBT 2021, Nicosia, Cyprus, March 23 - 26, 2021, pages 499–504. OpenProceedings.org, 2021. doi:10.5441/002/EDBT.2021.58. [30] Martin Leinberger, Philipp Seifer, Claudia Schon, Ralf Lämmel, and Steffen Staab. Type checking program code using SHACL. In Proc. of ISWC, volume 11778 of LNCS, pages 399–417. Springer, 2019. doi:10.1007/978-3-030-30793-6_23. [31] Mohamed Nadjib Mami, Damien Graux, Harsh Thakkar, Simon Scerri, Sören Auer, and Jens Lehmann. The query translation landscape: a survey. CoRR, abs/1910.03118, 2019. URL: http://arxiv.org/abs/1910.03118, arXiv:1910.03118. [32] Nandana Mihindukulasooriya, Mohammad Rifat Ahmmad Rashid, Giuseppe Rizzo, Raúl García-Castro, Óscar Corcho, and Marco Torchiano. RDF shape induction using knowledge base profiling. In Prov. of the Symposium on Applied Computing, pages 1952–1959. ACM, 2018. doi:10.1145/3167132.3167341. [33] Vinh Nguyen, Hong Yung Yip, Harsh Thakkar, Qingliang Li, Evan Bolton, and Olivier Bodenreider. Singleton property graph: Adding A semantic web abstraction layer to graph databases. In (BlockSW) (CKG) co-located with ISWC 2019, volume 2599 of CEUR Workshop Proceedings. CEUR-WS.org, 2019. URL: https://ceur-ws.org/Vol-2599/CKG2019_ paper_4.pdf. [34] Pouya Ghiasnezhad Omran, Kerry Taylor, Sergio José Rodríguez Méndez, and Armin Haller. Learning SHACL shapes from knowledge graphs. Semantic Web, 14(1):101–121, 2023. doi: 10.3233/SW-223063. [35] Rossana Paciello, Luca Trani, Daniele Bailo, Valerio Vinciarelli, and Manuela Sbarra. Shapeness: A shacl-driven metadata editor. In Metadata and Semantic Research - 16th Research Conference, MTSR 2022, London, UK, November 7-11, 2022, Revised Selected Papers, volume 1789 of Communications in Computer and Information Science, pages 274–288. Springer, 2022. doi:10.1007/978-3-031-39141-5\_23. [36] Eric Prud’hommeaux, José Emilio Labra Gayo, and Harold R. Solbrig. Shape expressions: an RDF validation and transformation language. In Proc. of the International Conference on Semantic Systems, SEMANTiCS, pages 32–40. ACM, 2014. doi:10.1145/2660517. 2660523. [37] Kashif Rabbani, Matteo Lissandrini, Angela Bonifati, and Katja Hose. Transforming RDF graphs to property graphs using standardized schemas. Proc. ACM Manag. Data, 2(6):242:1–242:25, 2024. doi:10.1145/3698817. [38] Kashif Rabbani, Matteo Lissandrini, and Katja Hose. Extraction of validating shapes from very large knowledge graphs. Proc. VLDB Endow., 16(5):1023–1032, 2023. doi:10.14778/ 3579075.3579078. [39] Mariano Rodriguez-Muro and Martín Rezk. Efficient SPARQL-to-SQL with R2RML mappings. J. Web Semant., 33:141–169, 2015. doi:10.1016/J.WEBSEM.2015.03.001. [40] Philipp Seifer, Daniel Hernández, Ralf Lämmel, and Steffen Staab. From shapes to shapes: Inferring SHACL shapes for results of SPARQL CONSTRUCT queries. In Proceedings of the ACM Web Conference 2024, (WWW ’24). ACM, 2024. doi:10.1145/3589334.3645550. 30

[41] Philipp Seifer, Daniel Hernández, Ralf Lämmel, and Steffen Staab. From shapes to shapes: Inferring SHACL shapes for results of SPARQL CONSTRUCT queries (extended version). CoRR, abs/2402.08509, 2024. arXiv:2402.08509, doi:10.48550/ARXIV.2402.08509. [42] Philipp Seifer, Daniel Hernández, Ralf Lämmel, and Steffen Staab. Code for From Shapes to Shapes (V1), 2024. doi:10.18419/darus-3977. [43] Philipp Seifer, Daniel Hernández, Ralf Lämmel, and Steffen Staab. Code for From Shapes to Shapes (V2), 2024. doi:10.18419/darus-3977. [44] Philipp Seifer, Ralf Lämmel, and Steffen Staab. Progs: Property graph shapes language. In ISWC 2021, volume 12922 of LNCS, pages 392–409. Springer, 2021. doi:10.1007/ 978-3-030-88361-4\_23. [45] Blerina Spahiu, Andrea Maurino, and Matteo Palmonari. Towards improving the quality of knowledge graphs with data-driven ontology patterns and SHACL. In Proc. of the Workshop on Ontology Design and Patterns (WOP 2018) co-located with ISWC 2018, volume 2195 of CEUR Workshop Proceedings, pages 52–66. CEUR-WS.org, 2018. URL: https://ceur-ws. org/Vol-2195/research_paper_2.pdf. [46] Benjamin A. Steer, Alhamza Alnaimi, Marco A. B. F. G. Lotz, Félix Cuadrado, Luis M. Vaquero, and Joan Varvenne. Cytosm: Declarative property graph queries without data migration. In Proceedings of the Fifth International Workshop on Graph Data-management Experiences & Systems, GRADES@SIGMOD/PODS 2017, Chicago, IL, USA, May 14 - 19, 2017, pages 4:1–4:6. ACM, 2017. doi:10.1145/3078447.3078451. [47] Michael Stonebraker. Implementation of integrity constraints and views by query modification. In Proc. of SIGMOD, pages 65–78. ACM, 1975. doi:10.1145/500080.500091. [48] Harsh Thakkar, Dharmen Punjani, Jens Lehmann, and Sören Auer. Two for one: querying property graph databases using SPARQL via gremlinator. In Proceedings of the 1st ACM SIGMOD Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA), Houston, TX, USA, June 10, 2018, pages 12:1–12:5. ACM, 2018. doi:10.1145/3210259.3210271. [49] Ratan Bahadur Thapa and Martin Giese. A source-to-target constraint rewriting for direct mapping. In Proc. of ISWC, volume 12922 of LNCS, pages 21–38. Springer, 2021. doi: 10.1007/978-3-030-88361-4\_2. [50] Ratan Bahadur Thapa and Martin Giese. Optimizing SPARQL queries with SHACL. In The Semantic Web - ISWC 2023 - 22nd International Semantic Web Conference, Athens, Greece, November 6-10, 2023, Proceedings, Part I, volume 14265 of Lecture Notes in Computer Science, pages 41–60. Springer, 2023. doi:10.1007/978-3-031-47240-4\_3. [51] Dominik Tomaszuk, Renzo Angles, and Harsh Thakkar. PGO: describing property graphs in RDF. IEEE Access, 8:118355–118369, 2020. doi:10.1109/ACCESS.2020.3002018. [52] Zihao Zhao, Xiaodong Ge, Zhihong Shen, Chuan Hu, and Huajin Wang. S2ctrans: Building a bridge from SPARQL to cypher. In Database and Expert Systems Applications - 34th International Conference, DEXA 2023, Penang, Malaysia, August 28-30, 2023, Proceedings, Part I, volume 14146 of Lecture Notes in Computer Science, pages 424–430. Springer, 2023. doi:10.1007/978-3-031-39847-6\_33.

31

A

Concrete Example

Listing 1 and Listing 2 show how the example from Figure 11 could be expressed in concrete G-CORE and SPARQL syntax, respectively. We also present the full experimental data from our empirical validation (Section 7) in Table 1, Table 2, Table 3, and Table 4. Listing 1 The G-CORE query from Figure 11 expressed using concrete G-CORE syntax. In this case, all constraints, as well as set and remove clauses are expressed in separate blocks. Alternatively, in the MATCH clause, e.g., (y) could also be expresses as (y:Person), resembling more closely the abstract syntax we introduce in Definition 11.

CONSTRUCT ( x ) −[ e ]−>(y ) SET y : POI REMOVE y : Person MATCH ( x ) −[ e ]−>(y ) WHERE x . name = " Smith " AND y : Person AND e : obs

Listing 2 The SPARQL query from Figure 11 expressed using concrete SPARQL syntax. Fresh (unique) variables introduced for generic copying operations are prefixed with underscores. Note the use of filter expressions on these variables.

CONSTRUCT { ? x a m: node . ? x ?_1 ?_2 . ? x m: n t e ? e . ? e a m: edge . ? e ?_3 ?_4 . ? e m: e t n ? y . ? y a m: node . ? y ?_5 ?_6 . ? y a } WHERE { ? x a m: node . ? x ?_1 ?_2 . ? x kn : name v : Smith ? x m: n t e ? e . ? e a m: edge . ? e ?_3 ?_4 . ? e a ? e m: e t n ? y . ? y a m: node . ? y ?_5 ?_6 . ? y a FILTER ( ?_1 != m: n t e ) . FILTER ( ?_3 != m: e t n ) . FILTER ( ?_5 != m: n t e ) . FILTER ( ?_6 != l n : Person ) }

B

l n : POI . l e : obs . l n : Person .

Proofs

This section includes proofs for all propositions in the main paper, starting with some preliminary definitions used throughout these proofs.

B.1

Preliminaries

We first summarize the validation semantics of ALCHOI-based SHACL shapes we introduced in [40] (based on work by Bogaerts et al. [8]), including also the semantics of ALCHOI, for the 32

Table 1 gen_small (25000 samples) — Time: 13.94s (Median: 11.00s)

Type

Min

Max

Average

Median

Node Variables Edge Variables Atoms MATCH Atoms CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys Input Shapes Output Shapes Cand. Shapes Shape Comp. Shape Clauses Shape Negation

1.00 0.00 1.00 1.00 0.00 0.00 0.00 0.00 0.00 1.00 1.00 20.00 1.00 1.00 0.00

4.00 2.00 1.00 1.00 5.00 3.00 2.00 9.00 5.00 1.00 186.00 862.00 3.00 1.00 1.00

2.27 1.50 1.00 1.00 3.15 1.59 0.99 3.67 1.31 1.00 7.54 256.24 2.16 1.00 0.07

2.00 2.00 1.00 1.00 3.00 2.00 1.00 4.00 1.00 1.00 2.00 240.00 2.00 1.00 0.00

Table 2 gen_deep (25000 samples) — Time: 34.81s (Median: 25.00s)

Type

Min

Max

Average

Median

Node Variables Edge Variables Atoms MATCH Atoms CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys Input Shapes Output Shapes Cand. Shapes Shape Comp. Shape Clauses Shape Negation

1.00 0.00 1.00 1.00 0.00 0.00 0.00 0.00 0.00 1.00 1.00 20.00 1.00 1.00 0.00

5.00 6.00 3.00 3.00 5.00 3.00 2.00 9.00 5.00 4.00 262.00 1740.00 4.00 1.00 4.00

3.52 2.54 1.21 2.21 3.20 1.57 0.99 3.64 1.33 2.63 7.53 408.25 2.96 1.00 0.28

4.00 2.00 1.00 2.00 3.00 2.00 1.00 4.00 1.00 3.00 2.00 370.00 3.00 1.00 0.00

33

Table 3 gen_wide (25000 samples) — Time: 42.23s (Median: 29.50s)

Type

Min

Max

Average

Median

Node Variables Edge Variables Atoms MATCH Atoms CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys Input Shapes Output Shapes Cand. Shapes Shape Comp. Shape Clauses Shape Negation

1.00 0.00 1.00 1.00 0.00 0.00 0.00 0.00 0.00 1.00 1.00 26.00 1.00 1.00 0.00

5.00 6.00 3.00 3.00 5.00 3.00 2.00 9.00 5.00 4.00 256.00 1884.00 7.00 2.00 4.00

3.52 2.53 1.21 2.20 3.18 1.56 0.98 3.61 1.33 2.61 9.85 510.25 4.95 1.86 0.39

4.00 2.00 1.00 2.00 3.00 2.00 1.00 4.00 1.00 3.00 2.00 468.00 5.00 2.00 0.00

Table 4 gen_large (25000 samples) — Time: 51.68s (Median: 36.00s)

Type

Min

Max

Average

Median

Node Variables Edge Variables Atoms MATCH Atoms CONSTRUCT WHEN Clauses SET Clauses REMOVE Clauses Distinct Labels Distinct Keys Input Shapes Output Shapes Cand. Shapes Shape Comp. Shape Clauses Shape Negation

1.00 0.00 1.00 1.00 0.00 0.00 0.00 0.00 0.00 3.00 1.00 56.00 1.00 1.00 0.00

5.00 6.00 3.00 3.00 5.00 3.00 2.00 9.00 5.00 7.00 258.00 2502.00 3.00 1.00 4.00

3.54 2.55 1.22 2.21 3.16 1.54 0.98 3.59 1.32 5.07 11.18 610.32 2.16 1.00 0.32

4.00 3.00 1.00 2.00 3.00 2.00 1.00 4.00 1.00 5.00 2.00 576.00 2.00 1.00 0.00

34

sake of completeness. Definition 38 (Summary of ALCHOI Semantics (cf. [7])). An ALCHOI knowledge base K is a pair (T , A), where T is a finite set of axioms and A is a finite set of assertions. In a slight abuse of notation, given an ABox A, we write A to refer to the knowledge base (∅, A), and given a TBox T we write T to refer to (T , ∅). An interpretation I is a pair (∆I , ·I ) consisting of a set ∆I , called the domain, and a function ·I such that we have for each individual name a ∈ I, an element aI ∈ ∆I ; for each concept name A ∈ C, a subset AI ⊆ ∆I ; and for each role name p ∈ R, a relation pI ⊆ ∆I × ∆I . The function ·I is extended to concept descriptions as follows: ⊥I = ∅, ⊤I = ∆I , {a}I = {aI }, (C ⊓ D)I = C I ∩ DI , (C ⊔ D)I = C I ∪ DI , (¬C)I = ⊤I \ C I (∃p.C)I = {d ∈ ∆I | (d, e) ∈ pI with e ∈ C I }, (∃p− .C)I = {d ∈ ∆I | (e, d) ∈ pI with e ∈ C I }, (∀p.C)I = {d ∈ ∆I | for all e ∈ ∆I , if (d, e) ∈ pI then e ∈ C I }, (∀p− .C)I = {d ∈ ∆I | for all e ∈ ∆I , if (e, d) ∈ pI then e ∈ C I }. An interpretation I is a model of a knowledge base K = (T , A) if and only if C I ⊆ DI for every axiom C ⊑ D in T ; pI ⊆ rI for every axiom p ⊑ r in T ; aI ∈ C I for every assertion a : C in A; and (aI , bI ) ∈ pI for every assertion (a, b) : p in A. Given two knowledge bases, K1 and K2 , K1 entails K2 , denoted K1 |= K2 , if and only if every model I of K1 is also a model of K2 . For the validation semantics, we interpret RDF graphs as ALCHOI A-Boxes G, and define SHACL validation based on the validation knowledge base (TG , G), relying on Definition 39. We say that a graph G is proof-valid regarding a set of ALCHOI axioms (e.g., a set of shapes) if and only if this set is consistent with this validation knowledge base of G (Definition 40). Definition 39 (RDF Graph Validation Semantics). The ALCHOI axioms TG of an RDF graph G are the TBox consisting of the: F 1. Domain Closure Assumption (DCA): ⊤ ≡ a∈I {a}. 2. Unique Name Assumption (UNA): {a}⊓{b} ≡ ⊥, for each pair of distinct individual names a, b ∈ I. 3. Closed-World Assumption (CWA): F • A ≡ a : A∈G {a}, for each concept name A ∈ C, F • ∃p.{a} ≡ (b,a) : p∈G {b}, and F • ∃p− .{a} ≡ (a,b) : p∈G {b}, for each role name p ∈ R, and for each individual name a ∈ I. 35

Definition 40 (Semantics of ALCHOI Shapes). A graph G is valid regarding a set S of ALCHOI shapes, denoted valid(G, S), if and only if G is proof-valid according to S; that is, if and only if S is consistent with this validation knowledge base of G. We next formalize extended graphs, that were informally introduced in Section 5. An extended graph unifies four different graphs: The input graph (which is given), the intermediate graph defined by renaming concept and role names matched by the query, the output graph constructed by the query (again modulo renaming), as well as the graph defined by variables and their bindings. Note, that the notion of extended graphs is only formally required in proofs; they are not explicitly constructed in our method. Definition 41 (Extended Graph). Given an RDF graph Gin and a query H ← (P, F ), we define S 1. the intermediate graph Gmed := µ∈JP,F Keccq-p µ(P ), Gin

2. the variable concept graph GV containing an assertion a : Vx if and only if there exists a valuation µ ∈ JP, F Keccq-p and µ(x) = a, Gin 3. the output graph Gout := JqKeccq Gin ,

4. and the extended graph Gext := Gin ∪ Ġmed ∪ GV ∪ G̈out .

B.2

Shape Mapping (Proposition 33)

We prove, that the mapping for shapes, pro7→shacl (s), preserves the validation semantics of ProGS. Proof. We consider shape targets and constraints separately. To this end, we first show that if and only if a node n (or edge e) is a target of the shape s in a property-graph G, then the corresponding node n in pg7→rdf (G) with the name n b is a target of the shape pro7→shacl (s). We differentiate between the possible target queries of a shape s: 1. n. The target query n targets exactly one node in G, namely n, which is uniquely mapped to n b in pg7→rdf (G), per Definition 21. The target query pro7→shacl (n) = {b n} targets all individuals in the extension of {b n} in pg7→rdf (G), which by definition is n b if and only if n b is in pg7→rdf (G), which is the case if and only if n was in G. Thus, if n is a target in G, then (and only then) is n b a target in pg7→rdf (G). 2. lN . This targets all nodes n ∈ N such that lN ∈ λ(n) in G (Figure 4). The corresponding RDF graph pg7→rdf (G) includes, by construction, exactly one triple (b n, rdf:type, lc N ) for each n ∈ N , and no other occurrences of the concept name lc (Definition 21). The target N c query pro7→shacl (lN ) is mapped to lN (Definition 23). By definition, this targets exactly the individuals in the extension of lc N ; in the constructed graph this includes exactly the subjects of triples of the form (b n, rdf:type, lc b for N ), and thus exactly the mapped nodes n all n identified above. 3. kN . This targets all nodes n ∈ N where σ(n, kN ) ̸= ∅ (Figure 4). The corresponding RDF graph pg7→rdf (G) includes, by construction, the triple (b n, kc b) if and only if σ(n, kN ) = N, v {v}, and for each n ∈ N , and no other occurrences of the role name kc N (Definition 21). (Note, that by definition we consider only singleton sets of values.) The target query maps to pro7→shacl (kN ) = ∃kc N .⊤ (Definition 23). By definition, this target query includes all nodes in the extension of ∃kc N .⊤, and with analogous reasoning to the previous case exactly the mapped nodes n b for all n identified above. 36

4. The remaining cases for e, lE , and kE are equivalent to the previous cases. Next, we consider the constraints. That is, we first show that when a node n (or edge e) satisfies the constraint of shapes s in a property-graph G, then there is a corresponding node n in b that satisfies the constraint of pro7→shacl (s). We show this by assuming pg7→rdf (G) with the name n that this corresponding node does not exist; we cover all cases for constraint components, by induction. We start with the base cases. 1. ⊤. This constraint is vacuously satisfied for any target node. The mapped constraint pro7→shacl (⊤) = ⊤ is also always vacuously satisfied for any target node. 2. n. This constraint is satisfied for a target node nt in G if and only if nt = n. Assume that the node nbt in pg7→rdf (G) would not satisfy the constraint pro7→shacl (n) = {b n}. This would imply that nbt ̸= n b. However, we know that nt = n from which nbt = n b follows directly. 3. lN . This constraint is satisfied for a target node nt if and only if lN ∈ λ(nt ) in G. Assume that the node nbt in pg7→rdf (G) would not satisfy the constraint pro7→shacl (lN ) = lc N . Then, c the individual nbt must not be in the extension of lN . However, by construction, the graph bt , rdf:type, lc b is in the extension of lc pg7→rdf (G) contains the triple (n N ) and thus n N . This contradicts the previous assumption. Indeed, the same can be shown for the inverse direction: Consider an individual nbt that is in the extension of lc N and thereby satisfying this constraint in pg7→rdf (G). Now assume that pg7→rdf (G) is constructed from the graph G where the corresponding node nt does not satisfy the corresponding constraint lN , i.e. it holds that lN ̸∈ λ(nt ). If this is the case, then pg7→rdf (G) does not contain the triple (nbt , rdf:type, lc N ), since the only way to construct that triple in the mapping is if lN ∈ λ(nt ). However, if the graph does not contain this triple, then nbt cannot be in the extension of lc N , which contradicts the previous assumption. 4. ∃kN .(= v). This constraint is satisfied for a target node nt if and only if σ(nt , kN ) = {v}. \ Assume that the individual nbt in pg7→rdf (G) would not satisfy pro7→shacl (∃kN .⊤) = ∃k N .⊤. Then, nbt must not be in the extension of ∃kc .b v . However, by construction, the graph N bt , kc b) if and only if σ(nt , kN ) = {v}. Since this is the pg7→rdf (G) contains the triple (n N, v case, we can follow that nbt is indeed in the extension of ∃kc v . This is a contradiction, so N .b our previous assumption must be false. Indeed, the same can be shown for the inverse direction: Consider an individual nbt that is in the extension of ∃kc v , thereby satisfying the constraint in pg7→rdf (G). Now assume N .b that pg7→rdf (G) is constructed from the graph G where the corresponding node nt does not satisfy the corresponding constraint ∃kN .(= v), i.e. it holds that v ̸∈ σ(nt , kN ). If this is the case, then pg7→rdf (G) does not contain the triple (nbt , kc b), since the only way N, v to construct that triple in the mapping is if σ(nt , kN ) = {v}. However, if the graph does \ not contain this triple, then nbt cannot be in the extension of ∃kc v , which contradicts the N .b previous assumption. 5. ∃kN .⊤. The proof for this case is very similar to the previous case, with the only difference that we only care about σ(nt , kN ) being non-empty. 6. ¬ϕN . We assume that the condition under investigation holds for ϕN . That is, for any target node nt in G that it satisfies ϕN if and only if, nbt satisfies pro7→shacl (ϕN ) in pg7→rdf (G). The negated cases follow directly. 37

7. ϕ1N ∧ ϕ2N . We assume that the condition under investigation holds for ϕ1N and ϕ2N . That is, for any target node nt in G that it satisfies ϕ1N if and only if, nbt satisfies pro7→shacl (ϕ1N ) in pg7→rdf (G) (and the same for ϕ2N , respectively). The conjunction follows directly. 8. We omit equivalent cases for edges (e.g., ϕE ) since their proofs work analogously. 9. ∃→ ϕE . This constraint is satisfied if and only if for the target node nt exists ρ(e) = (nt , n′ ), and e satisfies the constraint ϕE . Assume that the individual nbt in pg7→rdf (G) would not satisfy the constraint pro7→shacl (∃→ ϕE ) = ∃m:nte.pro7→shacl (ϕE ). By construction, we know that pg7→rdf (G) contains the triple (nbt , m:nte, eb). By our induction hypothesis, we can assume that eb satisfies the constraint pro7→shacl (ϕE ) in pg7→rdf (G), since we know that e satisfies ϕE in G. Because of both of these facts, we can follow that nbt is in the extension of ∃m:nte.pro7→shacl (ϕE ), and therefore satisfies this constraint. This contradicts the previous assumption. For the inverse direction, the same argument applies: Consider an individual nbt that is in the extension of ∃m:nte.pro7→shacl (ϕE ), thereby satisfying the constraint in pg7→rdf (G). Now assume that pg7→rdf (G) is constructed from the graph G where the corresponding node nt does not satisfy the corresponding constraint ∃→ ϕE , i.e. it holds that either ρ(e) = (nt , n′ ) is not in ρ, or e does not satisfy ϕE . By the induction hypothesis, we know that e must satisfy ϕE . Thus, the edge ρ(e) = (nt , n′ ) must not exist. If this is the case, then pg7→rdf (G) does not contain the triple (nbt , m:nte, eb), since the only way to construct that triple in the mapping is if there is an e where ρ(e) = (nt , n′ ). However, if the graph does not contain this triple, then nbt cannot be in the extension of ∃m:nte.pro7→shacl (ϕE ), which contradicts the previous assumption. 10. ∃← ϕE . This case works exactly analogously to the previous case (only in reverse). 11. ⇒ ϕN . This case works analogously to the previous cases (except we are considering node constraints instead of edge constraints). 12. ⇐ ϕN . Again, this case works analogously to the previous case (only in reverse).

B.3

Query Mapping (Proposition 34)

We prove Proposition 34 by defining and proving the following two lemmas. Lemma 42 (Invertable Graph Mapping). Given a PG G, then the mapping to an RDF graph can be inverted such that G = pg7→rdf −1 (pg7→rdf (G)). Proof. The mapping algorithm defined in Definition 21 can be trivially inverted to construct a property graph from an RDF graph by matching on triples included in the RDF graph required to construct nodes, edges, labels, and properties. The inverted algorithm is partial in the domain of RDF graphs, as there might be triples that are not matched; this suffices for Lemma 42. Lemma 43 (Soundness of Query Mapping Modulo Lemma 42). Given a PG G and a SGCQ q, then pg7→rdf (JqKG ) = Jsgcq7→eccq (q)Kpg7→rdf (G) .

Proof. We need to show that mapping the result of a SGCQ query is equivalent to mapping both the input graph and the query itself. We will show the lemma by showing that a SGCQ query is equivalent to an IQL (Definition 26) query, given the defined mapping (Figure 10), referring 38

to the semantics of SGCQ directly, and the semantics of IQL indirectly through the mapping to ECCQ queries (Figure 10). To this end, we consider the two parts of the queries (referred to here as matching and constructing) separately. We start by proving that the matching parts of both query languages produce equivalent results, modulo certain conditions we will define below. At the core, the semantics of both languages, as far as the matching part of the queries is concerned, differ in that in SGCQ we obtain a mapping from variable names to node and edge IDs, whereas in corresponding IQL (and ECCQ) queries we obtain a mapping from (a superset of equivalent) variable names to IRIs, including both the encoded node and edge IDs present in SGCQ results, but also all IRIs that correspond to labels and properties, since they are explicitly matched by variables, and not implicitly included as for SGCQ. For the sake of readability, we will refer to, e.g., queries as q (SGCQ) and q ′ (IQL or ECCQ) throughout this proof. Indeed, we apply this notation to any objects that can be mapped (such as PG graphs G and RDF graphs G′ ). Furthermore, we use IQL and ECCQ somewhat interchangeably; in particular, we refer to IQL for its syntax and to ECCQ for the semantics of IQL queries, directly. Matching We show that the sets of bindings Ω obtained by a SGCQ query q on a PG G = (N, E, ρ, λ, σ) is equivalent to the set of bindings obtained by the corresponding ECCQ query q ′ on an RDF graph G′ . The notion of equivalency we use is defined as follows: Definition 44 (Equivalency of Bindings). Two sets of valuations Ω (for SGCQ q on G) and Ω′ (for ECCQ q ′ on G′ ) are equivalent, written Ω ≈ Ω′ , if and only if 1. ∀µ ∈ Ω, ∀x ∈ dom(µ) such that µ(x) = n, then (a) ∃µ′ ∈ Ω′ : µ′ (x) = n b, (b) ∀l ∈ L if l ∈ λ(n) and ⊖l ̸∈ Sx , then ∃µ′ ∈ Ω′ : µ′ (cx ) = b l, (c) ∀k ∈ K, ∀v ∈ V if σ(n, k) = {v} and ⊖k ̸∈ Sx , then ∃µ′ ∈ Ω′ : µ′ (px ) = b k and µ′ (ox ) = vb. 2. ∀µ′ ∈ Ω′ , ∀x ∈ dom(µ′ ) : such that µ(x) = n b, then (a) ∃µ ∈ Ω : µ(x) = n, (b) µ′ (cx ) = b l such that l ∈ λ(n) and ⊖l ̸∈ Sx (or µ′ (cx ) = m:node), (c) µ′ (px ) = b k and µ′ (ox ) = vb such that σ(n, k) = {v} and ⊖k ̸∈ Sx (or µ′ (px ) = m:node), 3. ∀µ ∈ Ω, ∀x, y, z ∈ dom(µ) such that µ(x) = n1 , µ(y) = n2 , µ(z) = e, then (a) ∃µ′ ∈ Ω′ : µ′ (x) = n c1 , µ′ (y) = n c2 , and µ′ (z) = eb, (b) ∀l ∈ L if l ∈ λ(e) and ⊖l ̸∈ Sz , then ∃µ′ ∈ Ω′ : µ′ (cz ) = b l, (c) ∀k ∈ K, ∀v ∈ V if σ(e, k) = {v} and ⊖k ̸∈ Sz , then ∃µ′ ∈ Ω′ : µ′ (pz ) = b k and µ′ (oz ) = vb. 4. ∀µ′ ∈ Ω′ , ∀x, y, z ∈ dom(µ′ ) : such that µ(x) = n c1 , µ(y) = n c2 , µ(z) = eb, then (a) ∃µ ∈ Ω such that µ(x) = n1 , µ(y) = n2 , µ(z) = e, (b) µ′ (cz ) = b l such that l ∈ λ(e) and ⊖l ̸∈ Sz (or µ′ (cx ) = m:node), (c) µ′ (pz ) = b k and µ′ (oz ) = vb such that σ(e, k) = {v} and ⊖k ̸∈ Sz (or µ′ (pz ) = m:node). 39

where cx , px and ox are the same fresh variables defined for x in Definition 3, and we write, e.g., n and n b as implicit conversions between both representations of node (respectively edge) as IDs or IRI. We will first consider the two patterns (xn , ξ) and (xn , xn ):(xe , ξ) of SGCQ, and then their composition. 1. Case qSGCQ = (x, ξ). According to Figure 10, this is equivalent to an IQL query pattern of shape MN (x, WL , WK , WV , RL , RK ). We need to show equivalency for the bindings Ω obtained for (x, ξ) on G, and Ω′ obtained for the corresponding MN (x, WL , WK , WV , RL , RK ) on G′ . To this end, we show that Case 1 of Definition 44 holds (note, that the precondition of Case 2 is never satisfied, and we thus do not consider this case). We show this inductively on the structure of (x, ξ). We start with the base case where ξ = ∅, continue with singleton cases, and finally consider union of two sets. (a) ξ = ∅. Given: n ∈ N (in G) and µ(x) = n. Then, by construction of G′ , G′ contains the triple (b n, rdf:type, node). The corresponding ECCQ contains only the triple patterns {x : xC , (x, xI ) : xR , x : m:node}, as well as the filter pattern {xR ̸= nte}. We consider the three cases of Definition 44 (1) and (2): b; • Case 1.a and 2.a (Definition 44). By definition of G′ , x : m:node is satisfied for n Both x : xC and (x, xI ) : xR are trivially satisfied at least for one µ′ as the graph always contains the triple n b : m:node (and it is only then satisfies). Thus, there exists a mapping µ′ ∈ Ω′ such that µ′ (x) = n b exactly in this case. • Case 1.b and 2.b (Definition 44). For any label l ∈ L where l ∈ λ(n), by definition G′ contains the triple (b n, rdf:type, b l). We first assume that there is no ⊖l ∈ Sx . Then there exists a mapping µ′ ∈ Ω′ such that µ′ (x) = n b and µ′ (cx ) = b l, since x : xC is in the ECCQ. (The reverse is true by the same reasoning: If l ̸∈ λ(n), then G′ does not contain (b n, rdf:type, b l) by its construction, and the pattern can never be satisfied.) If there is a ⊖l ∈ Sx , then the corresponding ECCQ contains in addition the filter pattern xC ̸= b l. According to the semantics of ECCQ (Definition 4) we remove exactly the bindings µ′ such that µ′ (cx ) = b l. Thus, such a binding does not exist, as was required. (The same reasoning applies for the reverse case.) • Case 1.c and 2.c (Definition 44). For any property value pair k ∈ K, v ∈ V where σ(n, k) = {v}, by definition G′ contains the triple (b n, b k, vb). We first assume that there is no ⊖k ∈ Sx . Then there exists a mapping µ′ ∈ Ω′ such that µ′ (x) = n b and µ′ (ox,k ) = vb, since (x, xI ) : xR is in the ECCQ. (The reverse is true by the same reasoning: If not σ(n, k) = {v}, then G′ does not contain (b n, b k, vb) by its construction, and the pattern can never be satisfied.) If there is a ⊖k ∈ Sx , then the corresponding ECCQ contains in addition the filter pattern xR ̸= b k. According to the semantics of ECCQ (Definition 4) we remove exactly the bindings µ′ such that µ′ (px ) = b l. Thus, such a binding does not exist, as was required. (The same reasoning applies for the reverse case.) (b) ξ = { :l} ∪ ξr . Given: n ∈ N (in G) and µ(x) = n; equivalency holds for ξr (induction hypothesis). For any l ∈ L it holds that if { :l} is satisfied (for n), it must be the case n, rdf:type, b l). that l ∈ λ(n). By construction, therefore, G′ contains the triple (b b The corresponding ECCQ contains only the additional triple pattern {x : l}, which is thus satisfied in G′ in at least one µ′1 . Since we know that equivalency holds regarding 40

ξr (by the induction hypothesis), we know that there exists a µ′2 for this query where µ′2 (x) = n b, and that therefore, µ′1 ∼ µ′2 . With the same reasoning as for the previous case, there then exists a mapping µ′ = µ′1 ∪ µ′2 ∈ Ω′ where µ′ (x) = n b. For any l ∈ L where { :l} is not satisfied (for n), also l ̸∈ λ(n). Then, by construction, G′ does not contain the triple (b n, rdf:type, b l); the inverse of the previous case applies, since b {x : l} cannot be satisfied under these conditions. Therefore, there does not exist the µ′ in Ω′ . (c) ξ = { .k = v} ∪ ξr . Given: n ∈ N (in G) and µ(x) = n; equivalency holds for ξr (induction hypothesis). For any k ∈ K and v ∈ V it holds that if { .k = v} is satisfied (for n), it must be the case that σ(n, k) = {v}. By construction, therefore, G′ contains the triple (b n, b k, vb). The corresponding ECCQ contains only the additional triple pattern (x, vb) : b k, which is thus satisfied in G′ in at least one µ′1 where µ′1 (x) = n b. Since we know that equivalency holds regarding ξr (by the induction hypothesis), we know that there exists a µ′2 for this query where µ′2 (x) = n b, and that therefore, µ′1 ∼ µ′2 . With the same reasoning as for the previous case, there then exists a mapping µ′ = µ′1 ∪ µ′2 ∈ Ω′ such that µ′ (x) = n b. The inverse case works analogously to the second case. (d) ξ = { .k} ∪ ξr . Given: n ∈ N (in G) and µ(x) = n; equivalency holds for ξr (induction hypothesis). For any k ∈ K it holds that if { .k} is satisfied (for n), it must be the case that σ(n, k) = {v} for some v ∈ V . By construction, therefore, G′ contains a triple (b n, b k, vb). The corresponding ECCQ contains only the additional triple pattern (x, ox,k ) : b k, which is thus satisfied in G′ in at least one µ′1 , where ′ ′ µ (x) = n b and µ (ox,k ) = vb. Since we know that equivalency holds regarding ξr (by the induction hypothesis), we know that there exists a µ′2 for this query where µ′2 (x) = n b. Furthermore, we know that ox,k ̸∈ dom(µ′2 ) since the pattern is unique by definition. Therefore, µ′1 ∼ µ′2 . With the same reasoning as for the previous case, there then exists a mapping µ′ = µ′1 ∪ µ′2 ∈ Ω′ where µ′ (x) = n b. The inverse case works analogously to the second case. 2. Case qSGCQ = (x, y):(z, ξ). According to Figure 10, this is equivalent to an IQL query pattern of shape ME (x, y, z, WL , WK , WV , RL , RK ). We need to show equivalency of the set of bindings Ω obtained for (x, y):(z, ξ) on G, and Ω′ obtained for the corresponding ME (x, y, z, WL , WK , WV , RL , RK ). To this end, we show that Case 2 of Definition 44 holds. (Again, the premise of the other case is not satisfied). We show this case inductively on the structure of (x, y):(z, ξ). We start with the base case where ξ = ∅, continue with singleton cases, and finally consider union of two sets. (a) ξ = ∅. Given: n1 , n2 ∈ N , e ∈ E (in G), ρ(e) = (n1 , n2 ) and µ(z) = e, µ(x) = n1 , and µ(y) = n2 . Then, by construction of G′ , G′ contains and the triples (b e, rdf:type, edge), (c n1 , rdf:type, node), (c n2 , rdf:type, node), (c n1 , nte, eb), and (b e, etn, n c2 ). The corresponding ECCQ contains only the triple patterns {(x, z) : m:nte, (z, y) : m:etn, z : z C , (z, z I ) : z R , z : m:edge}, as well as the filter pattern {z R ̸= etn}. We consider the three cases of Definition 44 (3) and (4): • Case 3.a and 4.a (Definition 44). By definition of G′ , z : m:edge is satisfied for zb; Both z : z C and (z, z I ) : z R are trivially satisfied at least for one µ′ as the graph always contains the triple eb : m:node. Similarly, both (x, z) : m:nte and (z, y) : m:etn are satisfied by the definition of G′ (see above) for at least one µ′ . This µ′ satisfies µ′ (x) = n c1 , µ′ (y) = n c2 and µ′ (z) = eb, given the triples included in G′ (by definition) shown above. 41

• Case 3.b and 4.b (Definition 44). This case is equivalent to Case 1.b for 1. • Case 3.c and 4.c (Definition 44). This case is equivalent to Case 1.c for 1. (b) ξ = { :l} ∪ ξr . Analogous to 1.a.ii. (c) ξ = { .k = v} ∪ ξr . Analogous to 1.a.iii. (d) ξ = { .k} ∪ ξr . Analogous to 1.a.iv. 3. Case qSGCQ = {Γ1 , Γ2 }. For this case, we need to show that the equivalency of two sets of bindings holds under the join operation. That is, when Ω1 ≈ Ω′1 and Ω2 ≈ Ω′2 then (Ω1 ▷◁ Ω2 ) ≈ (Ω′1 ▷◁ Ω′2 ). This follows directly from the definition of ▷◁: By the definition of equivalency, both Ω and Ω′ must share corresponding bindings for common variables, while Ω′ might have additional variables. Thus, two mappings µ1 and µ2 are compatible if and only if µ′1 and µ′2 are compatible. Constructing We show that the graph Go = (No , Eo , ρo , λo , σo ) constructed by a SGCQ query q on a PG G = (N, E, ρ, λ, σ) is equivalent to the graph G′o obtained by the corresponding ECCQ query q ′ on an RDF graph G′ . To this end, we already showed that the set of bindings Ω obtained by the matching part of q is equivalent (w.r.t. Definition 44) to the set of bindings Ω′ obtained by the matching part of q ′ (i.e. Ω ≈ Ω′ ). In the following, w.l.o.g., we assume that this is the case; similarly, we assume that any fresh IRIs and node or edge IDs generated by either ECCQ or SGCQ queries, respectively, are the same modulo the graph mapping relation. To this end, we refer to them as aµ(x) or aµ′ (x) where µ and µ′ are SGCQ and ECCQ mappings from equivalent bindings Ω and Ω′ : Thus, b aµ(x) = aµ′ (x) holds. We will first consider the two patterns (xn , ξ) and (xn , xn ):(xe , ξ) of SGCQ, and then their composition. 1. Case qSGCQ = (x, S). We prove this construction by inductions on the structure of S. Without loss of generality, we assume that S never contains both ⊕l and ⊖l (or ⊕k = v and ⊖k); indeed, these cases behave like the removal cases. For each case, we show that both constructing an RDF output graph G′o and mapping Go to an RDF graph G′′o produces the same set of triples. (a) S = ∅. Here we construct the graph Go consisting of nodes n = µ(x) for all bindings µ ∈ Ω, which is defined as ∪µ∈Ω {{µ(x)}, ∅, ∅, λµ(x) , σµ(x) } (Definition 12). The query maps to CN (x, AL , AK , V ), the semantics of which are defined by the ECCQ construction patterns {x : xC , (x, xI ) : xR , x : m:node} if x ∈ V or {x : m:node} otherwise, as a union over all µ′ ∈ Ω′ with Ω′ ≈ Ω. If x ̸∈ V , then {x : m:node} constructs aµ′ (x) , for which a corresponding aµ(x) is constructed, given the assumption made above. Otherwise, we know for each µ(x) = n in Ω there exists a µ′ ∈ Ω′ where µ′ (x) = n b; the pattern x : m:node constructs therefore the triple x : m:node in G′o . Mapping Go to G′′o also includes the triple x : m:node by definition of the mapping (Definition 21). The remainder is the same for either case (where we use n for either n = aµ(x) or n = µ(x)). Secondly, we know that for each l ∈ λ(n) there exists a µ′ ∈ Ω′ where n, rdf:type, b l) in µ′ (cx ) = b l. The pattern x : xC constructs the respective triple (b ′ ′′ the output graph Go . Mapping Go to Go also includes this triple, since λµ(x) above includes l, which is mapped to exactly the required triple. Finally, we know that for each k ∈ K, v ∈ σ(n, k) there exists a µ′ ∈ Ω′ where µ′ (px ) = b k and µ′ (ox ) = vb; thus, I R ′ b pattern (x, x ) : x constructs the triple (b n, k, vb) for this µ in G′o . Mapping Go to ′′ Go also includes this triple, since σµ(x), k is v, which is mapped to the required triple. No other triples are included in either construction. Therefore, G′o is equal to G′′o . 42

(b) S = {⊕l} ∪ Sr . We assume, by the induction hypothesis, that the equivalency of the output graphs G′o and G′′o holds for Sr . The additional set clause ⊕l modifies the graph Go by adding l to λ(n) for all n ∈ N such that µ(x) = n, for some µ ∈ Ω (which may also be a fresh identifier of the form aµ(x) ). The equivalent ECCQ q ′ includes an additional pattern of the form x : b l (and equivalent bindings for x). By the semantics of ECCQ we know that G′o therefore includes (b n, rdf:type, b l) for all µ′ (x) = n b. By ′′ the definition of our graph mapping, we know that Go must include this triple, too, since l ∈ λ(n) for the respective n. Thus, G′o = G′′o . (c) S = {⊖l} ∪ Sr . We assume, by the induction hypothesis, that the equivalency of the output graphs G′o and G′′o holds for Sr . The additional remove clause ⊖l modifies the graph Go by exclusion of l in λ(n) for all n ∈ N where µ(x) = n, for some µ ∈ Ω. If such a remove clause exists, AL does not include the pattern ⊕l, by definition, for these x. Thus, the respective triples are never constructed (see also the base case), and G′o does not include (b n, rdf:type, b l). Similarly, G′′o does not include this triple, ′ since l is not in λ(n). Therefore, Go = G′′o . (d) S = {⊕k = v} ∪ Sr . This case is equivalent to the case with ⊕l. (e) S = {⊖k} ∪ Sr . This case is equivalent to the case with ⊖l. 2. Case qSGCQ = (x, y):(z, S). We can again prove this construction by inductions on the structure of S. Without loss of generality, we assume that S never contains both ⊕l and ⊖l (or ⊕k = v and ⊖k); indeed, these cases behave like the removal cases. For each case, we show that both constructing an RDF output graph G′o and mapping Go to an RDF graph G′′o produces the same set of triples. (a) S = ∅. Here we construct the graph Go consisting of nodes n1 = µ(x), n2 = µ(y), and e = µ(z) for all bindings µ ∈ Ω, defined as ∪µ∈Ω {{v, u}, {e}, {e→ (v, u)}, λµ(x) , σµ(x) } (Definition 12). The query maps to CE (x, y, z, AL , AK , V ), the semantics of which are defined by the ECCQ construction patterns of the form {(x, z) : m:nte, (z, y) : m:etn, z : z C , (z, z I ) : z R , z : m:edge} if z ∈ V or {(x, z) : m:nte, (z, y) : m:etn, z : m:edge} otherwise, as a union over all µ′ ∈ Ω′ with Ω′ ≈ Ω. If z ̸∈ V , then {(x, z) : m:nte, (z, y) : m:etn, z : m:edge} constructs aµ′ (z) , for which a corresponding aµ(z) is constructed, given the assumption made above. If z ∈ V , then µ(z) = e in Ω and there exists a µ′ ∈ Ω′ where µ′ (z) = eb. The remainder is the same for either case (where we use e for either e = aµ(z) or e = µ(z)). First, we know for each µ(x) = n1 and µ(y) = n2 in Ω there exists a µ′ ∈ Ω′ where µ′ (x) = n c1 and µ′ (y) = n c2 . The triples (c n1 , nte, eb), and (b e, etn, n c2 ) are therefore triples in G′o . Mapping Go to G′′o also includes (x, z) : m:nte and (z, y) : m:etn by definition of the mapping (Definition 21), since ρ(e) = (n1 , n2 ) in Go . Similarly, (b e, rdf:type, edge) is in G′o since z : m:edge is in q ′ . The triple is also in G′′o by its construction, since e ∈ Eo (edges of Go ). The remainder of this case, namely the inclusion of labels l ∈ L and properties k ∈ K is exactly analogous to case 1.a), with only very minor changes (i.e. e instead of n). No other triples are included in either construction. Therefore, G′o is equal to G′′o . (b) Remaining Cases. Since there are not further differences between edges and nodes not already covered by the first case, the remaining cases are exactly analogous (modulo minor notational differences) to the node cases in Case 1 of this proof. 3. Case qSGCQ = {B1 , B2 }. Finally, we show that when G′o,1 = G′′o,1 and G′o,2 = G′′o,2 , then also G′o = G′′o . G′o is simply the union of triples in both G′o,1 and G′o,2 (Definition 4). G′′o is the graph resulting from mapping Go to RDF. Go is the (graph) union of the graphs Go,1 and 43

Go,2 defined (N1 ∪N2 , E1 ∪E2 , ρ, λ, σ) where ∀e ∈ E1 ∪E2 : ρ(e) = ρ1 (e) if e ∈ E1 else ρ2 (e), ∀x ∈ N1 ∪ N2 ∪ E1 ∪ E2 , k ∈ K : λ(x) = λ1 (x) ∪ λ2 (x), and σ(x, k) = σ1 (x, k) ∪ σ2 (x, k). We consider the individual components of Go . (a) N1 ∪ N2 . Then G′′o contains (b n, rdf:type, node) for n ∈ N1 ∪ N2 . Given the equivalency of the graphs G′o,1 = G′′o,1 and G′o,2 = G′′o,2 , G′o clearly also contains these triples. (b) E1 ∪E2 . Then G′′o contains (b e, rdf:type, edge) for e ∈ E1 ∪E2 . Given the equivalency of the graphs G′o,1 = G′′o,1 and G′o,2 = G′′o,2 , G′o clearly also contains these triples. (c) ρ. Then G′′o contains (c n1 , nte, eb), and (b e, etn, n c2 ) for e ∈ E1 ∪E2 (and the respective n1 , n2 ). Given the equivalency of the graphs G′o,1 = G′′o,1 and G′o,2 = G′′o,2 , G′o clearly also contains these triples. (d) λ. Then G′′o contains (b u, rdf:type, b l) for u ∈ N1 ∪E1 ∪N2 ∪E2 . Given the equivalency ′ of the graphs Go,1 = G′′o,1 and G′o,2 = G′′o,2 , G′o clearly also contains these triples. (e) σ. Then G′′o contains (b u, b k, vb) for u ∈ N1 ∪ E1 ∪ N2 ∪ E2 . Given the equivalency of the graphs G′o,1 = G′′o,1 and G′o,2 = G′′o,2 , G′o clearly also contains these triples.

Finally, the proof for Proposition 34 follows directly from both lemmas. Proof. The proof follows directly from Lemma 42 and Lemma 43.

B.4

Shape Entailment (Proposition 35)

Following the proofs in [40], it suffices to show that the axioms in Σ are indeed valid on all extended graphs. We can adapt the respective proposition from [40] as given in Proposition 45. Note that Proposition 33 and Proposition 34 guarantee that this proposition suffices for showing the soundness of our method for property graphs, sProGS and SGCQ. Proposition 45 (Modification of Proposition 35). For every extended graph Gext of a ECCQ q and a set of ALCHOI shapes Sin where valid(Gin , Sin ), valid(Gext , infer(q, S)). We show for each of the seven steps of the inference algorithm separately that Proposition 45 holds, defining Lemma 48 through Lemma 54. We refer to the set of axioms inferred in each of the seven steps of Definition 31 as Σ1 through Σ7 as a shorthand. For each proof, we have the following preliminary assumptions: 1. A set of sProGS shapes S ′ , which can be mapped via pro7→shacl (S ′ ) to ALCHOI axioms (representing SHACL shapes) S; these are the input shapes to the problem. Any input graph G′ is assumed to be valid regarding S ′ . Thus, Proposition 33 ensures that for any of these input graphs G′ also G = pg7→rdf (G′ ) is valid regarding S = pro7→shacl (S ′ ). 2. A SGCQ query q ′ , which can be mapped to a ECCQ q = H ← (P, F ) = sgcq7→eccq (q ′ ); this is the input query of the problem. 3. Finally, we also build on Proposition 3S2S as was defined and proven in [40]. We repeat this proposition below (Definition 46) and adapt it to our notation, but refer to [40] for its proof, which applies here as well. NB: The proof is simple and relies on the property that extended graphs are defined as the union of four different graphs that do not share a vocabulary for concept names or role names. 44

Definition 46 (Modification of Proposition 3S2S [40]). Given an RDF graph Gin and an ECCQ q, let the graphs Gmed , Gout , and Gext be defined according to Definition 41. For every ALCHOI axiom φ that does not include names with dots, the following equivalences hold: 1. valid(Gin , {φ}), if and only if valid(Gext , {φ}). 2. valid(Gmed , {φ}), if and only if valid(Gext , {φ̇}). 3. valid(Gout , {φ}), if and only if valid(Gext , {φ̈}). In the remainder of this section, we prove the individual parts of Definition 31. Note that some proofs are directly based on, and others in part inspired by, [40] (or, more precisely, the extended version of that paper [41]). We first start with the auxiliary Lemma 47, which shows that generic patterns, that is atomic patterns of the form x : xC and (x, xI ) : xR do not restrict variables under certain conditions. Lemma 47. For a ECCQ q with variable x, inclusion of the pattern x : xC can never change the set of bindings for variable x, regardless of the input graph, as long as the query pattern also includes at least one pattern of the form x : A for any concept name A. Note that this is always true for queries utilizing our mapping. The equivalent holds for (x, xI ) : xR and (x, y) : p or (x, a) : p. Proof. This trivially follows from the definition of ECCQ syntax and semantics. First note that for patterns of the form x : xC (and (x, xI ) : xR , respectively), the variable xC (and xR , xI , respectively) cannot occur again within the query, by definition. Consider two query patterns P1 = x : A and P2 = x : xC . Let there be an individual name a and graph G. We can consider the following cases and what that means for the intersection of both patterns. 1. a ∈ µP1 (x) and a ∈ µP2 (x). Trivially, the intersection includes a. 2. a ∈ / µP1 (x) and a ∈ / µP2 (x). Trivially, the intersection does not include a, but neither does pattern x : A. 3. a ∈ / µP1 (x), but a ∈ µP2 (x). Trivially, the intersection does not include a, but neither does pattern x : A. 4. a ∈ µP1 (x), but a ∈ / µP2 (x). This is the interesting case where x : xC could possibly restrict the bindings for x : A in the intersection of both patterns. However, this case cannot occur. Assume that there was such an a in G. Then this means that G includes a : A. However, since xC is unrestricted, x : xC clearly matches this triple. This contradicts the initial assumption; thus, this case cannot exist. Thus, the intersection of x : A and x : xC is the same as x : A in all cases. The same can be shown for the (x, xI ) : xR case. We next consider the lemmas associated with the individual steps of the algorithm. Lemma 48 (Pert. to Definition 31.1). For every Gext of a ECCQ q, it holds that valid(Gext , Σ1 ). Proof. Adapted from [40]. This follows directly from Proposition 3S2S . All input graphs are valid regarding S and Σ1 = S, by definition. Lemma 49 (Pert. to Definition 31.2). For every Gext of a ECCQ q, it holds that valid(Gext , Σ2 ).

45

Proof. Inspired by [40]. We consider both directions of this case separately. We begin by proving the conditional case by contradiction. Let vcg(P ) be acyclic, G be a graph and let x be a variable occurring in P , and let C be a concept defined as l l l C≡ A⊓ ∃p. Cu ⊓ ∃p− . Cu . x : A∈P

(x,u) : p∈P

(u,x) : p∈P

Assume that there is an individual name c in G such that c : C is valid in Gext , but c : Vx is not valid in Gext . We will show that this leads to a contradiction. Assume, w.l.o.g., that P includes a single concept assertion x : A that includes x, and no role assertions of the form (x, b) : r (b is an individual name). If there were other atoms of these forms, we could define A as an auxiliary atom that is equivalent to their intersection instead. Further assume, w.l.o.g., that P does not include generic patterns of the form x : xC or (x, xI ) : xR . Patterns of these forms can never restrict the bindings of x (see Lemma 47), and if only generic patterns occur for a variable x in a query, Vx is not defined in this case anyway. Finally, assume – also w.l.o.g. – that Gext includes {a : Vy , (a, c) : r, c : A, (c, b) : s, b : Vz } Let Ω be the set of all mappings µ such that µ(P ) ⊆ G. Then, by definition there exist the mappings µ1 , µ2 ∈ Ω such that µ1 (y) = a and µ2 (z) = b, but there does not exist a mapping µ ∈ Ω such that µ(x) = c (given the assumption about x given above). Then also µ1 (x) ̸= c and µ2 (x) ̸= c. Let Py be the part of pattern P that connects with variables y and x, but not z. Let Pz be the part of pattern P that connects with variables z and x, but not y. Finally, let µy1 = µ1 var(P )\{x} ,

µz1 = µ1 var(P )\{x} ,

µy2 = µ2 var(Py )\{x} ,

µy2 = µ2 var(Pz )\{x} .

y

z

Then, µ1 = µy1 ∪ {x 7→ µ1 (x)} ∪ µz1 and µ2 = µy2 ∪ {x 7→ µ2 (x)} ∪ µz2 . Since µy1 and µz2 share no variables, µ3 = µy1 ∪ {x 7→ c} ∪ µz2 is a mapping. By the definition of the semantics of ECCQ µ3 ∈ Ω. Then c : Vx is valid in Gext . This contradicts the initial assumptions, from which we conclude Vx ⊒ C. We next consider the other direction. Assume a to be an arbitrary individual name such that {a} ⊑ Vx is valid in the extended graph Gext . For each operand k in the intersection of Definition 31.2 we show separately that {a} ⊑ k, assuming that the respective component is defined. We assume in all three cases, w.l.o.g., that P does not include generic patterns of the form x : xC or (x, xI ) : xR , with the same reasoning as before (Lemma 47). d 1. For k = x : A∈P A: If {a} ⊑ Vx , then by definition a is an instance of variable x in P , i.e. a ∈ µ(x). Then for each concept name A occurring in an atomic pattern of the form x : A ∈ P there must be a : A ∈ Gin (since otherwise a ̸∈ µ(x)), so also a : A ∈ Gext for each such A. Therefore, {a} ⊑ k. d 2. For k = (x,u) : p∈P ∃p. Cu : If {a} ⊑ Vx , then by definition a is an instance of variable x in P , i.e. a ∈ µ(x). Then for each property name p occurring in an atomic pattern of the form (x, u) : p ∈ P , one of two cases applies: if u is an individual name, then there must be (a, u) : p ∈ Gin , so also (a, u) : p ∈ Gext for such p. If u is a variable name, then there must be (a, b) : p ∈ Gin , so also (a, b) : p ∈ Gext , and also b ∈ µ(u) (since otherwise a ̸∈ µ(x)). Therefore, {a} ⊑ k. d 3. For k = (u,x) : p∈P ∃p− . Cu : Analogous to the previous case. 46

If one or more components k are defined, then l l {a} ⊑ A⊓ ∃p. Cu ⊓ x:A∈P

(x,u):p∈P

l

∃p− . Cu .

(u,x):p∈P

At least one component k must be defined, since otherwise the concept Vx would not be defined, as there must exist either x : A ∈ P for some concept name A or (x, u) : p ∈ P (or (x, u) : p ∈ P respectively) for some property p, if x ∈ var(P ). Note that this also covers the cases where only generic patterns (e.g., x : xC ) exist for a variable x; here, the concept Vx is not defined. (Similarly, the case where x ̸∈ P and a is fresh is also not possible, since we initially assumed that x ∈ P .) Thus, at least one of the components k must be defined; this proves the second direction. We thus prove both directions of this case. Lemma 50 (Pert. to Definition 31.3). For every Gext of a ECCQ q, it holds that valid(Gext , Σ3 ). Proof. Inspired by [40]. We consider both directions of this proof separately. G G Ä ⊑ Cu ⊔ VxA u : A∈H

x∈var(H)

Let a be an arbitrary individual name such that {a} ⊑ Ä is valid in Gext . By construction, this means that a : A ∈ Gout . This atom can arise for two reasons: 1. There is an atom v : A ∈ H such that a : A is an instance of pattern v : A, and v is either the concept name a or a variable x. If v is a, then {a} ⊑ Cv is trivially valid in Gext . Otherwise, v is x such that a is a binding of x or freshly generated (in the case where x ̸∈ FP ) and then it holds that a : Vx ∈ Gext , so {a} ∈ Cv is valid in Gext . Therefore, {a} ⊑ u : A∈H Cu is valid in Gext . 2. There is an atom x : xC in P and H, with xC ̸= A ̸∈ F , and a is an instance of x (i.e. a : Vx ∈ VxA ≡ Vx ⊓ A, as well as {a} ⊑ Vx and {a} ⊑ A and then also F Gext ). Since A {a} ⊑ x∈var(H) Vx is valid in Gext . Thus, at least one of the operands of the top-level disjunction holds for {a} via either case 1 or 2, and since {a} was arbitrary, this direction of the equivalency holds in general. We consider the inverse direction next. G G Ä ⊒ Cu ⊔ VxA u : A∈H

x∈var(H)

Here, we consider the two components of the top-level disjunction separately and show that in either case the property holds for all possible (i.e. arbitrary) individuals a. F F 1. Ä ⊒ u : A∈H Cu . Let a be an arbitrary individual name such that {a} ⊑ u : A∈H Cu is valid in Gext . Then there is at least one atom v : A ∈ H such that {a} ⊑ Cv is valid in Gext . If v is a, then a : A ∈ Gout , and thus a : Ä ∈ Gext . Otherwise, v is a variable x, and a : Vx ∈ Gext . By the definition of variable concepts, a : A ∈ Gout , so a : Ä ∈ Gext . Therefore, {a} ⊑ Ä is valid in Gout . F F 2. Ä ⊒ x∈var(H) VxA . Let a be an arbitrary individual name with {a} ⊑ x∈var(H) VxA is valid in Gext . Thus, {a} ⊑ VxA for some x ∈ var(P ). Since VxA ≡ Vx ⊓A, therefore {a} ⊑ Vx and {a} ⊑ A in Gext for that x, and there is an atom x : xC in P and H and xC ̸= A ̸∈ F . By the definition of the semantics of generic patterns x : xC , therefore a : A ∈ Gout , so a : Ä ∈ Gext . 47

Therefore, the complete subsumption holds as well. Since both directions hold, we have thus shown the equivalency. Lemma 51 (Pert. to Definition 31.4). For every Gext of a ECCQ q, it holds that valid(Gext , Σ4 ). Proof. Inspired by [40]. Since the proofs for the inverse role cases are extremely similar, we consider only the first three axioms of Definition 31.4. We start by considering: F

(u,v) : p∈H Cu ⊑ ∃p̈. Cv

Let I be the canonical model of Gext . By definition of the validation knowledge base of a graph, aI ∈ (∃p̈. Cv )I if and only if there exists an individual name b where (a, b) : p̈ ∈ Gext and (aI , bI ) ∈ pI . If there is an atomic pattern (u, v) : p ∈ H where u is the individual name a or a variable x, and v is the individual name b S or a variable y (and thus aI ∈ CIu ), then by I construction, (a, b) : p̈ ∈ Gext . Thus, when a ∈ (u,v) : p∈H CIu , then aI ∈ (∃p̈. Cv )I . Hence, F (u,v) : p∈H Cu ⊑ ∃p̈. Cv . Next, we consider the following rule: F F ∃p̈. Cv ⊑ (u,v) : p∈H Cu ⊔ (x,xI ) : xR ∈H Vx Let I be the canonical model of Gext . By definition of the validation knowledge base of a graph, aI ∈ (∃p̈. Cv )I if and only if there exists an individual name b where (a, b) : p̈ ∈ Gext and (aI , bI ) ∈ pI . By construction, (a, b) : p̈ ∈ Gext arises in exactly two cases: 1. If there exists an atom (u, v) : p ∈ H where u is the individual name a or a variable x, and I I I I v is the F individualI name b or a variable F y (and thus a ∈ Cu ). Then a ∈ (∃p̈. Cv ) if I a ∈ (u,v) : p∈H Cu . Hence, ∃p̈. Cv ⊑ (u,v) : p∈H Cu . I R C I I 2. If there is an atom (x, Fx ) : x in IH, with x ̸= p ̸∈ F F (and thus a ∈ Vx ). Then I I I a ∈ (∃p̈. Cv ) if a ∈ (u,v) : p∈H Cu . Hence, ∃p̈. Cv ⊑ (x,xI ) : xR ∈H Vx .

In either case, one of the top-level disjunctions of the initial axiom holds; thus the axiom is satisfied in all cases. Finally, we consider the third rule: F F ∃p̈.⊤ ≡ (u,v) : p∈H (Cu ⊓∃p̈. Cv ) ⊔ x∈var(H) Vxp By definition of the validation knowledge base of a graph, aI ∈ (∃p̈.⊤)I if and only if there exists an individual name b where (a, b) : p̈ ∈ Gext and (aI , bI ) ∈ pI . By construction, the inclusion (a, b) : p̈ ∈ Gext occurs in exactly two cases: 1. if there exists an atom (u, v) : p ∈ H where u is the individual name a or a variable x and v is the individual name b or a variableFy. Then, aI ∈ CIv and aI ∈ (∃p̈. Cv )I , so aI ∈ (∃p̈.⊤)I in this case if and only if aI ∈ (u,v) : p∈H CIu ⊓(∃p̈. Cv )I . 2. If there is an atom (x, xI ) : xR in P, with xR ̸= p ̸∈ F and x in voc(H). In this case, Vxp ≡ Vx ⊓ ∃p.Vxp,o . aI ∈ Vxp I and aI ∈ (∃p̈. Cv )I ; for all x, y ∈ var(P ) and p ∈ V if (x, xI ) : xR ∈ P , xR ̸= p ̸∈ F and (x, y) : pF̸∈ P , otherwise Vxp ≡ ⊥ and Vxp,o ≡ ⊥ so aI ∈ (∃p̈.⊤)I in this case if and only if aI ∈ x∈var(H) Vxp . Since at least one of these cases applies by construction, equivalency follows for their union. Lemma 52 (Pert. to Definition 31.5). For every Gext of a ECCQ q, it holds that valid(Gext , Σ5 ). 48

Proof. Adapted from [40]. For every property p ∈ voc(P ), ṗ ⊑ p is true, since Definition 41 guarantees that Gmed ⊆ Gin . Lemma 53 (Pert. to Definition 31.6). For every Gext of a ECCQ q, it holds that valid(Gext , Σ6 ). Proof. Adapted from [40]. Given P contains (x, y) : p and neither x nor y occur in any other atomic patterns in P – including any generic patterns such as (x, xI ) : xR – then from any (a, b) : p ∈ Gin it follows that (a, b) : ṗ ∈ Gmed , and thus p ⊑ ṗ. Lemma 54 (Pert. to Definition 31.7). For every Gext of a ECCQ q, it holds that valid(Gext , Σ7 ). Proof. Adapted from [40]. Let p ∈ voc(P ), r ∈ voc(H), and P contain only the atomic pattern (x, y) : p; let H contain only (x, y) : r; and let neither H nor P contain other atomic patterns involving x, y, p or r. If this is the case, for any (a, b) : ṗ ∈ Gmed matched in the intermediate graph, we construct (a, b) : r̈ ∈ Gout in the output graph. From this, we can infer that ṗ ⊑ r̈. Since r does not occur again in H, it also follows that r̈ ⊑ ṗ holds for all extended graphs Gext of the query.

B.5

Query Extension (Proposition 36)

Proof. We prove the property JqKeccq = JExt(q)Keccq for any ECCQ q and RDF graph G. We conG G sider, without loss of generality, a query pattern {x : A, x : xC } and the query template {x : xC }, and further the two cases where either xC ̸= A in F , or xC ̸= A is not in F . 1. xC ̸= A ̸∈ F . Then, it follows from the semantics of ECCQ queries, that if x : A is satisfied in a graph G, then the graph contains a : A for some a where a ∈ µ(x); then A ∈ µ(x̄C ). As a result, the output graph also contains a : A, since x : xC ∈ H (in the assumption above). Therefore, we can add the pattern x : xC A to the template of the query, without changing the semantics of the query, as defined in Ext(q). 2. xC ̸= A ∈ F in this case, Ext(q) does not change the query q given above, by definition, since the concept name of the potential candidate for extension, x : A, is in F . The property case can be shown to hold with the same reasoning.

49

Related documents

• String Diagrams for Process Mining#978502
• ZigZag Trie: A Novel Index for Contextual Queries#978503
• A Functional Pilot for Certified Freshness-Aware Semantic--Spatial Range Retrieval#978504
• Efficiently Linking Unstructured Data for Multi-step Reasoning#978505