arXiv CSopen access

On the Semantics of Generative SPARQL

On the Semantics of Generative SPARQL

arXiv:2606.23875v1 [cs.DB] 22 Jun 2026

Ratan Bahadur Thapa1∗ , Steffen Staab1,2 1 Institute for Artificial Intelligence, University of Stuttgart, Stuttgart, Germany 2 University of Southampton, United Kingdom {ratan.thapa, steffen.staab}@ki.uni-stuttgart.de

Abstract We extend SPARQL with a generative query construct, called GenOp, whose evaluation calls a language model and produces typed solution mappings. We define the semantics of the GenOp in the query in a way that maintains the fixeddataset assumption, on which formal semantics of SPARQL build, and extend solution mappings with values generated by the language model. We formalize the semantics of the extended language over these mappings using a compatibility relation that generalizes equality and supports similaritybased matching between RDF terms and generated values. We analyze the semantic consequences of generative query patterns, focusing on mapping-level recursion induced by the reuse of generated bindings. Under deterministic bounded generation and finite candidate coverage assumptions, we characterize acyclic and stratified fragments with fixpoint semantics, establish algebraic equivalence and semanticspreserving rewrite rules, and provide an executable evaluation method; and we show that data and combined complexity coincide with those of standard SPARQL.

1

Introduction

SPARQL (Prud’hommeaux and Seaborne 2008) is the de facto standard for querying RDF (Manola et al. 2004). The semantics of SPARQL query patterns is defined in terms of (partial) solution mappings, with operators analogous to relational-algebra operators (Codd 1970) and evaluated with respect to a fixed RDF graph (Pérez, Arenas, and Gutierrez 2006; Pérez, Arenas, and Gutierrez 2009). All semantic characterizations, equivalence results, and algebraic rewrite rules are stated relative to an underlying RDF graph that remains fixed during query evaluation (Schmidt, Meier, and Lausen 2010). Recent knowledge graph centric applications increasingly require exploratory enrichment over existing datasets (Hogan et al. 2021), such as synthesizing missing attributes, proposing related entities, or producing textual descriptions. Large language models (LLMs) can generate such values on demand, but current practice treats calls to language models operationally, as external procedures, middleware invocations, or prompt-based post-processing, outside the query algebra (Zhao, Agrawal, and Abbadi 2024; Tan et al. 2025; Khabiri et al. 2025; Saeed, De Cao, and Papotti 2024; ∗

Corresponding author: [email protected]

Dai et al. 2024; Molli et al. 2025). As a result, their interaction with SPARQL operators is not governed by the declarative semantics of the query language, and standard questions about query equivalence, recursion, and termination remain outside the scope of these works. One way to formally capture the semantics of operators that generate new values at query time is to relax the fixeddataset assumption and allow the queried graph to be discovered during evaluation, as in link-traversal querying (Hartig, Bizer, and Freytag 2009). However, such approaches rely on dynamic data discovery and require specialized semantics that preclude algebraic equivalence, recursion, and fixpoint reasoning under a fixed graph (Hartig, Bizer, and Freytag 2009; Florescu, Levy, and Mendelzon 1998; Hernández, Rivero, and Ruiz 2019). In contrast, we aim to preserve the fixed-dataset assumption of SPARQL while extending only the space of solution mappings under a bounded generation assumption. We integrate generative inference into the SPARQL algebra through a generative query pattern GenOp. A GenOp instantiates a prompt template using the currently bound variables, invokes a specified generative model, parses finitely many outputs, and returns them as bindings for designated output variables. At the semantic level, our central design choice is to lift generation to the level of solution mappings rather than RDF graphs. To support algebraic composition with standard SPARQL operators, we define query semantics over typed solution mappings that distinguish RDF-derived bindings from generated bindings. Each binding records its origin, keeping evaluation relative to a fixed RDF graph. To combine symbolic and generated values, we replace equalitybased compatibility with a generalized compatibility relation: it coincides with equality on RDF bindings and allows similarity-based matching between RDF terms and generated values, following the general spirit of similarity-based querying(Kiefer, Bernstein, and Stocker 2007; Zheng et al. 2016; Ferrada, Bustos, and Hogan 2024), via deterministic lexicalization and a variable-indexed similarity threshold. Although GenOp is non-recursive syntactically, cyclic dependencies may arise when generated bindings are reused as inputs to other GenOps. Such cycles occur solely at the level of extended solution mappings and induce selfreferential constraints on admissible solutions. We formal-

ize these dependencies via a consequence operator over sets of typed mappings and interpret cyclic queries using fixpoint semantics. We restrict ourselves to the deterministic bounded-generation assumption, where each fixed model specifier and instantiated prompt returns a fixed finite parsed output set, yielding a finite generated-value universe for each query instance. Under this assumption, query evaluation reduces to fixpoint computation over a finite mapping domain and therefore terminates by standard fixpoint arguments for finite lattices (Ullman 1988; Abiteboul, Hull, and Vianu 1995; Green et al. 2013). Let us explore the difficulty of including value-generating LLM calls into SPARQL query processing with the following example. Example 1. Let G = {:Paris a :City} be an RDF graph, and consider the following pseudo-generative SPARQL query: SELECT ?x ?y ?z WHERE { ?x a :City . GenOp("Suggest a topic related to ?x and ?z" AS ?y, GPT-4o). GenOp("Suggest a city related to topic ?y" AS ?z, Gemini 1.5 Pro). } Ideally, the first GenOp would behave analogously to a basic graph pattern: it should use currently available bindings and otherwise range over admissible combinations of variable assignments. Typical procedural implementations (e.g., (Florescu, Levy, and Mendelzon 1998)) require all input variables of a GenOp to be bound before invocation. In this query, however, each GenOp depends on a value produced by the other, so neither can be evaluated under such an execution model. The problem is therefore that procedural execution enforces an evaluation order that blocks mutually dependent generative calls; our semantics instead provides a declarative interpretation that admits jointly supported bindings. Under our semantics (see Appendix A.1), evaluation is defined over sets of typed solution mappings, and the basic graph pattern yields the initial mapping µ0 = ?x 7→ :Paris. Each GenOp induces a mapping transformer. A typed mapping µ ⊇ µ0 assigning ?y and ?z is admissible iff ?y is among the finitely many outputs generated from the first GenOp prompt instantiated with µ(?x) and µ(?z), and ?z is analogously supported by the second GenOp prompt instantiated with µ(?y). The two GenOp occurrences therefore induce a cyclic dependency over the mapping domain. The declarative solution set is given by the relevant fixpoint semantics, while executable evaluation validates finite candidates against the recursive equations under the candidate-coverage assumptions stated in Sect. 6. Overall, we isolate a semantic foundation for hybrid symbolic–generative querying in which generative operators are formalized as context-sensitive transformers of solution mappings. Their interaction is defined declaratively by fixpoint semantics over finite, typed mapping domains, supporting formal reasoning about correctness, termination,

and equivalence for queries that incorporate generative inference. Our contributions are as follows. (i) We extend SPARQL with a generative operator GenOp and define a denotational semantics over typed solution mappings together with a generalized compatibility relation. Generated values remain confined to solution mappings and do not induce fact derivation, distinguishing the semantics from existential-rule languages and chase-based formalisms(Abiteboul, Hull, and Vianu 1995; Calı̀, Gottlob, and Pieris 2010; Calı̀ et al. 2010). Recursion is interpreted over mappings rather than by model construction, distinguishing our approach from answer-set and stable-model approaches (Przymusinski 1990; Niemelä 1999). (ii) We characterize acyclic, stratified, and cyclic generative patterns and provide fixpoint semantics for the recursive cases. Recursive admissibility is defined by a self-support condition. The underlying fixpoint theory is classical (Ullman 1988; Abiteboul, Hull, and Vianu 1995), while its application to context-dependent, deterministic set-valued mapping transformers over solution mappings is new. (iii) We establish algebraic equivalence results and semantics-preserving rewrite rules for monotone and stratified fragments with respect to the fixpoint semantics over typed solution mappings, identifying both the preserved standard SPARQL algebraic laws and new algebraic rewritings in the presence of context-dependent generative patterns. (iv) We provide an executable realization of the recursive semantics by reducing evaluation to self-support checking over finite candidate mapping sets localized to strongly connected components of the dependency graph. This evaluation avoids chase-based reasoning and yields soundness and completeness relative to candidate coverage, following established treatments of logic programs with external operators (Eiter et al. 2006).Under the bounded-generation assumption and finite candidate coverage assumptions, both data and combined complexity coincide with those of standard SPARQL evaluation(Pérez, Arenas, and Gutierrez 2006) (Section 7).

2

Related Work

The formal semantics of SPARQL as an algebra over solution mappings, together with results on containment, entailment and optimization under a fixed RDF dataset, are well established (Pérez, Arenas, and Gutierrez 2009; Arenas and Pérez 2011; Chekol 2016; Kontchakov and Kostylev 2016; Kaminski, Kostylev, and Grau 2017). Our work builds on this foundation but departs from it by allowing solution mappings to be extended by generative operators during evaluation. A distinct line of SPARQL extension for the Web of Linked Data has formalized semantics and computability under full-Web and reachability-based interpretations (Hartig, Bizer, and Freytag 2009; Hartig 2013), examined the empirical behavior and limitations of link-traversal query execution over heterogeneous Web data (Umbrich et al. 2015), and proposed dedicated Web-of-Data query languages that separate navigation from query evaluation, such as LDQL (Hartig and Pérez 2016). These approaches ad-

dress open-world data discovery and computability over potentially unbounded graphs. Recent systems integrate LLMs into knowledge-graph querying pipelines. SparqLLM invokes LLMs as auxiliary services during SPARQL execution (Molli et al. 2025), while other work uses declarative orchestration of LLMassisted API and database calls around existing query engines (Khabiri et al. 2025). Related approaches combine retrieval and generation in pipeline architectures (Yang et al. 2025). In all cases, language model invocation remains external to the query algebra and is treated operationally, with generated outputs consumed procedurally rather than defined by the query semantics. Related relational data-management work has also studied SQL and SQL-adjacent query processing with languagemodel calls, including hybrid querying over relational databases and LLMs, SQL-style querying of LLMs, and query engines over unstructured data (Zhao, Agrawal, and Abbadi 2024; Saeed, De Cao, and Papotti 2024; Dai et al. 2024; Tan et al. 2025). These works establish model invocation as a useful operational primitive in query processing and study how such calls can be exposed through SQL-style syntax, user-defined functions, physical operators, or dedicated execution engines. In all cases, focus is primarily executionoriented and SQL-centric: model calls are incorporated as callable components of a query pipeline, without developing a formal denotational semantics for generated bindings inside a solution-mapping algebra. Fixpoint semantics for recursive queries originate in deductive databases and logic programming (Ullman 1988; Abiteboul, Hull, and Vianu 1995), with stratified and wellfounded semantics providing principled treatments of negation (Przymusinski 1990; Van Gelder 1989). Existential rules and Datalog± extend these ideas via domainexpanding inference (Calı̀, Gottlob, and Pieris 2010; Calı̀ et al. 2010). Our setting differs fundamentally: the RDF domain remains fixed, no facts are derived, and recursion is resolved over a finite space of typed solution mappings. Treatments of logic programs with external operators (Eiter et al. 2006) are conceptually closest, but does not address algebraic query languages or mapping-level recursion under fixed-dataset semantics.

3

Syntax and Semantics

We now introduce the syntax of generative SPARQL and define its denotational semantics in terms of typed solution mappings. Let V, I, B and L be countably infinite disjoint sets of variables, Internationalized Resource Identifiers (IRIs), blank nodes and literals, respectively. Let T = I∪B∪L be a set of RDF terms, and let Tgen be a disjoint set of generated terms. An RDF triple is an element of (I ∪ B) × I × T , and a triple pattern is an element of (I ∪ L ∪ V) × (I ∪ V) × (I ∪ L ∪ V). An RDF graph G is a finite set of RDF triples, and a basic graph pattern (BGP) is a finite set of triple patterns. A generative SPARQL query is a graph pattern P defined

by the following grammar: P := BGP | GenOp(π(X), Y, M) | Filter F (P) | Proj L (P) | P Union P | P Join P (1) | P Minus P | P Diff F P | P Opt F P, where GenOp(π(X), Y, M) is a generative pattern with prompt template π containing placeholders X ⊆ V, output variables Y ⊆ V with X ∩ Y = ∅, and generative model specifier M (abstract); L ⊆ V is a projection list, and F is a filter formula built from atoms bound(v), (v = c), (v = v ′ ) s.t. v, v ′ ∈ V and c ∈ T using logical connectives ∧ and ¬. The set of variables in a graph pattern P is denoted by var(P), and the size of P, i.e., the number of symbols in its writing, by |P|. Definition 1. Let P be a graph pattern. A BGP or generative GenOP pattern Q is said to occur in P, written Q ⪯ P, if Q is a syntactic subpattern of P, defined inductively by: (i) if P = Q, then Q ⪯ P; (ii) if P = Filter F (P ′ ) or P = Proj L (P ′ ), then Q ⪯ P iff Q ⪯ P ′ ; (iii) if P = P1 Op P2 for Op ∈ {Join, Union, Minus, Diff, Opt}, then Q ⪯ P iff Q ⪯ P1 or Q ⪯ P2 . Let {} be the empty graph pattern, with J{}KG = {∅} and var({}) = ∅. Definition 2. Let P be a graph pattern and let Q ⪯ P be a designated occurrence. The surrounding pattern of Q in P, denoted P \ {Q}, is obtained by replacing only that occurrence by the empty pattern {} and then simplifying the result by the following pruning ⇝ rules: 1. Filter F ({}) ⇝ {} and Proj L ({}) ⇝ {}; 2. For the Op ∈ {Join, Union, Minus, Diff, Opt} and graph pattern P ′ , {} Op P ′ ⇝ P ′

and

P ′ Op {} ⇝ P ′ ;

provided that the resulting graph pattern is well formed. Definition 3. (Well formed) A graph pattern P defined by the grammar 1 is well-formed if it satisfies the following conditions: (i) for every g = GenOp(π(X), Y, M) occurrence such that g ⪯ P, X ⊆ var(P \ {g}) \ Y ; (ii) for every filter Filter F (P), var(F) ⊆ var(P); and (iii) for every projection Proj L (P), L ⊆ var(P). We now define solution mappings, typing, and compatibility. Definition 4. A typed term is a pair (t, τ ) where either (i) t ∈ T and τ = rdf, or (ii) t ∈ Tgen and τ = gen. A typed solution mapping is a partial function µ : V ⇀ (T × {rdf}) ∪ (Tgen × {gen}) with domain domµ ⊆ V. Let Σ be a finite alphabet and Σ∗ be the set of all finite strings over Σ. Definition 5. A canonical lexicalization consists of fixed deterministic functions Canon : T → Σ∗

and

Lex : Tgen → Σ∗ ,

where Canon maps each RDF term to a canonical string and Lex maps each generated term to its textual realization.

Remark 1. In an implementation, literals can be lexicalized by their lexical forms. IRIs can be lexicalized by a deterministic label policy, for example by using an associated rdfs:label when available and otherwise a stable rendering of the IRI. Blank nodes can be lexicalized by a stable system-defined identifier or by a deterministic boundedneighbourhood description. We require only that the lexicalization policy is fixed during evaluation; the semantics does not require labels or blank-node descriptions to be semantically complete. Definition 6. Let Str≃ : Σ∗ × Σ∗ → [0, 1] be a symmetric similarity function, and let θ : V → (0, 1] be a variablespecific threshold function (default 1). For any two typed terms (t, τ ), (t′ , τ ′ ), we define Sim as, Sim((t, τ ), (t′ , τ ′ )) =  1 if    Str≃ (Canon(t), Lex(t′ ))  Str≃ (Lex(t), Canon(t′ ))   Str≃ (Lex(t), Lex(t′ ))

(τ = τ ′ = rdf) ∧ (t = t′ ) if τ = rdf, τ ′ = gen if τ = gen, τ ′ = rdf if τ = τ ′ = gen

Definition 7 (Variable-indexed similarity). For each variable v ∈ V, let ≈v be the binary relation on typed terms defined by α ≈v β

iff

Sim(α, β) ≥ θ(v).

Since only finitely many typed terms can bind a given variable under the bounded-generation assumption, the reflexive and transitive closure of ≈v therefore induces finitely many equivalence classes; we fix a deterministic total order ⪯ on typed terms, and write repv (α) for the ⪯ -minimal representative of the equivalence class of α under ≈v . Definition 8. For a variable v and typed terms α, β, we define canonical compatibility, Compatv (α, β) = ⊤

iff

repv (α) = repv (β).

Definition 9. Two typed solution mappings µ1 and µ2 are compatible, written µ1 ∼ µ2 , iff for every variable v ∈ domµ1 ∩ domµ2 , Compatv (µ1 (v), µ2 (v)) = ⊤. If µ1 ∼ µ2 , their canonical union µ1 ⊎ µ2 is the mapping with domain domµ1 ∪ domµ2 defined by  repv (µ1 (v)) if v ∈ domµ1 ∩ domµ2 , (µ1 ⊎ µ2 )(v) = µ1 (v) if v ∈ domµ1 \ domµ2 ,  µ2 (v) if v ∈ domµ2 \ domµ1 .

Generative patterns. We model a generative pattern as a set-valued mapping that transforms an instantiated prompt into finitely many tuples of generated terms via a generative step followed by parsing, while leaving the surrounding query algebra unchanged. A model specifier M induces finite-valued operations ∗ CallM : Σ∗ → 2Σ and ParseM , where CallM returns answer strings and ParseM returns tuples of generated terms. For every fixed query instance (P, G), we assume that iterating the generative occurrences of P from the RDF bindings in G yields finitely many generated terms. For complexity results, we assume constants n1 , n2 such that |CallM (s)| ≤ n1

and

|ParseM (a)| ≤ n2

for all relevant M, s, a, and that generated terms have bounded representation length. Definition 10. Let g = GenOp(π(X), Y, M), and let Y = ⟨y1 , . . . , yk ⟩ be a fixed ordering, where k = |Y |. Let |Y | ∗ CallM : Σ∗ → 2Σ and ParseM : Σ∗ → 2Tgen return finite sets. Let G be an RDF graph and S a context supply, i.e., a set of typed solution mappings, such that every µc ∈ S satisfies X ⊆ domµc . The evaluation of g with respect to S over G is the set:   a ∈ CallM (π [µc ] ),     [ (v1 , . . . , vk ) ∈ ParseM (a), S JgKG = µc ⊎ ν ν = {yi 7→ (vi , gen) | 1 ≤ i ≤ k},    µc ∈S  µc ∼ ν, where π [µc ] is the prompt obtained from π by replacing each placeholder in X by the lexicalization of its binding under µc . Example 2. Let G = {:Paris a :City} and the query: SELECT ?x ?y ?z WHERE { ?x a :City . GenOp("Describe the city ?x" AS ?y, GPT-4o). } By evaluating BGP, we get context supply µc = {?x 7→ (:Paris, rdf)} for the GenOp. Then, prompt instantiation produces π [µc ] = “Describe the city Paris”. Assume, CallGPT-4o (π [µc ] ) = {“capital of France”, “cultural center”}, and ParseGPT-4o (“capital of France”) = {(t1 )} ParseGPT-4o (“cultural center”) = {(t2 )}.

If µ1 ̸∼ µ2 , the union µ1 ⊎ µ2 is undefined. By slight abuse of notation, for a graph pattern P and mapping µ, we write µ(P) for the set of triples obtained by substituting the variables var(P) in P according to µ.

By the semantics of generative patterns,  {µ } JgKG c = µc ⊎ {?y 7→ (t1 , gen)},

BGP evaluation. Let P be a BGP and G an RDF graph . The evaluation of P over G is the set,

Filter . Let µ be a typed solution mapping. The truth value of a filter formula F under µ, denoted F µ ∈ {⊤, ⊥, ε} (where ε denotes an error), is defined inductively as follows.

JPKG = { µ | domµ = var(P) ∧ µ(P) ⊆ G },

where each binding µ(v) = (t, rdf) with t ∈ T .

µc ⊎ {?y 7→ (t2 , gen)} .

µ

1. bound(v) otherwise.

µ

= ⊤ if v ∈ domµ , and bound(v)

= ⊥

2. For c ∈ T , (v = c)µ = ε if v ∈ / domµ ; (v = c)µ = ⊤ if µ(v) = (c, rdf) or Compatv (µ(v), (c, rdf)) = ⊤; otherwise, (v = c)µ = ⊥. 3. (v = v ′ )µ = ε if {v, v ′ } ⊈ domµ ; (v = v ′ )µ = ⊤ if µ(v) = µ(v ′ ) = (t, rdf) for some t ∈ T , or if Compatv (µ(v), µ(v ′ )) = ⊤; otherwise, (v = v ′ )µ = ⊥. 4. (¬F)µ = ⊤ if F µ = ⊥; (¬F )µ = ⊥ if F µ = ⊤; (¬F)µ = ε if F µ = ε. 5. (F1 ∧ F2 )µ = F1 µ ∧ F2 µ .

4.1

Dependency Graph

Let P be a generative SPARQL graph pattern and let gen(P) = {g | g ⪯ P and g is a GenOp occurrence} denote the set of GenOp occurrences in P. For each g = GenOp(π(X), Y, M) in gen(P), let input(g) denote its set of placeholder variables X and out(g) its set of output variables Y . Definition 11 (Dependency graph). The dependency graph → − of P is the directed graph D P = (gen(P), →P ), where for gi , gj ∈ gen(P), gi →P gj

Graph Patterns. The evaluation of a graph pattern P over S an RDF graph G, denoted JPKG , returns a set of typed solution mappings and is defined recursively below relative to a context supply S. When the context supply is fixed or imS material, we write JPKG as shorthand for JPKG . The clauses below define a single-pass (one-step) evaluation; cyclic generative dependencies are handled by the fixpoint semantics in Section 4. 1. If P is a BGP, then JPKG is defined as above. If P is a S GenOp pattern, its single-pass evaluation is JPKG , where S provides the solution mappings used to instantiate the placeholder variables of its prompt template. 2. JFilter F (P)KG = {µ ∈ JPKG | F µ = ⊤}; 3. JProj L (P)KG = {µ|L | µ ∈ JPKG };

4.

JP1 Join P2 KG = {µ1 ⊎ µ2 | µ1 ∈ JP1 KG , µ2 ∈ JP2 KG , µ1 ∼ µ2 };

5. JP1 Union P2 KG = JP1 KG ∪ JP2 KG ; 6.

JP1 Diff F P2 KG = {µ1 ∈ JP1 KG | ∀µ2 ∈ JP2 KG : ; µ1 ̸∼ µ2 or F µ1 ⊎µ2 = ⊥}

7. JP1 Opt F P2 KG = JP1 Join P2 KG ∪ JP1 Diff F P2 KG ; 8.

JP1 Minus P2 KG = {µ1 ∈ JP1 KG | ∀µ2 ∈ JP2 KG :

either µ1 ̸∼ µ2 or domµ1 ∩ domµ2 = ∅};

where µ|L is the restriction of µ to L. If g ⪯ P, the context supply for g in a single evaluation step is the set S = JP \ {g}KG . Proposition 1. Let P be a well-formed graph pattern that contains no occurrence of GenOp. Then, for any RDF graph G, the evaluation of P under the extended semantics coincides with standard SPARQL evaluation under set semantics: JPKG = JPKG |standard SPARQL .

4

Fragments and Fixpoint Semantics

The preceding semantics characterize the meaning of generative SPARQL queries independently of any evaluation strategy. Section 6 presents an executable realization of these semantics under bounded generation.

iff

out(gi ) ∩ input(gj ) ̸= ∅.

Definition 12. A nonempty subset C ⊆ gen(P) is a strongly connected component (SCC) of P iff: 1. for all g, g ′ ∈ C, there exists a finite sequence g = g0 , . . . , gk = g ′ in C such that gi →P gi+1 for all i < k, and a sequence from g ′ to g; and 2. C is maximal w.r.t. set inclusion under this property. The SCCs of P form a partition of gen(P). Definition 13 (Acyclicity). A graph pattern P is acyclic iff → − D P is acyclic. If P is acyclic, all GenOp occurrences can be evaluated in → − a single pass following a topological order of D P , and the result coincides with the fixpoint semantics induced by ΦP (Cf. Section 4.3). Definition 14. (Signed Dependency Edge) Let gi →P gj be a dependency edge and let Vij = out(gi )∩input(gj ). Let gj ⪯ P. We classify the edge by the syntactic occurrences of variable v ∈ Vij in the surrounding pattern P \ {gj }. 1. The edge is positive if every syntactic occurrence of every v ∈ Vij in P \ {gj } is in a positive position, namely under only the operators Join, Union, Proj, the Join branch of Opt or within a Filter where v does not occur under ¬. 2. The edge is negative if there exists some v ∈ Vij that has a syntactic occurrence in P \ {gj } in a negative position, i.e., within the scope of Minus, Diff, the Diff branch of Opt or under ¬ in a Filter. Example 3. Let g1 and g2 be the two GenOp occurrences in SELECT ?x ?y ?z WHERE { ?x a :City . GenOp("Find topic for ?x" AS ?y, GPT-4o). GenOp("Find city for ?y" AS ?z, GPT-4o). } The variable ?y occurs as a placeholder in the prompt of g2 and only in positive positions in the surrounding pattern of g2 ; hence g1 → g2 is a positive dependency. In the variant obtained by adding MINUS { ?x :hasTopic ?y . } the variable ?y occurs under a negative operator in the surrounding pattern of g2 . Thus, g1 → g2 is a negative dependency, and any stratification as in Definition 15 must satisfy σ(g1 ) < σ(g2 ).

Definition 15. A stratification of P is a function σ : gen(P) → N such that for every gi →P gj : (i) if the edge is positive then σ(gi ) ≤ σ(gj ); (ii) if the edge is negative then σ(gi ) < σ(gj ). The pattern P is stratified if such a function exists. Acyclic patterns admit single-pass evaluation. Stratified patterns admit stratum-wise fixpoint semantics. Nonstratified patterns require well-founded semantics.

4.2

Consequence Operator

S|g = {µ ∈ S | input(g) ⊆ domµ }, S|

and the evaluation of g relative to S is then JgKG g .

Definition 16. The immediate consequence operator of P is the function S

ΦP : 2ΩP → 2ΩP , ΦP (S) := JPKG . The ΦP (S) evaluates the query once while allowing each GenOp to draw its placeholder bindings from the current supply S. Recursive behavior is captured by iterating ΦP to a fixpoint. ′

Proposition 2. If S, S ⊆ ΩP satisfy S|g = S |g for every GenOp pattern g in P, then ΦP (S) = ΦP (S ′ ).

4.3

S0 = ∅,

Sn+1 = ΦP (Sn ). S The least fixpoint of ΦP is lfp(ΦP ) = n≥0 Sn , and the lfp

We handle recursion among GenOp patterns via an immediate consequence operator, assuming bounded generation so that, for fixed P and G, the set of generated terms, and thus relevant typed solution mappings, is finite. Let ΩP be the finite set of all typed solution mappings over var(P) whose values range over T ∪ Tgen . To expose recursive dependencies, evaluation is parameterized by a context supply S ⊆ ΩP . For a GenOp pattern g, only those mappings in S that provide bindings for all placeholders input(g) are useful to instantiate the prompt, i.e., context set,

′

If ΦP is monotone, it admits a least fixpoint with respect to set inclusion. Under the bounded-generation assumption, this fixpoint can be computed by iterating ΦP from the empty set. Definition 17 (Least fixpoint semantics). Let ΦP be monotone, and the ascending sequence {Sn }n≥0 is defined by

Monotonicity and Least Fixpoint Semantics

We identify conditions for a least-fixpoint semantics by establishing monotonicity of the consequence operator. A generative SPARQL pattern P is monotone w.r.t. the context supply if, for every GenOp g ⪯ P, variables in out(g) occur only in positive positions in P, so added generated bindings cannot invalidate existing solution mappings. Lemma 1. If P is monotone with respect to the context supply, then the consequence operator ΦP is monotone on the complete lattice (2ΩP , ⊆): ∀S, S ′ ∈ 2ΩP : S ⊆ S ′ −→ ΦP (S) ⊆ ΦP (S ′ ). Proof. Expanding the context supply S only increases the set of mappings available to instantiate placeholders of GenOp patterns. Since each GenOp is defined as a union over all admissible contexts, additional contexts can only yield additional generated mappings. By the monotonicity condition, variables introduced by GenOp patterns occur only in positive positions. Hence, previously derived mappings cannot be invalidated, and ΦP is monotone.

meaning of P under least-fixpoint semantics is JPKG := lfp(ΦP ). Theorem 1. (Existence and characterization) If ΦP is monotone on (2ΩP , ⊆), then it has a least fixpoint, and [ lfp(ΦP ) = ΦnP (∅). n≥0

Moreover, if ΩP is finite, the sequence stabilizes after at most |ΩP | iterations. For acyclic patterns, the iteration stabilizes after one step (see B.1), and the fixpoint semantics coincides with standard compositional evaluation. Theorem 2. Let S ∗ = lfp(ΦP ). If S is any set of typed solution mappings such that ΦP (S) ⊆ S, then S ∗ ⊆ S. Thus, S ∗ is the minimal fixpoint model of P.

4.4

Stratified Semantics

Let P be a generative SPARQL pattern and let σ : gen(P) → N be a stratification. For i ∈ N, let Gen≤i (P) = {g ∈ gen(P) | σ(g) ≤ i}. Let P ≤i denote the pattern obtained from P by disabling all GenOp occurrences not in Gen≤i (P), that is, replacing each such occurrence by a pattern whose evaluation is empty for all context supply S, while leaving the remaining algebraic structure unchanged. Definition 18. (Stratum-wise operator) For each i, let S ΦP ≤i : 2ΩP → 2ΩP defined by ΦP ≤i (S) := JP ≤i KG . Definition 19. (Stratified semantics) Let P be stratified with stratification σ : gen(P) → N. Let S−1 := ∅. For each stratum index i = 0, 1, 2, . . . , consider the operator S 7→ ΦP ≤i (S ∪ Si−1 ), and let Si be its least fixpoint:
Si := lfp S 7→ ΦP ≤i (S ∪ Si−1 ) . Let m = max{σ(g) | g ∈ gen(P)}, with m = 0 if gen(P) = ∅. The meaning of P under stratified semanstrat tics is given by JPKG = Sm . Theorem 3. If P is stratified and ΩP is finite (bounded strat is wellgeneration), then the stratified semantics JPKG defined and unique. Theorem 4. Let P be stratified. For each stratum i, the least fixpoint Si is independent of the order in which GenOp occurrences in stratum i are evaluated.

4.5

Well-Founded Semantics for Non-Stratified Patterns

For query patterns that are not stratified, we adopt the standard three-valued semantics based on an alternating fixpoint construction (Przymusinski 1990; Van Gelder 1989), instantiated to typed solution mappings. Let Cand(P) ⊆ ΩP be a finite candidate set. assumed to be a sound over-approximation of all typed solution mappings that may arise during evaluation of P under bounded generation. A partial interpretation is a pair (I + , I − ) with I + , I − ⊆ Cand(P) and I + ∩ I − = ∅, where mappings in I + are true, mappings in I − are false, and all others are undefined. Definition 20. Let J ⊆ Cand(P). The reduct consequence operator ΦJP : 2Cand(P) → 2Cand(P) is defined as S

ΦJP (S) := JPKG , where all negative constructs (i.e., MINUS, DIFF, and negated filters) are evaluated with respect to the fixed set J. Under fixed J, the operator S 7→ ΦJP (S) is monotone, since all negative tests are evaluated against a constant context. Definition 21 (Alternating fixpoint (I0+ , I0− ) := (∅, ∅). For n ≥ 0,

sequence).

patterns remain valid: P1 Join P2 ≡ P2 Join P1 ; (P1 Join P2 ) Join P3 ≡ P1 Join (P2 Join P3 ); P1 Join (P2 Union P3 ) ≡ (P1 Join P2 ) Union (P1 Join P3 ); Filter F1 ∧F2 (P ) ≡ Filter F1 (Filter F2 (P )); Filter F (P1 Join P2 ) ≡ Filter F (P1 ) Join P2 if var(F ) ⊆ var(P1 ); and P1 Minus P2 ≡ P1 if var(P1 ) ∩ var(P2 ) = ∅. The proofs follow those of SPARQL, with equality on shared variables replaced by compatibility (cf. Appendix C). GenOp-specific rewrites. A generative pattern g = GenOp(π(X), Y, M) can be evaluated only using context mappings that bind X; moving g can therefore change the context set and the result. We first illustrate why unrestricted reordering of GenOp patterns is unsound. Example 4 (Unsafe GenOp reordering). Let g GenOp(π({?x}), {?y}, M ) and consider P1 = {(?s :p ?x)}, P2 = {(?s :q ?z)}.

Let

−
Cand(P)\In + := lfp S 7→ ΦP In+1 (S) ,

I+ − := Cand(P) \ lfp S 7→ ΦPn+1 (S) . In+1 Theorem 5. (Convergence and uniqueness) If Cand(P) is finite, then the alternating fixpoint sequence in Definition 21 stabilizes after finitely many steps at a pair (I + , I − ). The induced three-valued interpretation is unique and coincides with the well-founded model of P over G relative to Cand(P).

=

Assume G is such that JP1 KG ̸= ∅ and JP2 KG ̸= ∅, but no mapping in JP2 KG binds ?x. In (P1 Join P2 ) Join g, the left subpattern P1 Join P2 yields mappings binding ?x, so the context set for g is non-empty and g may produce bindings for ?y. In contrast, in P1 Join (P2 Join g), the left subpattern P2 yields no mapping binding ?x, hence the context set for g is empty and JP2 Join gKG = ∅. Thus, reordering a GenOp across joins is not semantics-preserving in general. We next give sufficient conditions guaranteeing that common rewrites involving GenOp patterns are sound.

Non-stratified generative SPARQL patterns, i.e., patterns with cyclic negative dependencies, fall outside the monotone fragment. Under the bounded-generation assumption, such patterns admit a three-valued well-founded semantics obtained by the standard alternating-fixpoint construction over the finite mapping lattice; the construction follows classical well-founded semantics.

Proposition 3. Let g = GenOp(π(∅), Y, M ) be a base{∅} S mode GenOp. Then, ∀ G, ∀ S : JgKG = JgKG .

5

Corollary 1. Let g = GenOp(π(∅), Y, M ) and Ωg = ∅ JgKG . Let P be a query pattern that contains no GenOp occurrences. Then, ∀ G, ∀ S, S ′ :

Algebraic Equivalences and Rewrite Rules

We prove equivalence results for the monotone or stratified fragments, where denotational and fixpoint semantics coincide.

Proof. By the base-mode convention, whenever input(g) = ∅ the evaluation of g ignores the supplied context and uses the fixed context set {∅}. Hence {∅} S JgKG = JgKG for all S.

S

S′

JP Join gKG = JP Join gKG = JP Join Ωg KG .

Definition 22. Two generative SPARQL patterns P and P ′ are equivalent, written P ≡ P ′ , if they produce the same set of solution mappings for every RDF graph G and every S S context-supply set S, i.e., JPKG = JP ′ KG .

Proposition 4. Let P1 , P2 be patterns and g a GenOp. For S all G, S and i ∈ {1, 2}, let Si := JPi KG and Si |g :=

SPARQL-specific equivalences. Standard SPARQL equivalences that preserve the context supplied to GenOp

JgKG1 g ∪ JgKG2 g , then J(P1 Union P2 ) Join gKG S J(P1 Join g) Union (P2 Join g)KG .

{µ ∈ Si | input(g) ⊆ domµ }. S |

S |

S | ∪S2 |g

If JgKG1 g

S

=

=

Proof. In (P1 Union P2 ) Join g, the GenOp g sees exactly the union of the solution mappings produced by the two branches, so its context is (S1 |g ∪ S2 |g ). By the separability assumption, evaluating g on this combined context produces precisely the union of the outputs obtained by evaluating g on each branch context separately. Joining these outputs back with their respective branch solutions, therefore, yields exactly the union of P1 Join g and P2 Join g. Proposition 5. Let g = GenOp(π(X), Y, M) and let F be a filter with var(F ) ⊆ X. Let P be a pattern with Y ∩ var(P) = ∅ and var(F ) ⊆ var(P). Then, JFilter F (P) Join gKG = JFilter F (P Join g)KG .

Proof. Let S = JPKG and S + = {µ ∈ S | F µ = ⊤}. In Filter F (P) Join g, the context supply for g is S + ; S in P Join g, it is S. By the GenOp clause, JgKG = S {µ} + µ∈S JgKG , hence the extensions generated from S are + exactly those generated from the S , contexts inside the run on S. Every generated mapping has the form µ ⊎ ν and does not change the truth value of F because var(F) ⊆ X and g only adds fresh bindings on Y (up to representative normalization). Thus, F µ = ⊤ iff F µ⊎ν = ⊤, so filtering after the join removes precisely the contributions from µ ∈ / S+, yielding the same result as filtering before. Example 5. Let g = GenOp(π({?x}), {?y}, M ), and suppose P1 binds ?x while P2 does not. Then: JP1 Join (P2 Join g)KG ̸= J(P1 Join P2 ) Join gKG

Proposition 6. (Safe Join Reordering ) Let g = GenOp(π(X), Y, M) and let P1 , P2 be patterns such that X ⊆ var(P1 ) and var(P2 ) ∩ X = ∅. Then, for all graph G and all context-supply set S, S

S

J(P1 Join P2 ) Join gKG = J(P1 Join g) Join P2 KG .

Topological evaluation orderings preserve semantics when the generative dependency graph is acyclic. Theorem 6. Let P be a pattern whose generative depen→ − dency graph D P is acyclic. Let γ1 and γ2 be two topological orders of gen(P). For each order, let Ωγ1 (resp. Ωγ2 ) be the set of typed solution mappings obtained by evaluating all GenOp occurrences according to that order, starting from the same non-generative base evaluation (cf. Appendix B.1). Then, Ωγ1 = Ωγ2 .

6

Executable Fixpoint Evaluation

Recursive evaluation is declaratively given by a fixpoint construction. With generative patterns, consequences depend on finite-valued external model calls. We therefore use candidate-model validation for executable fixpoint evaluation, following the treatment of external operators in logic programs (Eiter et al. 2006). Let P be a monotone query pattern with immediate consequence operator ΦP . Declaratively, the meaning of P is

lfp(ΦP ). Executable evaluation checks the self-support condition µ ∈ ΦP ({µ}) on finitely many candidates; soundness holds unconditionally, while completeness is relative to candidate coverage. Evaluation Roadmap. Query evaluation proceeds by invoking EvalSCC(G, P, C, η, K, B, T, R) (Algorithm 1) for each SCC C of P and each outer binding η. For a fixed call, EvalSCC first identifies the generated variables YC and required placeholders XC (Sect. 6.1), then uses bounded proposal (K, B) to enumerate a finite candidate set CandC (η) ⊆ ΩP (Sect. 6.2). Each candidate is subsequently checked for self-support by repeated validation (R), with optional bounded repairs (T ). The output RC (η) consists exactly of those candidates that satisfy self-support. A concrete execution trace is given in Appendix A.1.

6.1

SCC-local view and self-support

Recursion in generative SPARQL arises only through generative patterns. We therefore localize recursion using strongly connected components (SCCs). Let C be a SCC of the pattern P, i.e., C ⊆ gen(P). Let, [ [ YC = out(g) and XC = ( input(g)) \ YC . g∈C

g∈C

Here, YC are the variables generated within C, while XC are the external placeholders required by operators in C. An outer binding for C is a mapping η with XC ⊆ domη . Definition 23. Let C be an SCC of P. A mapping µ ∈ ΩP is self-supporting for C (denoted SSC (µ)) if XC ⊆ dom( µ) and for every generative pattern g = GenOp(π(X), Y, M) ∈ C, {µ

}

µ ∈ JgKG |X . The SSC (µ) requires that each GenOp in the SCC reproduces the bindings already present in µ when evaluated on the placeholder bindings induced by µ itself. This condition replaces incremental rule firing as the operational criterion for recursive admissibility.

6.2

Executable Interface

We separate executable evaluation into proposal, which heuristically enumerates a finite search space, and validation, which enforces semantic correctness. 1. Validation Oracle. For a generative pattern g = GenOp(π(X), Y, M) and a total placeholder binding θ over X, we assume a Boolean procedure Validate(g, θ, ν; R) ∈ {⊤, ⊥} that returns ⊤ iff, under fixed decoding, parsing, and normalization settings repeated R times, the extension {θ} (θ⊎ν) belongs to JgKG . Thus, Validate implements a bounded membership test for the denotation of g on fully instantiated prompts. 2. Proposal Routine. Propose(g, θ, K) returns up to K candidate bindings ν for variables in out(g) ∩ YC under

placeholder binding θ. Proposal may be invoked on partially instantiated contexts by filling missing placeholders with fixed sentinel tokens (or by fill in the blanks (Donahue, Lee, and Liang 2020)); sentinels serve only to diversify candidate enumeration and have no semantic status. Only fully instantiated bindings are validated. 3. Candidate sets and executable SCC answers. Let C be an SCC and an η outer binding. For each v ∈ YC , maintain a finite domain D[v] ⊆ Tgen × {gen} with |D[v]| ≤ B. These domains induce a finite candidate set Cand C (η) = {η ⊎ ν | ν : YC → Tgen × {gen}, o ∀v ∈ YC : ν(v) ∈ D[v], η ∼ ν . By construction, Cand C (η) ⊆ ΩP ((typed solution mappings)). The candidate set is an operational search space and is not defined in terms of the consequence operator ΦC ; it may therefore contain mappings that are not semantically admissible. The outer binding η can be viewed as a singleton context supply {η} ⊆ ΩP , consistent with the general evaluation semantics. Restriction of context supplies to placeholders (notation S|g ) is not used during candidate construction, since no generative operators are semantically evaluated at that stage. Such restrictions arise only during validation, where each candidate µ induces the placeholder binding µ|X used to check mem{µ

}

bership µ ∈ JgKG |X . Give a finite candidate set Cand C (η), let RC (η) = {µ|YC | µ ∈ Cand C (η) ∧ SSC (µ)}, Thus, executable evaluation RC (η) returns exactly the YC -projections of candidates that satisfy self-support. Finite candidate coverage and exactness assumption . For every SCC C of the generative-dependency graph and every outer binding η, the proposal step yields a finite candidate set Cand C (η). For the chosen semantics Sem ∈ {lfp, stratified, well-founded}, the accepted projections RC (η) are exactly the declarative answer projections for C under η. All generated terms, parsed tuples, candidates, and validation inputs have polynomial-size representations.

6.3

Algorithm EvalSCC

Algorithm 1 constructs finite domains D[·] by proposal, forms Cand C (η), and filters it by self-support validation. All semantic checks occur only during validation, on fully instantiated mappings. Guarantees. For any finite candidate set Cand C (η), Algorithm 1 returns exactly the candidate projections that pass the local self-support validation. Thus, the algorithm is exact on the chosen candidate set, sound relative to the selfsupport target, and complete when the candidate set covers all self-supporting extensions of η. Under the finite candidate coverage and exactness assumption above, this target

Algorithm 1 EvalSCC(G, P, C, η, K, B, T, R) Require: RDF graph G; pattern P; SCC C; outer binding η with XC ⊆ dom( η); bounds K (proposals), B (domain cap), T (repairs), R (validation repetitions). Ensure: RC (η) = {µ|YC | µ ∈ Cand C (η) ∧ SSC (µ)}. 1: Candidate enumeration (heuristic). 2: Initialize D[v] ← ∅ for all v ∈ YC . 3: while not saturated and ∃v ∈ YC : |D[v]| < B do 4: for all g = GenOp(π(Xg ), Yg , M) ∈ C do 5: Construct a possibly partial context θ extending η; fill any missing placeholders in Xg with fixed sentinel tokens. 6: A ← Propose(g, θ, K). 7: for all (v, a) ∈ A with v ∈ Yg ∩ YC do 8: if |D[v]| < B then 9: D[v] ← D[v] ∪ {a}. 10: end if 11: end for 12: end for 13: end while 14: Candidate construction. 15: Form Cand C (η) from D[·] as complete mappings extending η (optional symbolic pruning). 16: Backtracking search with validation. 17: RC (η) ← ∅. 18: for all complete candidates µ ∈ Cand C (η) do 19: Self-support validation: 20: if for every g = GenOp(π(Xg ), Yg , M) ∈ C, with νg := µ|Yg , we have dom( νg ) = Yg , µ|Xg ∪Yg = µ|Xg ⊎νg , and Validate(g, µ|Xg , νg ; R) = ⊤ then 21: RC (η) ← RC (η) ∪ {µ|YC }. 22: else 23: Optionally attempt up to T repairs by resampling values for a failing variable via Propose and revalidating. 24: end if 25: end for 26: return RC (η)

coincides with the declarative answer projections for C under η. For fixed bounds (K, B, T, R), the algorithm terminates; see Appendix D.

6.4

Evaluation via SCC-condensation

Each SCC C can be summarized as a derived macro-operator GenSCCC : XC −→ YC with denotation S

JGenSCCC KG = {η ⊎ ρ | η ∈ S, XC ⊆ dom( η),

ρ ∈ RC (η), η ∼ ρ}.

where RC (η) is computed by Algorithm 1. Replacing each SCC of P by its macro-operator yields an acyclic generative dependency graph, and the resulting condensed pattern can be evaluated in topological order, where each SCC is executed by EvalSCC for each outer binding produced upstream. This condensation is semantics-preserving for the monotone fragment.

7

Computational Complexity

We analyze the complexity of query evaluation under the semantics of Sections 3 and 4. We abstract from the internal cost of model inference and treat each GenOp as an external oracle, considering only symbolic query evaluation. We assume the deterministic bounded-generation, finitecandidate-coverage, and exactness conditions, and abstract from oracle-call and parsing costs, treating them as O(1) per invocation. The computational task is evaluation membership: given a graph pattern P, an RDF graph G, a typed solution mapping µ, and the applicable semantics (acyclic, stratified, or well-founded), decide whether µ belongs to the semantic value of P over G, i.e., whether µ ∈ JPKG . Theorem 7. Under deterministic bounded generation and the finite candidate coverage and exactness conditions, the evaluation-membership problem satisfies the following bounds:

1. Acyclic patterns are in PTIME in data complexity and PSPACE-complete in combined complexity. 2. Stratified patterns and non-stratified patterns under wellfounded semantics are also in PTIME in data complexity and PSPACE-complete in combined complexity. In generative SPARQL, recursion neither derives new RDF facts nor expands the data domain. Both acyclic and recursive patterns are evaluated over the same finite set of solution mappings, determined by the query and bounded generation. Recursion thus serves to validate self-support among already enumerable candidates, rather than to derive RDF facts or chase witnesses as in existential-rule systems. As a result, stratified or well-founded recursion affects only the admissibility of mappings, not the size of the search space, producing the same asymptotic complexity as acyclic evaluation. Dropping bounded-generation assumptions eliminates termination guarantees for fixpoint evaluation; in this case, generative patterns can simulate existential-rule application and chase-style reasoning, leading to undecidability (Abiteboul, Hull, and Vianu 1995; Calı̀, Gottlob, and Pieris 2010, Chapter 13).

8

Conclusions and Future Work

We presented a conservative, declarative extension of SPARQL with a generative pattern, GenOp. The proposed query semantics accommodates acyclic, stratified, and nonstratified generative dependencies via consequence operators and fixpoint constructions. Under a bounded-generation assumption, the extension preserves the established complexity bounds of SPARQL (Pérez, Arenas, and Gutierrez 2009). The only form of recursion supported arises from dataflow dependencies among generative patterns, where the outputs of one GenOp parameterize the prompt of another. This recursion operates at the level of prompt instantiation rather than fact derivation, and no generated value becomes part of the RDF graph under query. As a result, the language extends SPARQL with controlled generative dependencies while preserving its declarative and computational properties (Arenas, Gutierrez, and Pérez 2009) and remaining

fundamentally different from Datalog-style rule languages (Calı̀, Gottlob, and Pieris 2010; Gottlob, Lukasiewicz, and Pieris 2014; Calı̀ et al. 2010) in terms of both expressiveness and complexity. Future work includes relaxing bounded-generation assumptions, as well as incorporating Datalog-style existential predicate into GenOp patterns, and characterizing decidable fragments under guardedness or acyclicity conditions, following the methods for existential rules (Deutsch, Nash, and Remmel 2008; Gottlob, Morak, and Pieris 2015; Calautti, Gottlob, and Pieris 2015), and developing optimizer support for generative operators within the SPARQL algebra. Acknowledgments. This work is funded by the German Research Foundation (DFG) – SFB 1574 Circular Factory– 471687386.

References Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of databases, volume 8. Addison-Wesley Reading. Arenas, M., and Pérez, J. 2011. Querying semantic web data with SPARQL. In Proceedings of the thirtieth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, 305–316. Arenas, M.; Gutierrez, C.; and Pérez, J. 2009. Foundations of RDF databases. In Reasoning Web International Summer School. Springer. 158–204. Calautti, M.; Gottlob, G.; and Pieris, A. 2015. Chase termination for guarded existential rules. In Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 91–103. Calı̀, A.; Gottlob, G.; Lukasiewicz, T.; Marnette, B.; and Pieris, A. 2010. Datalog+/-: A family of logical knowledge representation and query languages for new applications. In 2010 25th annual IEEE symposium on logic in computer science, 228–242. IEEE. Calı̀, A.; Gottlob, G.; and Pieris, A. 2010. Query answering under non-guarded rules in Datalog+/-. In International Conference on Web Reasoning and Rule Systems, 1–17. Springer. Chekol, M. W. 2016. On the containment of sparql queries under entailment regimes. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 30. Codd, E. F. 1970. A relational model of data for large shared data banks. Communications of the ACM 13(6):377–387. Dai, H.; Wang, B.; Wan, X.; Dai, B.; Yang, S.; Nova, A.; Yin, P.; Phothilimthana, M.; Sutton, C.; and Schuurmans, D. 2024. UQE: A query engine for unstructured databases. Advances in Neural Information Processing Systems 37:29807–29838. Deutsch, A.; Nash, A.; and Remmel, J. 2008. The chase revisited. In Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, 149–158.

Donahue, C.; Lee, M.; and Liang, P. 2020. Enabling language models to fill in the blanks. https://arxiv.org/abs/2005. 05339. Eiter, T.; Ianni, G.; Schindlauer, R.; and Tompits, H. 2006. Effective integration of declarative rules with external evaluations for semantic-web reasoning. In European Semantic Web Conference, 273–287. Springer. Ferrada, S.; Bustos, B.; and Hogan, A. 2024. Similarity joins and clustering for SPARQL. Semantic Web 15(5):1701–1732. Florescu, D.; Levy, A.; and Mendelzon, A. 1998. Database techniques for the World-Wide Web: A survey. ACM Sigmod Record 27(3):59–74. Gottlob, G.; Lukasiewicz, T.; and Pieris, A. 2014. Datalog+/-: questions and answers. In KR. Gottlob, G.; Morak, M.; and Pieris, A. 2015. Recent advances in Datalog. Reasoning Web International Summer School 193–217. Green, T. J.; Huang, S. S.; Loo, B. T.; Zhou, W.; et al. 2013. Datalog and recursive query processing. Foundations and Trends® in Databases 5(2):105–195. Hartig, O., and Pérez, J. 2016. LDQL: A query language for the web of linked data. Journal of Web Semantics 41:9–29. Hartig, O.; Bizer, C.; and Freytag, J.-C. 2009. Executing SPARQL queries over the web of linked data. In International semantic web conference, 293–309. Springer. Hartig, O. 2013. SQUIN: a traversal based query execution system for the web of linked data. In Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data, 1081–1084. Hernández, I.; Rivero, C. R.; and Ruiz, D. 2019. Deep web crawling: a survey. World Wide Web 22(4):1577–1610. Hogan, A.; Blomqvist, E.; Cochez, M.; d’Amato, C.; Melo, G. D.; Gutierrez, C.; Kirrane, S.; Gayo, J. E. L.; Navigli, R.; Neumaier, S.; et al. 2021. Knowledge graphs. ACM Computing Surveys (Csur) 54(4):1–37. Kaminski, M.; Kostylev, E. V.; and Grau, B. C. 2017. Query nesting, assignment, and aggregation in SPARQL 1.1. ACM Transactions on Database Systems (TODS) 42(3):1–46. Khabiri, E.; Kephart, J. O.; Iii, F. F. H.; Jayaraman, S.; Li, Y.; Tipu, F. A.; Shah, D.; Fokoue-Nkoutche, A.; and Bhamidipaty, A. 2025. Declarative techniques for NL queries over heterogeneous data. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: Industry Track, 1744–1761. Kiefer, C.; Bernstein, A.; and Stocker, M. 2007. The fundamentals of iSPARQL: A virtual triple approach for similarity-based semantic web tasks. In International Semantic Web Conference, 295–309. Springer. Kontchakov, R., and Kostylev, E. V. 2016. On expressibility of non-monotone operators in SPARQL. In KR, 369–379. Manola, F.; Miller, E.; McBride, B.; et al. 2004. RDF primer. W3C recommendation 10(1-107):6. Molli, P.; Skaf-Molli, H.; Ferré, S.; Gaignard, A.; and Cellier, P. 2025. SparqLLM: Retrieval-augmented SPARQL

query processing. In European Semantic Web Conference, 103–107. Springer. Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of mathematics and Artificial Intelligence 25(3):241–273. Park, K.; Zhou, T.; and D’Antoni, L. 2025. Flexible and efficient grammar-constrained decoding. https://arxiv.org/abs/ 2502.05111. Pérez, J.; Arenas, M.; and Gutierrez, C. 2006. Semantics and complexity of SPARQL. In International semantic web conference, 30–43. Springer. Pérez, J.; Arenas, M.; and Gutierrez, C. 2009. Semantics and complexity of SPARQL. ACM Transactions on Database Systems (TODS) 34(3):1–45. Prud’hommeaux, E., and Seaborne, A. 2008. SPARQL query language for RDF. W3C recommendation, january 15, 2008. ”https:// www.w3.org/ TR/ rdf-sparql-query/ ”. Przymusinski, T. 1990. Well-founded semantics coincides with three-valued stable semantics. Fundamenta informaticae 13(4):445–463. Saeed, M.; De Cao, N.; and Papotti, P. 2024. Querying large language models with SQL. In EDBT. Schmidt, M.; Meier, M.; and Lausen, G. 2010. Foundations of SPARQL query optimization. In Proceedings of the 13th international conference on database theory, 4–33. Tan, J.; Zhao, K.; Li, R.; Yu, J. X.; Piao, C.; Cheng, H.; Meng, H.; Zhao, D.; and Rong, Y. 2025. Can large language models be query optimizer for relational databases? Proceedings of the ACM on Management of Data 3(6):1–28. Ullman, J. D. 1988. Principles of Computer and Knowledgebase Systems. Computer Science Press. Umbrich, J.; Hogan, A.; Polleres, A.; and Decker, S. 2015. Link traversal querying for a diverse web of data. Semantic Web 6(6):585–624. Van Gelder, A. 1989. The alternating fixpoint of logic programs with negation. In Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, 1–10. Yang, W.; Some, L.; Bain, M.; and Kang, B. 2025. A comprehensive survey on integrating large language models with knowledge-based methods. Knowledge-Based Systems 113503. Zhao, F.; Agrawal, D.; and Abbadi, A. E. 2024. Hybrid querying over relational databases and large language models. Zheng, W.; Zou, L.; Peng, W.; Yan, X.; Song, S.; and Zhao, D. 2016. Semantic SPARQL similarity search over RDF knowledge graphs. Proceedings of the VLDB Endowment 9(11):840–851.

Extended Proofs and Auxiliary Results A Sample run of Example 1 Below, we illustrate the executable treatment of mutually dependent GenOp occurrences. The run constructs a candidate mapping and checks whether it is locally self-supporting. Correctness with respect to the declarative component answers is relative to the finite candidate coverage and exactness assumption from Sect. 6. Example 6. Let G = {:Paris a :City} and consider the query Q = (BGP Join g1 ) Join g2 , where • BGP = {?x a :City}, • g1 = GenOp(π1 ({?x, ?z}), {?y}, GPT-4o) with π1 ({?x, ?z}) = “Suggest a topic related to ?x and ?z”, and • g2 = GenOp(π2 ({?y}), {?z}, Gemini 1.5 Pro) with π2 ({?y}) = “Suggest a city related to topic ?y”. Evaluating the basic graph pattern gives S (0) = J{?x a :City}KG = {µ0 },

µ0 = {?x 7→ (:Paris, rdf)}.

Neither g1 nor g2 is applicable to µ0 in a single pass: g1 requires a binding for ?z, while g2 requires a binding for ?y. Thus, the dependency graph of Q contains a cycle between g1 and g2 . Executable evaluation handles this cycle by considering finite candidate extensions of µ0 and validating them against the two local generative conditions. We now exhibit one candidate mapping and the validation witnesses for it. Hypothesized binding and instantiation of g2 . Assume that a candidate mapping µ∗ binds ?y to the generated term (tA , gen) with Lex(tA ) = “art”. Instantiating π2 with the input projection of µ∗ gives [µ∗

]

π2 |{?y} = “Suggest a city related to topic art”. Assume [µ∗

]

CallGemini 1.5 Pro (π2 |{?y} ) = {“Florence”}, and that ParseGemini 1.5 Pro (“Florence”) = {(tF )}, Lex(tF ) = “Florence”, This validates the generated binding {?z 7→ (tF , gen)} for g2 under the input binding ?y 7→ (tA , gen). Instantiation of g1 . Given the bindings for ?x and ?z, instantiating π1 gives [µ∗

]

π1 |{?x,?z} = “Suggest a topic related to Paris and Florence”.

Assume [µ∗

]

CallGPT-4o (π1 |{?x,?z} ) = {“art”}, and ParseGPT-4o (“art”) = {(tA )},

Lex(tA ) = “art”.

This validates the generated binding {?y 7→ (tA , gen)} for g1 under the input bindings ?x 7→ (:Paris, rdf) and ?z 7→ (tF , gen). Let, µ∗ = {?x 7→ (:Paris, rdf), ?y 7→ (tA , gen), ?z 7→ (tF , gen)}. Self-support validation. The mapping µ∗ extends µ0 and binds the input and output variables of both generative occurrences. For g1 , the projection µ∗|{?x,?z} instantiates the prompt, and the projection µ∗|{?y} is validated as an admissible output. For g2 , the projection µ∗|{?y} instantiates the prompt, and the projection µ∗|{?z} is validated as an admissible output. Hence µ∗ passes the local self-support test for the component {g1 , g2 }. If µ∗ belongs to the finite candidate set considered by the executable evaluator, then the evaluator accepts the projection µ∗|{?y,?z} . Under the finite candidate coverage and exactness assumption from Sect. 6, this accepted projection coincides with a declarative component-answer projection. The resulting full query answer is {?x 7→ (:Paris, rdf), ?y 7→ (tA , gen), ?z 7→ (tF , gen)}. The generated bindings ?y and ?z are typed with gen and they do not add RDF triples to G.

A.1

Executable Fixpoint Evaluation of Example 1

We now demonstrate executable fixpoint evaluation by bounded candidate enumeration followed by local selfsupport validation. We illustrate the executable procedure from Sect. 6 on Example 1, making explicit (i) how Propose induces a finite candidate set and (ii) how validation checks candidate mappings on fully instantiated prompts. We separate candidate discovery from candidate validation: Propose determines which candidates are explored, while validation determines which explored candidates are accepted. Correctness with respect to the declarative component answers is relative to the finite candidate coverage and exactness assumption from Sect. 6. Recall Example 1, SELECT ?x ?y ?z WHERE { ?x a :City . GenOp("Suggest a topic related to ?x and ?z" AS ?y, GPT-4o). GenOp("Suggest a city related to topic ?y" AS ?z, Gemini 1.5 Pro). }

Let G = {:Paris a :City}. Let g1 = GenOp(π1 ({?x, ?z}), {?y}, M1 ), g2 = GenOp(π2 ({?y}), {?z}, M2 ), where • π1 is the template "Suggest a topic related to ?x and ?z"; and • π2 is "Suggest a city related to topic ?y". We assume canonical lexicalization for RDF terms, e.g., Canon(:Paris) = “Paris”, and that generated terms t ∈ Tgen carry lexicalizations Lex(t) ∈ Σ∗ . Assume the following operational bounds and decodingformat conventions. 1. Proposal bound K (i.e., maximum proposals per Propose call) and domain cap B (i.e., maximum pervariable domain size). Here, K bounds the number of distinct values returned by a single proposal call, while B bounds the total number of values accumulated for each generated variable across proposal calls. Together, K and B make the explored candidate domains finite. Values not proposed because of these bounds are not explored operationally; they are part of the declarative semantics only when covered by the finite candidate coverage assumption. 2. Validation repetitions R and optional repair attempts T . Validation uses a binary membership-style query to the model. The parameter R bounds repeated validation calls used by an implementation to stabilize the acceptance decision. If validation fails, T bounds the number of local repair attempts in which an alternative generated value is substituted and revalidated. These parameters affect the executable procedure and runtime; the declarative semantics is fixed independently of them. 3. The model response must be parseable as JSON, which can be enforced by grammar-constrained decoding for LLMs (Park, Zhou, and D’Antoni 2025). For g1 (output variable ?y), we use the schema {"y":

["<string>", ...]},

and for g2 (output variable ?z), we use {"z":

["<string>", ...]}.

4. Decoding parameters, such as temperature, top-p, and maximum number of tokens, are fixed per model and treated as part of the implementation. Parsing maps each output string s to a fresh generated term ts ∈ Tgen with Lex(ts ) = s, or reuses an existing ts if already created. Propose and Self-validation Procedures We instantiate the abstract semantics with two concrete operational procedures. (A) Propose as bounded enumeration. Given g = GenOp(π(X), Y, M), a context mapping S, and a bound K:

1. Prompt instantiation. Build a concrete prompt string π [S] by replacing placeholders in X ∩ dom( S) using lexicalization. If some placeholder in X is unbound in S, render it using a fixed sentinel token <unknown:?v>. 2. Model call. Query M under fixed decoding parameters with an instruction requiring JSON output and at most K items. 3. Parse and deduplicate. Parse the JSON, extract up to K distinct strings, and map them to generated terms deterministically. 4. Return. Return the resulting set of at most K generatedterm tuples. In this example, all tuples are singletons because |Y | = 1. This procedure never claims completeness; it merely returns a bounded set of candidates. Finiteness is enforced by the explicit bound K and by the domain cap B applied when inserting into D[·]. (B) Self-support validation as membership checking. Given a complete candidate mapping µ and g = GenOp(π(X), Y, M), validation checks whether the tuple µ|Y is an admissible output for g under the fully instantiated prompt π [µ|X ] . We use a verification query, that is, a Boolean YES/NO query, rather than relying on exact re-generation: 1. Instantiate the base instruction prompt π [µ|X ] . 2. Form a verification prompt that includes the instruction and the candidate output tuple µ|Y , and asks for a strict YES/NO answer. 3. Query M under the fixed validation policy. Repeat R times if specified. 4. Accept if the aggregation policy for the R validation calls accepts the candidate. This gives an explicit implementation of the abstract membership test {µ

}

µ|X ⊎ µ|Y ∈ JgKG |X .

Memoization Maintain two caches: (i) a proposal cache keyed by (g, π [S] , K, decoding); and (ii) a validation cache keyed by (g, π [µ|X ] , µ|Y , R). Caches stabilize evaluation and reduce repeated model calls. 1. Step 1: Base RDF evaluation. Evaluating the basic graph pattern ?x a : City over G yields the unique typed solution mapping µ0 = {?x 7→ (:Paris, rdf)}. This is the outer binding η := µ0 . 2. Step 2: SCC identification and summarization. Since ?y feeds g2 and ?z feeds g1 , the dependency graph contains one SCC: C = {g1 , g2 }. The externally supplied variables are XC = {?x},

and the variables generated inside the component are YC = {?y, ?z}. We summarize C by the macro-operator GenSCCC . For an outer binding η, this operator returns full mappings of the form η ⊎ ρ, where ρ ranges over the accepted YC projections produced by the executable evaluation of C under η. Under the finite candidate coverage and exactness assumption from Sect. 6, these accepted projections coincide with the declarative component-answer projections. 3. Step 3: Candidate enumeration, operational only. We invoke E VAL SCC(G, P, C, η, K, B, T, R). Initialize finite domains: D[?y] = ∅

and

Cand(C) = {η ⊎ ν | ν(?y) ∈ D[?y], ν(?z) ∈ D[?z]}. Suppose, in this run, |D[?y]| = 2 and |D[?z]| = 2. Then, |Cand(C)| = 4. 4. Step 4: Candidate validation. We enumerate candidates µ ∈ Cand(C) and accept those that pass local selfsupport validation, that is, those for which each g ∈ C validates the output assigned by µ under the prompt instantiated from the input variables of g. Candidate sample. Consider

We call

S1 = {?x 7→ (:Paris, rdf)}. Since ?z ∈ / dom( S1 ), the sentinel policy instantiates [S ]

π1 1 = “Suggest a topic related to Paris and <unknown:?z>”. We query M1 with an instruction such as: Return JSON {"y":[...]} with at most K short topic strings.

Suppose the model returns: {"y":["Art","Cuisine"]}. Parsing yields generated terms tArt and tCuisine with Lex(tArt ) = “Art”,

Finite candidate set. The induced candidate set is the finite product:

µ = {?x 7→ (:Paris, rdf), ?y 7→ (tArt , gen), ?z 7→ (tFlorence , gen)}.

D[?z] = ∅.

Round 1: propose values for ?y. Propose(g1 , S1 , K) with

g2 until no new values are added or the cap B is reached. In all cases, |D[v]| ≤ B is enforced by construction.

Lex(tCuisine ) = “Cuisine”.

Update, respecting the cap B: D[?y] = {tArt , tCuisine }. Round 2: propose values for ?z conditional on ?y. Choose a currently discovered value, for example ?y = tArt , and call Propose(g2 , S2 , K) with S2 = {?x 7→ (:Paris, rdf), ?y 7→ (tArt , gen)}. Then, [S ]

π2 2 = “Suggest a city related to topic Art”. Query M2 requiring JSON {"z":[...]} with at most K city strings. Suppose it returns: {"z":["Florence","Rome"]}. Parsing yields tFlorence and tRome , and we update: D[?z] = {tFlorence , tRome }. Further rounds. One can repeat conditional proposals, for example for ?y = tCuisine , and alternate between g1 and

Validate g1 on µ (topic validation). We have X = {?x, ?z} and Y = {?y}. Instantiate the base instruction prompt using µ|X : [µ

]

π1 |X = “Suggest a topic related to Paris and Florence”. We then issue a verification query to M1 such as: Instruction: “Suggest a topic related to Paris and Florence.” Candidate topic: “Art”. Is the candidate a valid output for the instruction? Answer YES or NO only.

Repeat according to the validation bound R and accept if the validation aggregation policy accepts. If accepted, this operationally establishes that tArt is admissible for g1 under the input projection µ|X . Validate g2 on µ (city validation). We have X = {?y} and Y = {?z}. Instantiate: [µ

]

π2 |X = “Suggest a city related to topic Art”. Verification query to M2 : Instruction: “Suggest a city related to topic Art.” Candidate city: “Florence”. Is the candidate a valid output for the instruction? Answer YES or NO only.

Again, repeat according to the validation bound R and accept if the validation aggregation policy accepts. Acceptance. The candidate µ is accepted iff both validations pass. In that case, µ satisfies the local self-support condition for the component C. If either validation fails, µ is rejected. Optional repair. If µ fails due to, say, g2 , we may attempt up to T repairs: keep µ|X fixed for g2 , here ?y = Art, call Propose(g2 , {?y = Art}, K) or consult cached proposals, substitute an alternative ?z from the proposals, for example Rome, and rerun the same validation checks. Only mappings that pass the same local self-support validation are accepted.

5. Step 5: Final result. For each accepted candidate µ, the SCC yields µ|YC , and the full query answer is obtained by joining with the outer mapping µ0 , which is already included in µ. Thus, answers have the form {?x 7→ (:Paris, rdf), ?y 7→ (t, gen), ?z 7→ (u, gen)}. Remark 2. The mechanisms Propose, sentinel placeholders, decoding choices, JSON schemas, caching, and repair only control candidate discovery and execution cost. Acceptance of a candidate is determined by local self-support validation on fully instantiated prompts. Correctness with respect to the declarative component answers is obtained under the finite candidate coverage and exactness assumption from Sect. 6.

B

Fixpoint-Based Semantics

We assume a bounded-generation regime: for every GenOp occurrence g = GenOp(π(X), Y, M), every instantiated prompt string produces a finite set of textual answers via CallM , and every textual answer yields a finite set of parsed tuples via ParseM . The total set of typed solution mappings that may be produced during evaluation is finite. Formally, the induced universe ΩP (as defined in the main text) is finite. Set-theoretic lattice facts. For any set U , the powerset (2U , ⊆) is a complete lattice with least element ∅, greatest element U , and joins given by unions. If U is finite, every ascending chain in (2U , ⊆) stabilizes after at most |U | strict increases. Compatibility. We use the compatibility relation ∼ and union ⊎ of typed solution mappings as defined in the main text. We rely on the following basic fact: if µ1 ∼ µ2 , then µ1 ⊎ µ2 is well-defined and extends both µ1 and µ2 . Context restriction. For a context supply S ⊆ ΩP and a GenOp pattern g, we recall S|g = {µ ∈ S | input(g) ⊆ domµ }. For any S ⊆ S ′ , we always have S|g ⊆ S ′ |g . Immediate consequence operator. We use ΦP : 2ΩP → S 2ΩP given by ΦP (S) = JPKG (main text). Whenever we write ΦnP , this denotes n-fold composition, with Φ0P being the identity.

B.1

Acyclic patterns: single-pass evaluation coincides with fixpoint semantics

This subsection proves the theorem stated in the main text: acyclic dependency implies that the semantics can be computed in a single pass and matches the least-fixpoint semantics. Operational single-pass evaluation for acyclic patterns. → − Let D P = (gen(P), →P ) be the dependency graph. Let → − D be acyclic, and let γ = (g1 , . . . , gm ) be a topological order of the nodes gen(P). [k] For k ∈ {0, . . . , m}, let Pγ denote the pattern obtained from P by disabling every GenOp occurrence not among {g1 , . . . , gk }, i.e., replacing it by a pattern whose evaluation yields ∅, while leaving the remaining algebraic struc[0] ture unchanged. Thus, Pγ has all GenOps disabled and [m] Pγ = P.

The staged sets are: ∅

Sγ(0) := JPγ[0] KG ,

S (k−1)

Sγ(k) := JPγ[k] KGγ

(1 ≤ k ≤ m).

That is, at stage k, GenOp occurrences up to gk may fire using the context supply accumulated at stage (k − 1). Lemma 2. (Well-defined staged evaluation) For each k ∈ (k) {0, . . . , m}, the set Sγ is well-defined and contained in ΩP . Proof. By bounded generation, each GenOp call yields finitely many outputs, and every inductive evaluation clause returns a finite set of typed solution mappings. Since evaluation is defined for any supply S ⊆ ΩP (via S|g for GenOps), (k) each Sγ is defined. Containment in ΩP follows by construction. Lemma 3. (No backward dependencies) Let γ = (g1 , . . . , gm ) be topological. If i < j, then out(gj ) ∩ input(gi ) = ∅. Proof. If out(gj ) ∩ input(gi ) ̸= ∅, then by definition of →P we have gj →P gi , contradicting that γ is a topological order. Theorem 8 (Acyclic collapse: single-pass equals least fix→ − point). Assume D P is acyclic and fix a topological order γ. Then: (m)

1. Sγ

is a fixpoint of ΦP .

(m) Sγ equals the least fixpoint lfp(ΦP ).

2. 3. In particular, the result is independent of the chosen topological order. Proof. We proceed in steps. (m)

(1) Sγ

(m)

is a post-fixpoint. We show ΦP (Sγ

(m)

) ⊆ Sγ

.

Sγ(m)

(m) Let µ ∈ ΦP (Sγ ) = JPKG . In evaluating P relative (m) to Sγ , each GenOp occurrence gi draws its contexts from (m) Sγ |gi .

We claim that any placeholder-binding used for gi at stage m is already available at stage (i − 1). That is, (m) (i−1) for every η ∈ Sγ |gi there exists η ′ ∈ Sγ |gi with ′ η |input(gi ) = η|input(gi ) . Indeed, by Lemma 3, the variables in input(gi ) can be bound only by (i) non-generative parts of P or (ii) outputs of GenOps gj with j < i. All such (i−1) outputs are included in Sγ by construction. Since prompt instantiation depends on a context mapping only via its restriction to input(gi ), the set of instantiated prompts (and hence generated outputs) available for gi un(m) (i−1) der Sγ coincides with that under Sγ . Consequently, no new GenOp-extensions arise when evaluating P relative (m) to Sγ beyond those already produced during the staged S (m)

construction up to m. Therefore JPKGγ

(m)

⊆ Sγ

.

(m)

(2) Sγ

is a fixpoint.

Sγ(m−1)

[m]

(m−1)

JPγ KG = ΦP (Sγ monotonicity of ΦP ,

(m)

By construction, Sγ (m−1)

) and Sγ

(m)

⊆ Sγ

=

. By

Sγ(m) = ΦP (Sγ(m−1) ) ⊆ ΦP (Sγ(m) ). (m)

(m)

Combined with (1), this yields ΦP (Sγ ) = Sγ . Leastness. Let S be any fixpoint of ΦP . Consider the Kleene chain S0 = ∅ and Sn+1 = ΦP (Sn ). By the standard induction argument (using S monotonicity), Sn ⊆ S for all n, hence lfp(ΦP ) = n≥0 Sn ⊆ S. Applying this to the (m)

(m)

fixpoint Sγ yields lfp(ΦP ) ⊆ Sγ . (m) (k) Sγ ⊆ lfp(ΦP ). Each stage Sγ is obtained by one (k−1) [k] application of ΦP [k] to Sγ , and Pγ is a sub-instance γ of P (with some GenOps disabled). Hence every mapping (m) in Sγ is derivable by a finite number of iterations of ΦP S (m) starting from ∅, so Sγ ⊆ n≥0 ΦnP (∅) = lfp(ΦP ). (m) Combining (3) and (4), we arrive to Sγ = lfp(ΦP ). ′

(5) Independence of γ. If γ and γ are two topological orders, standard poset arguments show that γ can be transformed into γ ′ by swapping adjacent incomparable elements. For adjacent incomparable generators gi , gi+1 , neither depends on the other, i.e., out(gi ) ∩ input(gi+1 ) = ∅ and out(gi+1 ) ∩ input(gi ) = ∅. Thus, the set of placeholder-bindings available to each is unchanged by the swap, and so is the set of generated outputs. Repeating swaps yields equality of the final staged sets.

B.2

Context equivalence invariance

Proposition 7 (Context invariance (corrected)). Let S, S ′ ⊆ ΩP be context supplies such that for every GenOp occurrence g in P, ′

S|g = S |g ,

where S|g = {µ ∈ S | input(g) ⊆ dom( µ)}.

S′

S

Thus JPKG = JPKG for all P, and therefore ΦP (S) = ΦP (S ′ ).

B.3

Monotonicity of the consequence operator

We now give a fully detailed proof of Lemma 1. Lemma 4 (Monotonicity of ΦP ). If P is monotone w.r.t. the context supply (main text condition), then ΦP is monotone on (2ΩP , ⊆): S ⊆ S ′ =⇒ ΦP (S) ⊆ ΦP (S ′ ). Proof. We prove the stronger statement: for all patterns P satisfying the monotonicity condition, S′

S

S ⊆ S ′ =⇒ JPKG ⊆ JPKG .

The proof is by structural induction on P.

Case 1: Let P be a BGP. Evaluation then does not depend on context supply. Hence, equality holds.

Then, ΦP (S) = ΦP (S ′ ). S

Proof. We prove by structural induction on P that JPKG = S

S

1. If P = Proj L (P ′ ), then JPKG is obtained by restricting S each mapping in JP ′ KG to L, which preserves equality. 2. If P = P1 Union P2 , then evaluation is set union of the evaluations of P1 and P2 , hence equality follows. 3. If P = P1 Join P2 , then evaluation is the set of unions µ1 ⊎ µ2 for compatible µi from each side. By IH, the sets of µi coincide under S and S ′ , hence the join result coincides. 4. If P = Filter F (P ′ ), evaluation is subset selection of S JP ′ KG by a predicate on µ alone (F µ depends only on µ). Since the underlying set is equal by IH, the filtered subset is equal. 5. The cases Opt , Diff , and Minus are analogous: each is defined purely in terms of membership/compatibility relations among mappings in the evaluated subpatterns, so equality of those evaluated sets implies equality of the resulting sets.

′

JPKG .

Case 2: Let P = g = GenOp(π(X), Y, M). We have Ω S|g ⊆ S ′ |g because S ⊆ S ′ . By the definition of JgKG c as a union over contexts µc ∈ Ωc , enlarging Ωc can only add terms to the union: S

S Base case 1: P is a BGP. Then JPKG is independent of S,

S|

S′ |

S′

JgKG = JgKG g ⊆ JgKG g = JgKG .

hence equality holds.

Base case 2: P is a GenOp pattern g GenOp(π(X), Y, M). By definition, S

S|

JgKG = JgKG g ,

=

S|g = {µ ∈ S : X ⊆ domµ }.

By assumption, for this occurrence g we have S|g = S ′ |g . Hence, the same set of context mappings µc is used in both · evaluations. Since JgKG is defined as a union over all µc S

S′

in the context supply, it follows directly that JgKG = JgKG . Inductive cases. Assume the claim holds for immediate subpatterns.

S

S′

S

S′

Case 3: Let P = Proj L (P ′ ). By IH, JP ′ KG ⊆ JP ′ KG . Restriction to L is monotone on sets: if A ⊆ B then {µ|L : µ ∈ A} ⊆ {µ|L : µ ∈ B}, hence inclusion holds. Case 4: Let P = P1 Union P2 . By IH, JPi KG ⊆ JPi KG . Taking unions preserves inclusion, so the claim follows. S

Case 5: Let P = P1 Join P2 . Let µ ∈ JP1 Join P2 KG . S S Then there exist µ1 ∈ JP1 KG and µ2 ∈ JP2 KG with µ1 ∼ µ2 S′

and µ = µ1 ⊎ µ2 . By IH, µi ∈ JPi KG as well, so the same S′

pair witnesses µ ∈ JP1 Join P2 KG .

S

Case 6: Let P = Filter F (P ′ ). By IH, JP ′ KG ⊆ ′

S JP ′ KG . Now

S

S

JFilter F (P ′ )KG = {µ ∈ JP ′ KG : F µ = ⊤}.

Since the predicate F µ = ⊤ depends only on µ, subset inclusion of the underlying sets yields inclusion of the filtered sets. Case 7: Assume negative constructs. These comprise Minus, Diff, and Opt. In general, such constructs are non-monotone in SPARQL. However, we restrict attention to patterns P satisfying the main-text monotonicity condition: no variable introduced by a GenOp output occurs in a negative position. Under this condition, enlarging the context supply from S to S ′ may introduce additional generated bindings, but these bindings cannot influence the evaluation of any negative construct, since all negative tests range only over variables whose bindings are fixed independently of GenOp outputs. Hence, the truth of membership and compatibility checks performed by negative constructs is invariant under such enlargements. It follows that the denotation of each negative construct is unchanged when passing from S to S ′ , and the desired inclusion holds by the induction hypothesis applied to the positive subpatterns. This completes the induction.

B.4

Least fixpoint: existence, characterization, and minimality

Theorem 9 (Existence and characterization of the least fixpoint). If ΦP is monotone on (2ΩP , ⊆), then: 1. ΦP has a least fixpoint lfp(ΦP ); S 2. lfp(ΦP ) = n≥0 ΦnP (∅); 3. if ΩP is finite, the Kleene chain stabilizes after at most |ΩP | strict increases. (Equivalently, under the alternative assumption that Φ is ωcontinuous, Item 2 holds without requiring finiteness.) Proof. (1) Existence. (2ΩP , ⊆) is a complete lattice. Since Φ is monotone, Knaster–Tarski yields existence of a least fixpoint, namely \ lfp(Φ) = {S ⊆ ΩP | Φ(S) ⊆ S}. (2) Kleene characterization under finiteness. Consider the Kleene sequence by S0 = ∅ and Sn+1 = Φ(Sn ). By monotonicity, S0 ⊆ S1 ⊆ S2 ⊆ · · · . Assume ΩP is finite. Then (Sn )n can strictly increase at most |ΩP | times, hence there exists N ≤ |ΩP | such that SN = SN +1 = Φ(SN ). Thus SN is a fixpoint. To show minimality, let T be any fixpoint of Φ. By induction on n, Sn ⊆ T for all n: base S0 = ∅ ⊆ T , and if Sn ⊆ T then Sn+1 = Φ(Sn ) ⊆ Φ(T ) = T by monotonicity and Φ(T ) = T . Hence SN ⊆ T for every fixpoint T , so SN is the least fixpoint: SN = lfp(Φ).

S (3) Finally, since the chain stabilizes at N , we have n≥0 Sn = SN , and therefore [ lfp(Φ) = SN = Φn (∅), n≥0

with stabilization after at most |ΩP | strict increases. Theorem 10 (Minimality of the least fixpoint). Let S ∗ = lfp(ΦP ) and let S ⊆ ΩP satisfy ΦP (S) ⊆ S (i.e., S is a pre-fixpoint, or closed under one-step consequences). Then S ∗ ⊆ S. Proof. Let S0 = ∅ and Sn+1 = ΦP (Sn ). We show by induction that Sn ⊆ S for all n. Base: S0 = ∅ ⊆ S. Step: assume Sn ⊆ S. By monotonicity, ΦP (Sn ) ⊆ ΦP (S). By assumption ΦP (S) ⊆ S. Therefore SS n+1 = ΦP (Sn ) ⊆ S. Taking unions over n produces S ∗ = n Sn ⊆ S.

B.5

Stratified semantics: well-definedness, uniqueness, and order-independence

Theorem 11 (Well-definedness and uniqueness of stratified semantics). If P is stratified and ΩP is finite, then the stratstrat ified semantics JPKG is well-defined and unique. Proof. Assume stratification σ : gen(P) → N, and let S−1 = ∅ and for each i ≥ 0: Fi (S) := ΦP ≤i (S ∪ Si−1 ),

Si := lfp(Fi ),

where P ≤i denotes the restriction of P to GenOp occurrences in strata at most i, as defined in the main text. We then must show each Fi is monotone, so Si exists and is unique. Let S ⊆ S ′ . Then S∪Si−1 ⊆ S ′ ∪Si−1 . We claim ΦP ≤i is monotone in its context argument when all negative dependencies of generators in strata ≤ i point strictly below i and are, therefore, evaluated against a fixed lower-stratum supply Si−1 . Stratification guarantees that any occurrence of an output variable of a stratum ≤ i generator under a negative operator can only depend on generators in strictly lower strata, hence, is already fixed when computing stratum i. Thus, as the varying part S grows, no negative test that depends on generated variables can flip from true to false. Therefore Lemma 4 applies to the operator S 7→ ΦP ≤i (S ∪ Si−1 ), producing Fi (S) ⊆ Fi (S ′ ). Hence, Fi is monotone on (2ΩP , ⊆), so by Theorem 9 it has a unique least fixpoint Si . Since ΩP is finite, each stratum stabilizes in finitely many steps. The final stratum value Sm (with m = max σ) is, therefore, well-defined and unique. Theorem 12 (Order-independence within strata). Let P be stratified and fix i ≥ 0. Then, the computed stratum value Si = lfp(Fi ) is independent of any operational evaluation order of GenOp occurrences within stratum i, provided that: (i) lower strata < i are fully computed first, and (ii) within stratum i, evaluation is fair in the sense that any enabled GenOp occurrence is eventually applied.

Proof. Within stratum i, semantics is defined denotationally as the least fixpoint of the monotone operator Fi on the complete lattice 2ΩP . Let (Tn )n≥0 be the Kleene S sequence for Fi : T0 = ∅, Tn+1 = Fi (Tn ). Then, Si = n Tn by Theorem 9. Any fair operational schedule that repeatedly applies enabled GenOp occurrences and closes under the algebra corresponds to generating an ascending chain (Uα )α such that: (1) U0 = S ∅, (2) Uα ⊆ Uα+1 ⊆ Fi (Uα ), and (3) the limit U∞ := α Uα is a fixpoint of Fi (fairness ensures no further Fi -consequences are missed). Since Tn is the least chain closed under full application of S Fi , we have by induction Tn ⊆ U∞ for all n, hence Si = n Tn ⊆ U∞ . But, U∞ is a fixpoint of Fi , so by minimality of lfp(Fi ) we also have U∞ ⊆ Si . Therefore, U∞ = Si , showing independence of the operational order.

(3) Finite convergence. Because Cand(P) is finite, 2Cand(P) is finite. By (2), (In+ )n and (In− )n are ascending chains in finite posets, hence, each stabilizes after finitely many strict increases. Therefore, the pair sequence stabilizes.

B.6

C

Well-founded semantics: convergence and uniqueness

Theorem 13 (Convergence and uniqueness of well-founded semantics). If Cand(P) is finite, then the alternating fixpoint sequence (In+ , In− ) from Definition 21 stabilizes after finitely many steps at a pair (I + , I − ), and the induced threevalued interpretation (true on I + , false on I − , undefined otherwise) is unique. Proof. We prove four claims. (1) Each step is well-defined. Fix n ≥ 0. Consider the − Cand(P)\In operator Tn (S) := ΦP (S). By definition of reduct consequence operator, all negative constructs are evaluated against the fixed set Cand(P) \ In− , and thus, do not depend on S. Therefore, Tn is monotone on (2Cand(P) , ⊆): if S ⊆ S ′ , the only dependence on S is through positive constructs, which are monotone in S exactly as in Lemma 4. Hence, + lfp(Tn ) exists and defines In+1 . I+

Similarly, let Un (S) := ΦPn+1 (S), which is monotone − by the same reasoning, and lfp(Un ) exists. Then, In+1 = Cand(P) \ lfp(Un ) is well-defined. + − (2) Monotone growth: In+ ⊆ In+1 and In− ⊆ In+1 . We prove both inclusions by induction on n. Base case is trivial since I0+ = I0− = ∅. − Inductive step: let In− ⊆ In+1 . Then, Cand(P) \ − − In+1 ⊆ Cand(P) \ In . Shrinking the set against which negatives are evaluated makes it harder for negatives to block derivations, so the positive least fixpoint can only grow. That is, for any S, evaluating negative checks against − Cand(P) \ In+1 is weaker than against Cand(P) \ In− , hence, Tn (S) ⊆ Tn+1 (S) pointwise. By monotone operator theory, pointwise inclusion implies inclusion of least + fixpoints: lfp(Tn ) ⊆ lfp(Tn+1 ), hence In+1 ⊇ In+ . + + Next, since In+1 ⊇ In , negative checks evaluated against a larger fixed set may block more derivations, so lfp(Un ) can − only shrink, and thus its complement In+1 can only grow. − − This gives In+1 ⊇ In .

(4) Uniqueness. Let (J + , J − ) be any pair satisfying the alternating fixpoint equations: Cand(P)\J −

J + = lfp S 7→ ΦP

(S) ,

+ J − = Cand(P) \ lfp S 7→ ΦJP (S) . Assume the information ordering (A+ , A− ) ⪯ (B + , B − ) iff A+ ⊆ B + and A− ⊆ B − . The construction starts from the least element (∅, ∅) and, by (2), proceeds monotonically in this ordering, so its limit is the least solution of the defining equations. Therefore, it is unique.

Algebraic Equivalences and Rewrite Rules

All equivalences below are with respect to the denotational semantics JPKG of Section 3 over a fixed RDF graph G. We assume the underlying string similarity Str≃ : Σ∗ × ∗ Σ → [0, 1] is symmetric, i.e., Str≃ (s, s′ ) = Str≃ (s′ , s) for all s, s′ ∈ Σ∗ . Lemma 5 (Symmetry of typed-term similarity). For all typed terms α, β ∈ (T ∪ Tgen ) × {rdf, gen}, we have Sim(α, β) = Sim(β, α), where Sim(·, ·) is defined with Str≃ in Section 3. Proof. Let α = (t, τ ) and β = (t′ , τ ′ ). If τ = τ ′ = rdf, then Sim(α, β) = 1 iff t = t′ and otherwise Sim(α, β) = 0; symmetry is immediate. If (τ, τ ′ ) = (rdf, gen), then Sim(α, β) = Str≃ (Canon(t), Lex(t′ )) and Sim(β, α) = Str≃ (Lex(t′ ), Canon(t)), which are equal by symmetry of Str≃ . The remaining two cases are analogous. Lemma 6 (Symmetry of canonical compatibility). For every variable v ∈ V and typed terms α, β, Compatv (α, β) = ⊤

iff

Compatv (β, α) = ⊤.

Proof. By definition, Compatv (α, β) = ⊤ iff repv (α) = repv (β), which is symmetric. Lemma 7 (Symmetry of mapping compatibility). For all typed solution mappings µ1 , µ2 , µ1 ∼ µ2

iff

µ2 ∼ µ1 .

Proof. By Definition 9, µ1 ∼ µ2 holds iff for every v ∈ domµ1 ∩ domµ2 we have repv (µ1 (v)) = repv (µ2 (v)). This condition is symmetric in µ1 , µ2 . Lemma 8 (Canonical union preserves bindings outside overlaps). If µ1 ∼ µ2 , then: 1. for every v ∈ domµ1 \ domµ2 , (µ1 ⊎ µ2 )(v) = µ1 (v); 2. for every v ∈ domµ2 \ domµ1 , (µ1 ⊎ µ2 )(v) = µ2 (v); 3. for every v ∈ domµ1 ∩ domµ2 , (µ1 ⊎ µ2 )(v) = repv (µ1 (v)) = repv (µ2 (v)). Proof. Immediate from Definition 9.

Lemma 9 (Canonical union is commutative). If µ1 ∼ µ2 , then µ1 ⊎ µ2 = µ2 ⊎ µ1 . Proof. By Lemma 8, both unions agree on variables outside the overlap. On the overlap domµ1 ∩ domµ2 , both yield the representative repv (µ1 (v)) = repv (µ2 (v)). Hence the resulting partial functions are equal. Join

From Section 3:

JP1 Join P2 KG = {µ1 ⊎ µ2 | µ1 ∈ JP1 KG ,

µ2 ∈ JP2 KG , µ1 ∼ µ2 }.

Proposition 8. For all patterns P1 , P2 ,

JP1 Join P2 KG = JP2 Join P1 KG . Proof. Let µ ∈ JP1 Join P2 KG . Then µ = µ1 ⊎ µ2 with µi ∈ JPi KG and µ1 ∼ µ2 . By Lemma 7, µ2 ∼ µ1 , and by Lemma 9, µ = µ2 ⊎ µ1 ∈ JP2 Join P1 KG . The reverse inclusion is symmetric. Proposition 9. For all patterns P1 , P2 , P3 , J(P1 Join P2 ) Join P3 KG = JP1 Join (P2 Join P3 )KG .

Proof. We prove ⊆; the reverse direction is analogous. Let µ ∈ J(P1 Join P2 ) Join P3 KG . Then, there exist µ12 ∈ JP1 Join P2 KG and µ3 ∈ JP3 KG such that µ = µ12 ⊎ µ3 and µ12 ∼ µ3 . Unfolding µ12 ∈ JP1 Join P2 KG , there exist µ1 ∈ JP1 KG and µ2 ∈ JP2 KG such that µ12 = µ1 ⊎ µ2 and µ1 ∼ µ2 . Claim 1: µ2 ∼ µ3 . Let v ∈ domµ2 ∩ domµ3 . Then, v ∈ domµ12 ∩ domµ3 , so µ12 ∼ µ3 gives repv (µ12 (v)) = repv (µ3 (v)). Also, by Lemma 8, µ12 (v) equals either µ2 (v) (if v ∈ / domµ1 ) or repv (µ2 (v)) (if v ∈ domµ1 ∩ domµ2 ), and in both cases repv (µ12 (v)) = repv (µ2 (v)). Hence, repv (µ2 (v)) = repv (µ3 (v)), i.e., µ2 ∼ µ3 . Let µ23 := µ2 ⊎ µ3 . Then µ23 ∈ JP2 Join P3 KG . Claim 2: µ1 ∼ µ23 and µ = µ1 ⊎ µ23 . Let v ∈ domµ1 ∩ domµ23 . If v ∈ domµ2 , then µ1 ∼ µ2 implies repv (µ1 (v)) = repv (µ2 (v)). Moreover, µ23 (v) is either µ2 (v) or repv (µ2 (v)), hence repv (µ23 (v)) = repv (µ2 (v)). Thus repv (µ1 (v)) = repv (µ23 (v)). If instead v ∈ domµ3 \ domµ2 , then v ∈ domµ12 ∩ domµ3 (since v ∈ domµ1 ⊆ domµ12 ), and µ12 ∼ µ3 gives repv (µ12 (v)) = repv (µ3 (v)). But v ∈ / domµ2 implies µ12 (v) = µ1 (v) by Lemma 8, hence repv (µ1 (v)) = repv (µ3 (v)). Also µ23 (v) = µ3 (v), so repv (µ1 (v)) = repv (µ23 (v)). Therefore µ1 ∼ µ23 . For equality, note that both (µ1 ⊎ µ2 ) ⊎ µ3 and µ1 ⊎ (µ2 ⊎ µ3 ) are defined (by the compatibilities shown) and, for each variable v in the union domain, both evaluate to: (i) the unique non-overlap binding when v occurs in exactly one of µ1 , µ2 , µ3 , or (ii) repv (·) of the shared equivalence class when v occurs in two or three of them. Hence (µ1 ⊎ µ2 ) ⊎ µ3 = µ1 ⊎ (µ2 ⊎ µ3 ). Thus µ = µ12 ⊎ µ3 = (µ1 ⊎ µ2 ) ⊎ µ3 = µ1 ⊎ (µ2 ⊎ µ3 ) = µ1 ⊎ µ23 , and therefore µ ∈ JP1 Join (P2 Join P3 )KG .

Proposition 10. For all patterns P1 , P2 , P3 , J(P1 Union P2 ) Join P3 KG =

J(P1 Join P3 ) Union (P2 Join P3 )KG .

Proof. (⊆) Let µ ∈ JP1 Union P2 Join P3 KG . Then µ = µ12 ⊎ µ3 with µ3 ∈ JP3 KG , µ12 ∈ JP1 Union P2 KG , and µ12 ∼ µ3 . By the definition of union, µ12 ∈ JP1 KG or µ12 ∈ JP2 KG . In the first case, µ ∈ JP1 Join P3 KG ; in the second, µ ∈ JP2 Join P3 KG . Thus µ is in the union on the right-hand side. (⊇) If µ ∈ JP1 Join P3 KG , then µ = µ1 ⊎ µ3 with µ1 ∈ JP1 KG . Since JP1 KG ⊆ JP1 Union P2 KG , we have µ ∈ JP1 Union P2 Join P3 KG . The argument for P2 Join P3 is identical. Filter laws (grounded in ε-semantics) Proposition 11 (Filter decomposition). For all patterns P and filter formulas F1 , F2 , JFilter F1 ∧F2 (P )KG = JFilter F1 (Filter F2 (P ))KG . Proof. By definition, JFilter F (P )KG = {µ ∈ JP KG | F µ = ⊤}. By the inductive filter semantics, (F1 ∧ F2 )µ = F1µ ∧ F2µ , and in particular (F1 ∧ F2 )µ = ⊤ iff F1µ = ⊤ and F2µ = ⊤. Thus both sides select exactly the same mappings from JP KG . Lemma 10 (Filter invariance under representative normalization). Let µ be a typed solution mapping and define µ b by µ b(v) = repv (µ(v)) for all v ∈ domµ . Then, for every filter formula F, we have F µ = F µb . Proof. By induction on F. For atoms, the only changes are (i) replacing a binding by another element of the same ≈v -equivalence class, and (ii) possibly replacing an exact RDF match by a representative in that class. In both, (v = c) and (v = v ′ ), the semantics accepts either exact RDF equality (when applicable) or canonical compatibility via Compat· (·, ·), and Compatv (µ(v), (c, rdf)) = ⊤ iff repv (µ(v)) = repv ((c, rdf)) iff Compatv (b µ(v), (c, rdf)) = ⊤. The Boolean cases (¬, ∧) follow immediately. Proposition 12 (Filter pushdown over join (safe form)). Let P1 , P2 be patterns and F a filter formula. Assume that for every µ1 ∈ JP1 KG we have var(F) ⊆ domµ1 . Then, JFilter F (P1 Join P2 )KG =

J(Filter F (P1 )) Join P2 KG .

Symmetrically, if for every µ2 ∈ JP2 KG we have var(F ) ⊆ domµ2 , then JFilter F (P1 Join P2 )KG =

JP1 Join (Filter F (P2 ))KG .

Proof. We prove the first equality; the second is symmetric. (⊆) Let µ ∈ JFilter F (P1 Join P2 )KG . Then µ ∈ JP1 Join P2 KG and F µ = ⊤. So µ = µ1 ⊎ µ2 with µ1 ∈ JP1 KG , µ2 ∈ JP2 KG and µ1 ∼ µ2 . By assumption, var(F) ⊆ domµ1 . Let µ c1 be the representativenormalization of µ1 as in Lemma 10. On all variables in var(F), µ agrees with µ c1 up to representative choice: if v ∈ var(F ) is also in domµ2 , then µ(v) = repv (µ1 (v)) = µ c1 (v) by Definition 9; if v ∈ / domµ2 then µ(v) = µ1 (v) and µ c1 (v) = repv (µ1 (v)), which is still equivalent for filter evaluation by Lemma 10. Hence F µ = ⊤ implies F µ1 = ⊤ (equivalently F µc1 = ⊤), so µ1 ∈ JFilter F (P1 )KG .Thus, µ = µ1 ⊎ µ2 ∈ JFilter F (P1 ) Join P2 KG . (⊇) Let µ ∈ JFilter F (P1 ) Join P2 KG . Then µ = µ1 ⊎ µ2 with µ1 ∈ JFilter F (P1 )KG , µ2 ∈ JP2 KG , and µ1 ∼ µ2 . Thus F µ1 = ⊤ and var(F) ⊆ domµ1 . By Lemma 10, also F µc1 = ⊤. As above, µ agrees with µ c1 on var(F) up to representative choice enforced by ⊎, hence F µ = ⊤. Therefore µ ∈ JFilter F (P1 Join P2 )KG . Minus Proposition 13. If var(P1 ) ∩ var(P2 ) = ∅, then JP1 Minus P2 KG = JP1 KG . Proof. By definition, JP1 Minus P2 KG contains exactly those µ1 ∈ JP1 KG such that for all µ2 ∈ JP2 KG , either µ1 ̸∼ µ2 or domµ1 ∩ domµ2 = ∅. If var(P1 ) ∩ var(P2 ) = ∅, then for all such µ1 , µ2 we have domµ1 ∩ domµ2 = ∅, so no µ1 is removed. Thus, JP1 Minus P2 KG = JP1 KG .

C.1

Context Independence of Base-Mode GenOp Proposition 14 (Base-mode context independence). Let g = GenOp(π(X), Y, M) be a GenOp pattern with input(g) = X = ∅. Assume the base-mode convention of Section 3 that whenever X = ∅, the GenOp is evaluated with context set {∅}. Then, for every supply S ⊆ ΩP ,

Proof. Since X = ∅, we have S|g = {µ ∈ S | ∅ ⊆ domµ } = S. By the base-mode convention, however, the evaluation clause for P ignores its supplied context set and S| {∅} uses {∅} whenever X = ∅. Therefore, JgKG g = JgKG for all S. Corollary 2 (Hoisting base-mode GenOp). Let g = ∅ GenOp(π(∅), Y, M ) and let Ωg = JgKG . Let P be a query pattern that contains no GenOp occurrences. Then, for every RDF graph G and all context supplies S, S ′ , S′

S

JP Join gKG = JP Join gKG = JP Join Ωg KG , where Ωg is treated extensionally as a relation (set of typed solution mappings). Proof. Let S be an arbitrary context supply. Step 1 (base-mode context-independence of g). Since g = GenOp(π(∅), Y, M ) is base-mode, Proposition 14 yields S

Acyclic setting and stagewise (single-pass) evaluation → − Assume the dependency graph D P = (gen(P), →P ) is acyclic, and fix a topological order γ = (g1 , . . . , gm ) of gen(P). For each k ∈ {0, . . . , m}, recall (Appendix B.1) that P ≤k denotes the pattern obtained from P by disabling all GenOp occurrences not among {g1 , . . . , gk } (treating them as returning ∅), while keeping the remaining algebra unchanged. We define stagewise (single-pass) sequence:

,

i.e., the denotation of g is independent of S.

GenOp-Specific Rewriting Rules

In contrast to the purely algebraic equivalences of Section C, the rules in this subsection depend essentially on the contextsensitive evaluation of GenOp patterns (Section 3) and are therefore sound only under explicit side conditions. Throughout, fix an RDF graph G and a well-formed pattern P.

{∅}

S|

JgKG g = JgKG

∅

JgKG = JgKG = Ωg .

(∗)

S

That is, JgKG is independent of S.

Step 2 (context-independence of P). Because P contains no GenOp, its evaluation does not depend on the context supply (Proposition 19 / Proposition 1 in the main text). Hence, for all supplies S, S ′ , S

S′

JPKG = JPKG = JPKG .

(†)

Step 3 (join evaluation and elimination of the context parameter). By the semantic clause for join (Section 3), S

S

S

JP Join gKG = {µ ⊎ ν | µ ∈ JPKG , ν ∈ JgKG , µ ∼ ν}. Substituting (∗) and (†) gives S

∅ Sγ(0) := JP ≤0 KG ,

(k−1)

S Sγ(k) := JP ≤k KGγ

(1 ≤ k ≤ m).

Intuitively, at stage k, only generators among {g1 , . . . , gk } may fire, using as context the supply accumulated at stage k − 1. For a GenOp occurrence g = GenOp(π(X), Y, M) and a supply S, we recall the context restriction operator: S|g := {µ ∈ S | X = input(g) ⊆ domµ }.

JP Join gKG = {µ ⊎ ν | µ ∈ JPKG , ν ∈ Ωg , µ ∼ ν}, which is manifestly independent of S. S S′ Therefore, JP Join gKG = JP Join gKG for all S, S ′ . And, treating Ωg extensionally as a relation and applying the (join) clause of the denotational semantics gives, {µ ⊎ ν | µ ∈ JPKG , ν ∈ Ωg , µ ∼ ν} = JP Join Ωg KG . This establishes the stated equalities.

Proposition 15. Let P1 , P2 be patterns and g a GenOp. For S all G, S and i ∈ {1, 2}, let Si := JPi KG and Si |g := {µ ∈ S | ∪S2 |g

S |

Si | input(g) ⊆ domµ }. If JgKG1 g

= JgKG1 g ∪

S |

JgKG2 g , then

S

J(P1 Union P2 ) Join gKG =

S

J(P1 Join g) Union (P2 Join g)KG .

Proof. Let G be an RDF graph. Let Si := JPi KG and Si |g := Si |g for i ∈ {1, 2}. Step 1: In (P1 Union P2 ) Join g, by removing the designated occurrence of g,
S∪ = J (P1 Union P2 ) Join g \ {g}KG = JP1 Union P2 KG = S1 ∪ S2 .

Therefore, the context set passed to g is

is not guaranteed in general; however, such ω cannot arise from the semantics of g under (P1 Union P2 ) Join g unless g admits cross-branch generation, i.e., unless A2 contributes extensions that are compatible with contexts from S1 . The branch-separability hypothesis (∗) rules out exactly these cross-branch effects by forcing the set of outputs under S1 |g ∪ S2 |g to decompose into outputs attributable to each branch. Thus, every ω witnessed in (4) is witnessed with µ ∈ Si and ν ∈ Ai for the same i, and hence lies in J1 ∪ J2 . (⊇) Let ω ∈ J1 ∪ J2 . If ω ∈ J1 , then ω = µ ⊎ ν with µ ∈ S1 ⊆ S1 ∪ S2 and ν ∈ A1 ⊆ A1 ∪ A2 and µ ∼ ν, so ω belongs to the RHS of (4). The case ω ∈ J2 is symmetric. Therefore, (4) equals J1 ∪ J2 . Step 4: identify Ji with the branch joins and conclude. By the semantics of join and the context-supply convention applied to Pi Join g, JPi Join gKG =

(S1 ∪ S2 )|g = S1 |g ∪ S2 |g . Similarly, in Pi Join g, removing the occurrence of g yields Pi , so the context supply Si = JPi KG and the effective context set is Si |g . Step 2: By the join clause , J(P1 Union P2 ) Join gKG =

{µ ⊎ ν | µ ∈ JP1 Union P2 KG , ν ∈ JgKG , µ ∼ ν}.

(2)

By the union clause, JP1 Union P2 KG = S1 ∪ S2 , and then, by GenOp definition, S |

S | ∪S2 |g

JgKG = JgKG∪ g = JgKG1 g

.

S | ∪S2 |g

{µ ⊎ ν | µ ∈ S1 ∪ S2 , ν ∈ JgKG1 g

, µ ∼ ν}. (3)

Step 3: Assume,

Then, (3) becomes

JP1 Join gKG ∪ JP2 Join gKG =

J(P1 Join g) Union (P2 Join g)KG ,

where the last equality is the union clause. This completes the proof. Proposition 16. Let g = GenOp(π(X), Y, M) and let F be a filter with var(F) ⊆ X. Let P be a pattern such that X ⊆ var(P), Y ∩ var(P) = ∅, and var(F) ⊆ var(P). Then, Proof. Let G be an RDF graph, and assume,

J(P1 Union P2 ) Join gKG =

S | ∪S2 |g

J(P1 Union P2 ) Join gKG = J1 ∪ J2 =

JFilter F (P) Join gKG = JFilter F (P Join g)KG .

Substituting into (2) gives

JgKG1 g

Thus,

S |

{µ ⊎ ν | µ ∈ Si , ν ∈ JgKGi g , µ ∼ ν} = Ji .

S |

S |

= JgKG1 g ∪ JgKG2 g .

J(P1 Union P2 ) Join gKG =

{µ ⊎ ν | µ ∈ S1 ∪ S2 , ν ∈ A1 ∪ A2 , µ ∼ ν},

(∗)

(4)

S | where Ai := JgKGi g .

For i ∈ {1, 2}, let

Ji := {µ ⊎ ν | µ ∈ Si , ν ∈ Ai , µ ∼ ν}. We show that the set on the right-hand side of (4) equals J1 ∪ J2 . (⊆) Let ω be an element of the RHS of (4). Then, ω = µ ⊎ ν with µ ∈ S1 ∪ S2 and ν ∈ A1 ∪ A2 and µ ∼ ν. If µ ∈ S1 and ν ∈ A1 , then ω ∈ J1 . If µ ∈ S2 and ν ∈ A2 , then ω ∈ J2 . If µ ∈ S1 and ν ∈ A2 , then ω ∈ J1 ∪ J2

S := JPKG ,

S + := {µ ∈ S | F µ = ⊤}, S|g := {µ ∈ S | X ⊆ domµ }.

Since X ⊆ var(P) and µ is a solution mapping for P, every µ ∈ S binds all variables in X; hence S|g = S and similarly S + |g = S + . Step 1: expand the left-hand side. In the pattern Filter F (P) Join g, the surrounding pattern of g is Filter F (P), so the context supply for g is JFilter F (P)KG = S + . Then, by the semantics of join and GenOp, JFilter F (P) Join gKG =

S+

{µ ⊎ ν |µ ∈ S + , ν ∈ JgKG , µ ∼ ν}. (5)

Step 2: expand the right-hand side. In the pattern Filter F (P Join g), the join P Join g is evaluated first. Here, the surrounding pattern of g is P, so the context supply for g is S, and thus JP Join gKG =

S

{µ ⊎ ν |µ ∈ S, ν ∈ JgKG , µ ∼ ν}.

(6)

Applying the filter clause, JFilter F (P Join g)KG =

{ω ∈ JP Join gKG | F ω = ⊤}.

(7)

Step 3: relate filter truth before and after joining with g. Let µ ∈ S and let ν be any mapping produced by g from context µ, i.e., ν is of the form µ⊎νY with νY binding only variables {µ} in Y to generated terms, as in the definition of JgKG . Since Y ∩ var(P) = ∅, no variable in Y occurs in P and, in particular, no variable in var(F) is in Y (since var(F ) ⊆ X ⊆ var(P)). Thus, the canonical union µ ⊎ ν does not introduce new bindings for variables in var(F); it may only replace existing bindings by representatives. By Lemma 10 (filter invariance under representative normalization), Fµ = ⊤

←→

F µ⊎ν = ⊤.

(8)

Moreover, by the side condition var(F) ⊆ domµ for all µ ∈ S, F µ ̸= ε, so, (8) is not affected by errors. Step 4: show (5) ⊆ (7). Let ω ∈ JFilter F (P) Join gKG . S+

By (5), ω = µ⊎ν with µ ∈ S + , so F µ = ⊤, and ν ∈ JgKG . S

+

S

Since S + ⊆ S, the GenOp definition implies JgKG ⊆ JgKG . Thus, ω is witnessed in (6), i.e., ω ∈ JP Join gKG . Finally, (8) yields F ω = ⊤, hence ω ∈ JFilter F (P Join g)KG by (7). Step 5: show (7) ⊆ (5). Let ω ∈ JFilter F (P Join g)KG . S By (7) and (6), ω = µ ⊎ ν with µ ∈ S, ν ∈ JgKG , µ ∼ ν, ω µ + and F = ⊤. By (8), F = ⊤, hence µ ∈ S . It remains to ensure that ν is produced from a context in S + . By the GenOp definition, [ {η} S JgKG = JgKG , η∈S

{η}

{η}

so ν ∈ JgKG for some η ∈ S. But any output of JgKG extends η on X (and only adds bindings on Y ); since var(F) ⊆ X, the truth of F for ω = µ ⊎ ν is determined by the X-bindings contributed by the context used to instantiate g, and therefore F η = ⊤ and η ∈ S + . Hence S+ ν ∈ JgKG , and thus ω is witnessed in (5). Therefore ω ∈ JFilter F (P) Join gKG . Steps 4 and 5 give mutual inclusion, proving the equality. Safe Reordering of GenOp with Join Proposition 17 (Safe join reordering around a GenOp). Let g = GenOp(π(X), Y, M) be a GenOp occurrence. Let P1 , P2 be patterns such that: 1. X ⊆ var(P1 ), and 2. var(P2 ) ∩ X = ∅. Then, the following reordering is semantics-preserving (under the denotational semantics of Section 3): ∀G, ∀S, S

S

J(P1 Join P2 ) Join gKG = J(P1 Join g) Join P2 KG .

Remark. The condition domµ2 ∩ X = ∅ strengthens the syntactic condition var(P2 ) ∩ X = ∅ and is needed because var(P2 ) may over-approximate the variables actually bound by P2 (e.g., under Optional and Filter). Proof. Let S be a context supply. S

(⊆) Let µ ∈ J(P1 Join P2 ) Join gKG . By the join clause, there exist S

µ12 ∈ JP1 Join P2 KG

and

such that µ12 ∼ µg and

JP1 Join P2 KS G |g

µg ∈ JgKG

µ = µ12 ⊎ µg .

(9)

S

S

Unfolding µ12 ∈ JP1 Join P2 KG , there exist µ1 ∈ JP1 KG S and µ2 ∈ JP2 KG with µ1 ∼ µ2 and µ12 = µ1 ⊎ µ2 .

(10)

Claim 1: µ1 ∼ µg . Let v ∈ domµ1 ∩ domµg . Then v ∈ domµ12 ∩ domµg because domµ1 ⊆ domµ12 by (10). Since µ12 ∼ µg , Compatv (µ12 (v), µg (v)) = ⊤, i.e., repv (µ12 (v)) = repv (µg (v)). We show that repv (µ12 (v)) = repv (µ1 (v)). There are two sub-cases. 1. If v ∈ domµ1 \ domµ2 , then by Definition 9 (canonical union), µ12 (v) = µ1 (v), hence trivially repv (µ12 (v)) = repv (µ1 (v)). 2. If v ∈ domµ1 ∩ domµ2 , then by Definition 9 (compatibility), µ1 ∼ µ2 implies Compatv (µ1 (v), µ2 (v)) = ⊤ so repv (µ1 (v)) = repv (µ2 (v)). Again by canonical union, µ12 (v) = repv (µ1 (v))

(equivalently = repv (µ2 (v))).

Since repv is idempotent on representatives, we have repv (µ12 (v)) = repv (repv (µ1 (v))) = repv (µ1 (v)). Thus, in all cases repv (µ12 (v)) = repv (µ1 (v)), and therefore repv (µ1 (v)) = repv (µg (v)), i.e., Compatv (µ1 (v), µg (v)) = ⊤. Since this holds for all shared v, we conclude µ1 ∼ µg . Let µ1g := µ1 ⊎ µg , which is well-defined by Claim 1. Then S µ1g ∈ JP1 Join gKG . Claim 2: µ1g ∼ µ2 . Let v ∈ domµ1g ∩ domµ2 . There are two cases. 1. If v ∈ domµ1 ∩ domµ2 , then µ1 ∼ µ2 yields repv (µ1 (v)) = repv (µ2 (v)). Moreover, by Definition 9, µ1g (v) = repv (µ1 (v)), hence repv (µ1g (v)) = repv (repv (µ1 (v))) = repv (µ1 (v)) = repv (µ2 (v)), so, Compatv (µ1g (v), µ2 (v)) = ⊤.

2. Otherwise, v ∈ / domµ1 and thus v ∈ domµg ∩ domµ2 . Then v ∈ domµ12 ∩ domµg because v ∈ domµ2 ⊆ domµ12 . Since µ12 ∼ µg , repv (µ12 (v)) = repv (µg (v)). We also have v ∈ / domµ1 , hence by the canonical union definition µ12 (v) = µ2 (v). Therefore, repv (µ2 (v)) = repv (µg (v)). Finally, because v ∈ / domµ1 , canonical union gives µ1g (v) = µg (v), so repv (µ1g (v)) = repv (µg (v)) = repv (µ2 (v)), i.e. Compatv (µ1g (v), µ2 (v)) = ⊤. Thus µ1g ∼ µ2 holds. Since µ1g ∼ µ2 , the union µ1g ⊎µ2 is defined and belongs to S J(P1 Join g) Join P2 KG . It remains to show that it equals µ. Claim 3: µ = (µ1 ⊎ µg ) ⊎ µ2 . Both sides are defined and have the same domain domµ1 ∪ domµ2 ∪ domµg . We check pointwise that they coincide using Definition 9. Let v be any variable. 1. If v ∈ domµ1 ∩ domµ2 , then µ12 (v) = repv (µ1 (v)) and  repv (µ12 (v)) if v ∈ domµg , µ(v) = (µ12 ⊎µg )(v) = µ12 (v) if v ∈ / domµg . On the other hand, (µ1 ⊎ µg )(v) is either repv (µ1 (v)) (if v ∈ domµg ) or µ1 (v) (if v ∈ / domµg ), and then union with µ2 makes the result repv (µ1 (v)) in either subcase because v ∈ domµ2 and repv (µ1 (v)) = repv (µ2 (v)). Thus both constructions yield the same value. 2. If v ∈ domµ1 \ domµ2 , then µ12 (v) = µ1 (v) and a direct inspection of the two unions shows both yield repv (µ1 (v)) if v ∈ domµg and µ1 (v) otherwise. 3. If v ∈ domµ2 \ domµ1 , then µ12 (v) = µ2 (v) and similarly both yield repv (µ2 (v)) if v ∈ domµg and µ2 (v) otherwise. 4. If v ∈ domµg \ (domµ1 ∪ domµ2 ), then both yield µg (v). Hence µ = (µ1 ⊎ µg ) ⊎ µ2 , and therefore µ S J(P1 Join g) Join P2 KG .

∈

The reverse inclusion (⊇) is analogous.

Order Invariance under Acyclic GenOp Dependencies → − Proposition 18. Assume D P is acyclic. Let γ and γ ′ be two topological orders of gen(P). Then, the final stagewise results coincide: (m) Sγ(m) = Sγ ′ . Proof. We prove that swapping adjacent incomparable generators does not change the final result, and then conclude by a standard swap argument. Step 1: a single adjacent swap is harmless. Let γ = (. . . , gi , gi+1 , . . . ) be a topological order such that gi and gi+1 are incomparable (no edges in either direction). Let γ ′ be the order obtained by swapping them: γ ′ = (. . . , gi+1 , gi , . . . ).

Incomparability means: out(gi ) ∩ input(gi+1 ) = ∅ and out(gi+1 ) ∩ input(gi ) = ∅. Consider the stage just before either of these two generators is applied; call the current supply S (this is the same set for both orders up to that point). Because out(gi ) does not occur among placeholders of gi+1 , evaluating gi may add bindings to out(gi ), but cannot change which mappings in S bind all of input(gi+1 ), hence it cannot change S|gi+1 nor any instantiated prompt for gi+1 . Symmetrically, evaluating gi+1 first cannot change the contexts for gi . Therefore, the sets of generated extensions contributed by gi and gi+1 are the same regardless of which is applied first, and since join is associative, the supply after applying both is identical under γ and γ ′ . For any two topological orders are connected by adjacent swaps. It is standard that any two linear extensions of a finite poset can be transformed into each other by repeatedly swapping adjacent incomparable elements. Applying Step 1 along this sequence of swaps shows that the final result is invariant. (m) (m) Therefore, Sγ = Sγ ′ . (Alternatively, theorem is exactly Item (3) of Theorem 8. Briefly, if two GenOp occurrences are incomparable in the dependency graph, neither depends on the outputs of the other, so swapping their evaluation order does not change the extracted contexts or the generated extensions. Any two topological orders are related by a sequence of such swaps, and the resulting stagewise evaluations therefore coincide.)

C.2

Conservativity w.r.t. SPARQL

Proposition 19. Let P be a well-formed graph pattern that contains no occurrence of GenOp. Then, for any RDF graph G, evaluation of P under the extended semantics coincides with standard SPARQL evaluation:
JPKG = JPKG standard SPARQL . Proof. Let G be fixed. Since P contains no GenOp, the evaluation rules for JPKG never invoke any context-dependent generator clause and, therefore, never introduce gen-typed values. Hence, every mapping µ ∈ JPKG assigns variables only to RDF-typed terms, i.e., values in T × {rdf}. We first show that on RDF-typed values the extended notions of compatibility and canonical union coincide with SPARQL’s usual agreement-on-overlap and set-theoretic union. Claim 1 (RDF-typed compatibility collapses to equality). Let v ∈ V and let α = (t, rdf) and β = (t′ , rdf). Then Compatv (α, β) = ⊤

iff

t = t′ .

By definition, Compatv (α, β) = ⊤ iff repv (α) = repv (β). For RDF-typed inputs, the typed-term similarity Sim(α, β) equals 1 exactly when t = t′ and otherwise 0 (Section 3). Thus the induced ≈v -classes are singletons, so repv (t, rdf) = (t, rdf) and the equivalence follows.

Claim 2 (Mapping compatibility and canonical union coincide with SPARQL). Let µ1 , µ2 be typed solution mappings with range contained in T × {rdf}. Then: (i) µ1 ∼ µ2 iff µ1 and µ2 agree on every shared variable; and (ii) whenever µ1 ∼ µ2 , the canonical union µ1 ⊎ µ2 coincides with the ordinary union of partial functions µ1 ∪ µ2 . For (i), unfold µ1 ∼ µ2 : for all v ∈ domµ1 ∩ domµ2 we require repv (µ1 (v)) = repv (µ2 (v)), which by Claim 1 is equivalent to equality of the underlying RDF terms. For (ii), by Definition 9, ⊎ preserves non-overlapping bindings and, on overlaps, returns the representative; by Claim 1 this representative is the same RDF-typed binding. We now prove the proposition by structural induction on P. Base case (BGP). For a basic graph pattern, the extended semantics matches triples in G exactly as SPARQL does; the only difference is that bound RDF terms are tagged by rdf. Forgetting this tag yields precisely the standard SPARQL BGP solution mappings, hence the two evaluations coincide. Inductive steps. Assume the claim holds for strict subpatterns. For each constructor of graph patterns used in P (join, union, optional, minus/diff, filter, projection, etc.), the extended semantics is defined by the standard SPARQL settheoretic clause, except that it uses ∼ for join compatibility and ⊎ for merging compatible mappings, and it evaluates filter atoms using canonical compatibility. On the fragment without GenOp, all intermediate mappings are RDF-typed, so by Claims 1–2 these operations coincide with SPARQL agreement on overlaps, ordinary union, and standard filter evaluation. Therefore, each constructor yields exactly the same set of solutions as standard SPARQL. Consequently, JPKG = (JPKG )|standard SPARQL .

C.3

Optimizer Implications

Propositions 14–18 justify standard optimizer actions in the acyclic fragment: 1. Hoisting base-mode GenOps. By Corollary 2, a GenOp with input(g) = ∅ can be evaluated once and treated as a constant relation, avoiding repeated model calls and enabling early materialization. 2. Join reordering around GenOps under safe side conditions. Proposition 17 characterizes when a GenOp may be moved across a join without changing the extracted context used for its evaluation, allowing cost-based join planning while preserving semantics. 3. Topological freedom in acyclic programs. Proposition 18 shows that any topological order of acyclic generative de(m) pendencies yields the same final stagewise result Sγ , enabling planners to choose among valid orders using cost estimates (e.g., prompt cost, expected fan-out). These principles do not apply unchanged to cyclic dependencies, where least-fixpoint or well-founded semantics is required and intermediate results may depend on iteration strategy rather than a single-pass topological order.

D

Proofs for Executable Fixpoint Evaluation

We prove the guarantees stated for Algorithm 1: exactness on the chosen candidate set, soundness relative to the self-

support target, relative completeness under candidate coverage, and termination.

D.1

Objects and explicit assumptions

Let G be an RDF graph, let P be a graph pattern, and let C ⊆ gen(P) be an SCC. Let XC and YC be as in the main text, and let η be an outer binding with XC ⊆ dom( η). Let ΩP denote the universe of typed solution mappings used in the semantics. Self-support. For µ ∈ ΩP , we write SSC (µ) if XC ⊆ dom( µ) and, for every g = GenOp(π(Xg ), Yg , M) ∈ C, the following conditions hold. Let θg := µ|Xg and νg := µ|Yg . Then, dom( θg ) = Xg ,

dom( νg ) = Yg ,

µ|Xg ∪Yg = θg ⊎ νg , {θ }

θg ⊎ νg ∈ JgKG g .

(⋆)

Self C (η) = {µ|YC | µ ∈ ΩP , µ ⊇ η, SSC (µ)}.

(†)

and

Self-support target under an outer binding. We define the self-support answer set of C under η by

Under the finite candidate coverage and exactness assumption from Sect. 6, this set coincides with the declarative answer projections for the component under η. Candidate set. Algorithm 1 constructs a finite candidate set CandC (η) ⊆ ΩP whose elements extend η and bind the variables in YC . The algorithm returns RC (η) = {µ|YC | µ ∈ CandC (η) ∧ SSC (µ)}.

(‡)

Validation. Algorithm 1 tests self-support using Validate. We use the following semantic correctness assumption. Assumption 1. For every g = GenOp(π(Xg ), Yg , M) ∈ C, every typed mapping θ with dom( θ) = Xg , every typed mapping ν with dom( ν) = Yg , and every repetition parameter R, {θ}

Validate(g, θ, ν; R) = ⊤ ⇐⇒ θ ⊎ ν ∈ JgKG .

Remark 3. The assumption 1 fixes the model, decoding, parsing, normalization, and repetition policy used by the validation oracle.

D.2

Exactness on the candidate set

Theorem 14. For any finite candidate set CandC (η) constructed by the algorithm, Algorithm 1 returns exactly RC (η) as defined in (‡). Proof. We prove both inclusions. (⊆) Let ρ be returned by the algorithm. Then the algorithm added ρ = µ|YC for some µ ∈ CandC (η) whose validation test succeeded. Thus, for every g = GenOp(π(Xg ), Yg , M) ∈ C, with θ: = µ|Xg and νg = µ|Yg , the algorithm checks dom( νg ) = Yg ,

µ|Xg ∪Yg = θg ⊎ νg , and

Validate(g, θg , νg ; R) = ⊤.

D.4

By Assumption 1, {θ }

θg ⊎ νg ∈ JgKG g .

Thus, SSC (µ) holds by (⋆). Since µ ∈ CandC (η) and ρ = µ|YC , we obtain ρ ∈ RC (η). (⊇) Let ρ ∈ RC (η). By (‡), there exists µ ∈ CandC (η) such that ρ = µ|YC and SSC (µ). For every g = GenOp(π(Xg ), Yg , M) ∈ C, let θg := µ|Xg

and

νg := µ|Yg .

By (⋆), {θ }

Relative completeness

Theorem 16 (Relative completeness under candidate coverage). Assume that the candidate set covers all selfsupporting extensions of η: ∀µ ∈ ΩP : (µ ⊇ η ∧ SSC (µ)) ⇒ µ ∈ CandC (η). (♣) Then, RC (η) = Self C (η). Proof. We prove both inclusions. (⊆) By Theorem 15, every returned projection belongs to the self-support target. Hence RC (η) ⊆ Self C (η).

Under the finite candidate coverage and exactness assumption from Sect. 6, this set coincides with the declarative answer projections for the component under η.

(⊇) Let ρ ∈ Self C (η). By the definition of Self C (η) in (†), there exists a mapping µ ∈ ΩP such that ρ = µ|YC , µ ⊇ η and SSC (µ). The coverage assumption (♣) applies to this µ, since it extends η and satisfies SSC (µ). Therefore, µ ∈ CandC (η). Now we have µ ∈ CandC (η) and SSC (µ). By the definition of RC (η) in (‡), the projection µ|YC belongs to RC (η). Since ρ = µ|YC , we obtain ρ ∈ RC (η). Thus, Self C (η) ⊆ RC (η). Combining the two inclusions gives RC (η) = Self C (η), ref. equation 11. Therefore, the equality above gives relative completeness for the declarative component answers.

D.3

D.5

dom( νg ) = Yg ,

µ|Xg ∪Yg = θg ⊎νg , and θg ⊎νg ∈ JgKG g .

Assumption 1 gives

Validate(g, θg , νg ; R) = ⊤. Therefore, the validation test succeeds when the algorithm processes µ, and the algorithm adds µ|YC = ρ to the output. Hence, ρ is returned. Both inclusions hold, so the returned set is exactly RC (η). Self-support target. We define the self-support answer set of C under η by Self C (η) = {µ|YC | µ ∈ ΩP , µ ⊇ η, SSC (µ)}.

(11)

Soundness

Termination

Theorem 15 (Soundness relative to the self-support target). For every outer binding η,

Theorem 17 (Termination). For fixed bounds (K, B, T, R), Algorithm 1 terminates.

RC (η) ⊆ Self C (η).

Proof. We bound each phase. Candidate enumeration. For each v ∈ YC , the algorithm maintains a finite set D[v] and enforces |D[v]| ≤ B. Hence the total number of successful insertions into all candidate domains is bounded by X |D[v]| ≤ B|YC |.

Proof. Let ρ ∈ RC (η). By the definition of the returned set in (‡), there exists a candidate µ ∈ CandC (η) such that ρ = µ|YC

and

SSC (µ).

The candidate set CandC (η) is constructed from the outer binding η by assigning values to the variables generated inside C. Hence every candidate in CandC (η) extends η, and therefore µ ⊇ η. Combining the three facts ρ = µ|YC ,

µ⊇η

and

SSC (µ),

we obtain exactly the membership condition in the definition of Self C (η) in (†). Thus, ρ ∈ Self C (η). Since ρ was arbitrary, RC (η) ⊆ Self C (η), ref. equation 11. Therefore, every projection returned by the algorithm is sound with respect to those declarative component answers.

v∈YC

The saturation test stops the enumeration once a full pass adds no new value or all domains reach their cap. Therefore the enumeration loop is finite. Candidate construction. After enumeration, each D[v] is finite. Thus Y |CandC (η)| ≤ |D[v]| ≤ B |YC | . v∈YC

So the candidate set is finite. Validation and repair. The algorithm iterates over the finite set CandC (η). For each candidate and each g ∈ C, it performs at most R validation repetitions. Repair attempts are bounded by T , and each repair invokes only finitely many calls to Propose and Validate, bounded by K and R. All phases are finite; thus Algorithm 1 terminates.

E

Complexity

We prove Theorem 7 using the SCC-based execution scheme from Section 6. The proof is deliberately local: it bounds one SCC call, one accepted projection, and one algebraic constructor at a time. Throughout this section, the RDF graph G is an input. Generated values occur only as values of typed solution mappings. We count calls to proposal, parsing, and validation procedures as symbolic oracle calls on polynomial-size encodings; the internal neural-inference cost is outside the symbolic query-evaluation problem.

E.1

Decision Problem and Exact SCC-Bounded Evaluation

Definition 24. (Evaluation-membership problem) An instance consists of a graph pattern P, an RDF graph G, a typed solution mapping µ with dom( µ) ⊆ var(P), and Sem ∈ {lfp, strat, wfs}. The task is to decide membership whether Sem

Lemma 11. Deterministic bounded generation assumption, together with fixed Section 6 parameters (K, B, T, R) and polynomial-size encodings, gives the finite local candidatedomain clauses of Assumption 2. Lemma 11 does not imply the semantic exactness clause of Assumption 2. Proof. Deterministic bounded generation assumption fixes the model specifier, prompt instantiation, decoding, parsing, and normalization. Hence one instantiated prompt has one finite deterministic set of parsed outputs. Algorithm 1 uses the fixed proposal bound K and the fixed per-variable cap B; therefore, for each generated variable v ∈ YC , it constructs a finite domain satisfying η |DC [v]| ≤ B.

Consequently, the candidate construction has the product form CandC (η) = {η ⊎ ν | ν : YC → Tgen × {gen},

µ ∈ JPKG .

For Sem = wfs, membership means membership in the true component of the well-founded value; false and undefined status queries are not part of this decision problem. Data complexity fixes P, Sem, and the execution parameters of Algorithm 1; only G and µ vary. Combined complexity takes P, G, and µ as input, while the execution parameters remain fixed constants of the semantics. Assumption 2. (Exact SCC-bounded executable) Let C be an SCC of the generative-dependency graph of P. Let   [ [ YC = out(g) and XC =  input(g) \ YC . g∈C

η [v] for every v ∈ YC , η ∼ ν}, ν(v) ∈ DC

which is the finite-domain part of Assumption 2. The validation phase defines the accepted projection relation RC (η) by the self-support test SSC . None of these finite-domain facts entails RC (η) = AnsSem C (η), where AnsSem C (η) denotes the declarative SCC-answer projection under Sem. That equality is exactly the semantic exactness premise stated separately in Assumption 2. Thus bounded generation supplies finite local bounds and polynomial encodings, while Assumption 2 supplies the additional exactness needed by the complexity proof.

g∈C

For every outer binding η with XC ⊆ dom( η), Algorithm 1 η constructs finite domains DC [v] for v ∈ YC such that η |DC [v]| ≤ B,

where B is a fixed execution parameter. It forms CandC (η) := {η ⊎ ν | ν : YC → Tgen × {gen}, η ν(v) ∈ DC [v] for every v ∈ YC , η ∼ ν}.

The accepted projection set is RC (η) := {ρ | ∃θ ∈ CandC (η) : ρ = θ|YC and SSC (θ)}. The regime is exact when RC (η) equals the declarative SCC-answer projection for C under η, for the chosen semantics Sem ∈ {lfp, strat, wfs} and for every generative SCC and every outer binding used during evaluation. This equality is a semantic exactness premise: deterministic bounded generation supplies finite deterministic candidate domains, but it does not by itself imply equality between self-supported candidates and the declarative least-fixpoint, stratified, or well-founded answers. Every generated value, prompt instance, parsed tuple, candidate, and validation object has representation length polynomial in |P| + |G| + |µ|.

For an SCC C, write NC := B |YC | . In data complexity, NC is a constant because P is fixed. In combined complexity, NC can be exponential in |P|, but one assignment ν : YC → Tgen × {gen} has polynomial representation length.

E.2

Typed SCC Condensation

Definition 25 (Typed SCC summary operator). For an SCC C, the summary operator GenSCCC maps a context supply S to the typed mapping set S

JGenSCCC KG = {η ⊎ ρ | η ∈ S, XC ⊆ dom( η), ρ ∈ RC (η), η ∼ ρ}.

Thus, RC (η) remains the YC -projection returned by Algorithm 1, while GenSCCC reattaches the outer binding η before the surrounding SPARQL algebra consumes the result. b is obtained from P by replacing The condensed pattern P every generative SCC C by GenSCCC and preserving the surrounding SPARQL algebraic structure.

Lemma 12. Under Assumption 2, for each semantics symbol Sem ∈ {lfp, strat, wfs} and each typed mapping µ, Sem µ ∈ JPKG

⇐⇒

is surjective by the definition of RC (η). Thus, |RC (η)| ≤ |{θ ∈ CandC (η) | SSC (θ)}| ≤ |CandC (η)| ≤ NC .

b {∅} . µ ∈ JPK G

For Sem = wfs, the left-hand side denotes membership in the true component.

For the summary operator, let BC (S) = {(η, ρ) | η ∈ S, XC ⊆ dom( η),

Proof. Let C be one generative SCC and let S be the context supply reaching C. The declarative contribution of C under S is AC (S) = {η ⊎ ρ | η ∈ S, XC ⊆ dom( η), ρ ∈ AnsSem C (η), η ∼ ρ},

ρ ∈ RC (η), η ∼ ρ}. Then, S

|JGenSCCC KG | = |{η ⊎ ρ | (η, ρ) ∈ BC (S)}| ≤ |BC (S)| X ≤

where AnsSem C (η) is the declarative SCC-answer projection under η for the chosen semantics Sem. Assumption 2 gives AnsSem C (η) = RC (η)

|RC (η)|

η∈S, XC ⊆dom( η)

for every admissible η. ≤

Substituting this equality in the definition of AC (S) yields

X

NC

η∈S

AC (S) = {η ⊎ ρ | η ∈ S, XC ⊆ dom( η), ρ ∈ RC (η), η ∼ ρ}

= NC · |S|.

S = JGenSCCC KG .

Thus, replacing C by GenSCCC preserves the relation supplied to the parent algebraic constructor. Repeating this argument along the SCC condensation order replaces every generative component by an extensionally equal summary. Projection, filtering, union, join, difference, minus, and optional are compositional: equal input relations give equal output relations by their set-theoretic definitions. Thus, the final root relation is unchanged. For well-founded semantics, the same replacement is applied to the true component of each exact local summary, which is the component queried by Definition 24. Lemma 13. Let C be an SCC and let η be an outer binding for C. Then, |CandC (η)| ≤ NC

and

|RC (η)| ≤ NC .

For every context supply S, S

|JGenSCCC KG | ≤ NC · |S|.

Proof. A candidate is determined by one value choice for each generated variable. Therefore, η |CandC (η)| = |{η ⊎ ν | ∀v ∈ YC : ν(v) ∈ DC [v], η ∼ ν}| η ≤ |{ν | ∀v ∈ YC : ν(v) ∈ DC [v]}| Y η ≤ |DC [v]|

Lemma 14 (Validation of One Accepted Projection). Let C be an SCC, let η be an outer binding, and let ρ be a mapping with dom( ρ) = YC . Deciding whether ρ ∈ RC (η) uses polynomial time in data complexity and polynomial space in combined complexity. Proof. Put mC := |C|,

yC := |YC |,

n := |P| + |G| + |η| + |ρ|.

Let p(n) bound the symbolic time and space needed to construct, inspect, or compare one generated value, prompt instance, parsed tuple, mapping restriction, or validation input. Assumption 2 gives such a polynomial. By the definition of RC (η) in Assumption 2, membership expands as ρ ∈ RC (η) ⇐⇒ ∃θ ∈ CandC (η) : ρ = θ|YC ∧ SSC (θ). (12) Expanding the candidate product gives the following equivalent form: ρ ∈ RC (η) ⇐⇒ ∃ν : dom( ν) = YC , η ∀v ∈ YC : ν(v) ∈ DC [v], η ∼ ν, ρ = (η ⊎ ν)|YC , SSC (η ⊎ ν).

(13)

v∈YC

≤

Y

B

v∈YC

= B |YC | = NC . The projection map h : {θ ∈ CandC (η) | SSC (θ)} → RC (η), h(θ) := θ|YC .

Indeed, if (12) holds, then θ ∈ CandC (η) means that there is a total assignment ν : YC → Tgen × {gen} such that θ = η ⊎ ν,

η ∀v ∈ YC : ν(v) ∈ DC [v],

η ∼ ν.

Together with ρ = θ|YC and SSC (θ), this yields (13). Conversely, any ν satisfying (13) yields θ := η⊎ν ∈ CandC (η), ρ = θ|YC , and SSC (θ); hence (12) holds. This derivation does not require dom( η) ∩ YC = ∅: if η already binds

a variable in YC , compatibility η ∼ ν and the equality ρ = (η ⊎ ν)|YC enforce the shared value. We now bound the decision procedure induced by (13). Candidate-Assignment Part. For a guessed or enumerated assignment ν, the product-membership test is ^ η ν(v) ∈ DC [v]∧η ∼ ν∧ρ = (η⊎ν)|YC . dom( ν) = YC ∧ v∈YC η For each v ∈ YC , the scan over DC [v] has at most B elements. Thus, for one ν, the symbolic time is bounded by

E.3

Polynomial Bounds for Fixed Condensed Patterns

Lemma 15. Let B0 = {t1 , . . . , tm } be a fixed basic graph pattern. Then, |JB0 KG | ≤ |G|m .

Moreover, JB0 KG can be enumerated in polynomial time for fixed B0 . Proof. For each triple pattern ti , let Mi := {a ∈ G | a matches ti }.

B · yC · p(n) + p(n) ≤ (ByC + 1)p(n), Then,

and the symbolic space is bounded by O(1)

p(n) + O(log yC ) ≤ n

.

Self-support part. Let θ := η ⊎ ν. The self-support predicate expands as ^ {θ } SSC (θ) ⇐⇒ XC ⊆ dom( θ) ∧ θ ∈ JgKG |input(g) . g∈C

Using validation correctness, each conjunct for g = GenOp(π(Xg ), Yg , Mg ) is checked by applying the validation procedure to the two restrictions θ|Xg and θ|Yg . Each restriction has polynomial encoding length, and hence one validation check costs at most p(n) symbolic time and space. Therefore, the self-support phase for one ν has time X p(n) = mC p(n), g∈C

and space p(n) + O(log mC ) ≤ nO(1) . Data-complexity bound. When P is fixed, yC , mC , and NC = B yC are constants. A deterministic algorithm enumerates all assignments Y η ν∈ DC [v] v∈YC

and applies the preceding checks. The number of assignments is at most Y η |DC [v]| ≤ B yC = NC , v∈YC

so the total symbolic time is bounded by
NC (ByC + 1)p(n) + mC p(n) , which is polynomial in the data input because NC , B, yC , and mC are constants. The algorithm stores only one assignment ν, one mapping θ, and one validation configuration at a time, thus, the space is polynomial as well. Combined-complexity bound. When P is part of the input, NC may be exponential. The procedure need not enumerate or store all assignments. It nondeterministically guesses one assignment ν of polynomial representation length and checks the right-hand side of (13). The space used is

|Mi | ≤ |G|

for every i.

Every solution of B0 is induced by a compatible tuple from M1 × · · · × Mm . Hence, |JB0 KG | ≤ |M1 × · · · × Mm | m Y = |Mi | ≤

i=1 m Y

|G|

i=1 m

= |G| . Enumeration uses nested loops over M1 , . . . , Mm , checks compatibility, and stores one m-tuple of RDF triples and one induced mapping at a time. Since m is fixed, the enumeration time is polynomial in |G|. Lemma 16 (Polynomial preservation by fixed condensed b If the input patterns). Let Q be a fixed subpattern of P. context supply S(G) satisfies |S(G)| ≤ qS (|G|) for a polynomial qS , then there is a polynomial qQ such that S(G)

|JQKG

| ≤ qQ (|G|). S(G)

If S(G) can be enumerated in polynomial time, then JQKG can be enumerated in polynomial time for fixed Q.

Proof. We use structural induction on Q. Put n := |G|. For a proper subpattern Qi , write S(G)

Ωi := JQi KG

,

|Ωi | ≤ qi (n).

Basic graph pattern. For Q = B0 , Lemma 15 gives S

|JB0 KG | = |JB0 KG | ≤ nm .

Set qQ (n) := nm . SCC summary. For Q = GenSCCC , Lemma 13 gives S

|ν| + |η ⊎ ν| + p(n) + O(log(|C| + |YC |)) ≤ nO(1) .

|JGenSCCC KG | ≤ NC · |S|

Thus, the test is in NPSPACE, and by NPSPACE=PSPACE, it is decidable in polynomial space.

Since Q is fixed, NC is constant. Set qQ (n) := NC qS (n).

≤ NC · qS (n).

S

Projection. For Q = Proj L (Q1 ), put Ω := JQKG . Then,

Therefore Ω ⊆ Ω1 , and

Ω = {µ|L | µ ∈ Ω1 }. The map ρL : Ω1 → Ω, ρL (µ) = µ|L , is surjective. Therefore, |Ω| = |ρL (Ω1 )| ≤ |Ω1 | ≤ q1 (n).

|Ω| ≤ |Ω1 | ≤ q1 (n). Set qQ (n) := q1 (n). Minus. For Q = Q1 Minus Q2 , S

Ω := JQKG = {µ1 ∈ Ω1 | ¬∃µ2 ∈ Ω2 :

µ1 ∼ µ2 ∧ dom( µ1 ) ∩ dom( µ2 ) ̸= ∅}.

Set qQ (n) := q1 (n). Filter. For Q = Filter F (Q1 ),

Thus, Ω ⊆ Ω1 , and |Ω| ≤ |Ω1 | ≤ q1 (n).

S

Hence,

Ω := JQKG = {µ ∈ Ω1 | F µ = ⊤}. Set qQ (n) := q1 (n).

|Ω| = |{µ ∈ Ω1 | F µ = ⊤}| ≤ |Ω1 | ≤ q1 (n).

Optional. For Q = Q1 Opt F Q2 , the main semantics is S

Set qQ (n) := q1 (n). Union. For Q = Q1 Union Q2 ,

S

Set J := {µ1 ⊎ µ2 | µ1 ∈ Ω1 , µ2 ∈ Ω2 , µ1 ∼ µ2 },

S

Ω := JQKG = Ω1 ∪ Ω2 .

Thus,

S

JQKG = JQ1 Join Q2 KG ∪ JQ1 Diff F Q2 KG .

DF := {µ1 ∈ Ω1 | ∀µ2 ∈ Ω2 : µ1 ̸∼ µ2 or F µ1 ⊎µ2 = ⊥}. Then, Ω = J ∪ DF . The join and difference derivations give

|Ω| = |Ω1 ∪ Ω2 | = |Ω1 | + |Ω2 | − |Ω1 ∩ Ω2 | ≤ |Ω1 | + |Ω2 | ≤ q1 (n) + q2 (n).

|J| ≤ |Ω1 | · |Ω2 | ≤ q1 (n)q2 (n), |DF | ≤ |Ω1 | ≤ q1 (n), |Ω| = |J ∪ DF | ≤ |J| + |DF | ≤ q1 (n)q2 (n) + q1 (n).

Set qQ (n) := q1 (n) + q2 (n). Join. For Q = Q1 Join Q2 , S

Ω := JQKG = {µ1 ⊎ µ2 | µ1 ∈ Ω1 , µ2 ∈ Ω2 , µ1 ∼ µ2 }.

Let

A := {(µ1 , µ2 ) ∈ Ω1 × Ω2 | µ1 ∼ µ2 }. The map h : A → Ω, h(µ1 , µ2 ) = µ1 ⊎ µ2 , is surjective. Hence,

Set qQ (n) := q1 (n)q2 (n) + q1 (n). Each qQ is obtained from qS and the induction polynomials by a finite number of additions and multiplications. Because Q is fixed, the induction depth is fixed; therefore qQ is a polynomial. For enumeration, the displayed definitions give the following time recurrences for fixed Q: TGenSCCC (n) ≤ |S|NC nO(1) ,

|Ω| ≤ |A| ≤ |Ω1 × Ω2 | = |Ω1 | · |Ω2 | ≤ q1 (n)q2 (n).

TProj L (Q1 ) (n) ≤ T1 (n) + |Ω1 |nO(1) , TFilter F (Q1 ) (n) ≤ T1 (n) + |Ω1 |nO(1) ,

Set qQ (n) := q1 (n)q2 (n). Difference. For Q = Q1 Diff F Q2 , the main semantics gives S

Ω := JQKG = {µ1 ∈ Ω1 | ∀µ2 ∈ Ω2 :

µ1 ̸∼ µ2 or F µ1 ⊎µ2 = ⊥}.

TQ1 Union Q2 (n) ≤ T1 (n) + T2 (n) + (|Ω1 | + |Ω2 |)nO(1) , TQ1 Join Q2 (n) ≤ T1 (n) + T2 (n) + |Ω1 ||Ω2 |nO(1) ,
TQ1 Diff F Q2 (n) ≤ T1 (n) + |Ω1 | T2 (n) + |Ω2 |nO(1) ,
TQ1 Minus Q2 (n) ≤ T1 (n) + |Ω1 | T2 (n) + |Ω2 |nO(1) , TQ1 Opt F Q2 (n) ≤ TQ1 Join Q2 (n) + TQ1 Diff F Q2 (n) + (|J| + |DF |)nO(1) .

Equivalently, µ1 ∈ Ω ⇐⇒ µ1 ∈ Ω1 ∧ ¬∃µ2 ∈ Ω2 : µ1 ∼ µ2 ∧ F

µ1 ⊎µ2

̸= ⊥.

All cardinalities on the right-hand side are polynomial by the preceding derivations. Hence enumeration is polynomial time for fixed Q.

E.4

Data Complexity

Theorem 18 (Data-complexity upper bound). Under Assumption 2, the evaluation-membership problem for acyclic patterns, stratified patterns, and non-stratified patterns under well-founded semantics is decidable in deterministic polynomial time in |G| + |µ|. Sem

Proof. By Lemma 12, membership in JPKG to membership in b {∅} . JPK

InS(η) = ⊤

G

|{∅}| = 1. b and S = {∅} gives a polyApplying Lemma 16 to Q = P nomial qPb such that {∅}

b |JPK b (|G|). G | ≤ qP The enumeration part of Lemma 16, together with Lemma 14, computes the condensed relation in time qPb (|G|) · (|G| + |µ|)O(1) . The final membership test scans the computed relation and compares each mapping with µ, which costs qPb (|G|) · |µ|O(1) . Both bounds are polynomial in |G| + |µ|. The argument is independent of whether Sem is lfp, strat, or wfs, because exact SCC condensation has already converted the generative components into typed summary operators.

⇐⇒

MEM(Q, G, InS, µ) S

that decides whether µ ∈ JQKG for every subpattern Q of b provided InS decides membership in the input supply S P, using polynomial space. Proof. Let n := |Q| + |G| + |µ|. We give a nondeterministic polynomial-space procedure for membership and use NPSPACE = PSPACE; for negative subtests we use closure of PSPACE under complement. Basic graph pattern. For Q = B0 = {t1 , . . . , tm }, µ ∈ JB0 KG ⇐⇒ ∃(a1 , . . . , am ) ∈ G m : m m ^ [ ai matches ti and µ = µai . i=1

i=1

The procedure guesses ai sequentially, stores at most m RDF triples and the accumulated mapping, and checks compatibility after each guess. The space is O(m log |G|) + |µ|O(1) ≤ nO(1) . SCC summary. For Q = GenSCCC , Definition 25 gives S

µ ∈ JGenSCCC KG ⇐⇒ ∃η, ρ :

Combined Complexity

For combined complexity, P is part of the input. Then, |YC | may be linear in |P|, and NC = B |YC | may be exponential. The upper-bound proof therefore stores and validates one assignment ρ at a time. Theorem 19 (Combined PSPACE-hardness). For each Sem ∈ {lfp, strat, wfs}, the evaluation-membership problem is PSPACE-hard in combined complexity. Proof. Given a standard SPARQL pattern P0 , an RDF graph G, and a mapping µ, view P0 as a generative SPARQL pattern with no GenOp occurrence. Then

(P0 , G, µ) 7−→ (P0 , G, µ) is therefore a polynomial-time many-one reduction to generative SPARQL membership.

InS(η) = ⊤, XC ⊆ dom( η), ρ ∈ RC (η), η ∼ ρ, µ = η ⊎ ρ.

The guessed mappings η and ρ assign only variables occurring in Q, hence have polynomial length. The test InS(η) uses polynomial space by hypothesis. The test ρ ∈ RC (η) uses polynomial space by Lemma 14. Thus, sQ (n) ≤ sInS (n) + nO(1) . Projection. For Q = Proj L (Q1 ), S

S

µ ∈ JQKG ⇐⇒ ∃µ′ : µ′|L = µ ∧ µ′ ∈ JQ1 KG .

The guessed µ′ assigns only variables of Q1 , so

Sem JP0 KG = JP0 KG

for every Sem ∈ {lfp, strat, wfs}, because there is no generated value, no generative SCC, and no self-support validation. Standard SPARQL membership is PSPACE-hard in combined complexity (Pérez, Arenas, and Gutierrez 2006; Pérez, Arenas, and Gutierrez 2009). The identity map

η ∈ S.

Lemma 17. There is a polynomial-space procedure

is equivalent

Since P is fixed in data complexity, the condensed pattern b is fixed. The initial supply satisfies P

E.5

Definition 26. A predicate InS is an implicit membership predicate for a conceptual set S of typed solution mappings if, for every typed mapping η,

sQ (n) ≤ sQ1 (n) + nO(1) . Filter. For Q = Filter F (Q1 ), S

Thus,

S

µ ∈ JQKG ⇐⇒ F µ = ⊤ ∧ µ ∈ JQ1 KG . sQ (n) ≤ sQ1 (n) + nO(1) .

Union. For Q = Q1 Union Q2 , S

S

S

µ ∈ JQKG ⇐⇒ µ ∈ JQ1 KG ∨ µ ∈ JQ2 KG .

The first disjunct has the join-space bound and the second has the difference-space bound. Hence,

Hence, sQ (n) ≤ max{sQ1 (n), sQ2 (n)} + nO(1) .

sQ (n) ≤ sQ1 (n) + sQ2 (n) + nO(1) . The recursive membership calls follow the syntax tree of Q and have depth at most |Q|. At each level, the procedure stores only polynomial-size mappings, indices, and one subcall configuration. Hence the total space is polynomial in n.

Join. For Q = Q1 Join Q2 , S

S

µ ∈ JQKG ⇐⇒ ∃µ1 , µ2 :

µ1 ∈ JQ1 KG , S µ2 ∈ JQ2 KG , µ1 ∼ µ2 , µ = µ 1 ⊎ µ2 .

The procedure guesses µ1 , µ2 , checks compatibility and equality with µ, and calls the two subprocedures sequentially. Therefore, sQ (n) ≤ sQ1 (n) + sQ2 (n) + nO(1) .

Theorem 20 (Combined PSPACE upper bound). Under Assumption 2, the evaluation-membership problem is in PSPACE in combined complexity for Sem ∈ {lfp, strat, wfs}. Proof. By Lemma 12, Sem

µ ∈ JPKG

Difference. For Q = Q1 Diff F Q2 , S

S

µ ∈ JQKG ⇐⇒ µ ∈ JQ1 KG ∧ ¬∃µ2 :

S

µ2 ∈ JQ2 KG , µ ∼ µ2 , F µ⊎µ2 ̸= ⊥.

The existential right-witness test uses space sQ2 (n)+nO(1) , and its complement is in PSPACE. Thus sQ (n) ≤ sQ1 (n) + sQ2 (n) + nO(1) .

S

S

∧ ¬∃µ2 :

S

µ2 ∈ JQ2 KG , µ ∼ µ2 , dom( µ) ∩ dom( µ2 ) ̸= ∅.

Therefore,

Optional. For Q = Q1 Opt F Q2 ,

Thus,

Let S0 := {∅}. Its implicit membership predicate is InS0 (η) = ⊤ ⇐⇒ η = ∅, which is decidable in polynomial space. Applying b S = S0 , and InS = InS0 yields a Lemma 17 to Q = P, polynomial-space test for the right-hand side. The equivalence above transfers the bound to the original pattern P. For Sem = wfs, this decides membership in the true component, as specified in Definition 24.

Proof. The lower bound is Theorem 19. The upper bound is Theorem 20. Therefore the problem is PSPACE-complete.

E.6 sQ (n) ≤ sQ1 (n) + sQ2 (n) + nO(1) .

S

S

S

JQKG = JQ1 Join Q2 KG ∪ JQ1 Diff F Q2 KG . 



    S µ ∈ JQKG ⇐⇒  ∃µ1 , µ2 :    

b {∅} . µ ∈ JPK G

Theorem 21 (Combined PSPACE-completeness). Under Assumption 2, the evaluation-membership problem is PSPACE-complete in combined complexity for Sem ∈ {lfp, strat, wfs}.

Minus. For Q = Q1 Minus Q2 , µ ∈ JQKG ⇐⇒ µ ∈ JQ1 KG

⇐⇒

   S  µ1 ∈ JQ1 KG ,   S µ2 ∈ JQ2 KG ,    µ1 ∼ µ2 , µ = µ 1 ⊎ µ2 

        S . ∨ µ ∈ JQ K , 1 G    ¬∃µ : µ ∈ JQ KS ,  2 2 2 G    µ ∼ µ2 ,  F µ⊎µ2 ̸= ⊥

Proof of Theorem 7

Proof of Theorem 7. The bounded-generation statement in the main theorem is used only to obtain finite local candidate domains and polynomial-size encodings, as stated in Lemma 11. The equality between accepted SCC projections and declarative SCC answers is the separate semantic exactness premise in Assumption 2. Under that exact SCCbounded regime, Lemma 12 reduces membership for P to b membership for the typed condensed pattern P. The data-complexity upper bound follows from Theorem 18. The combined-complexity lower bound follows from Theorem 19. The combined-complexity upper bound follows from Theorem 20. Combining the lower and upper bounds gives Theorem 21. The proof uses only local products Y η DC [v] v∈YC

and one-projection validation tests in the following existential generated-assignment form: ^ η ρ ∈ RC (η) ⇐⇒ ∃ν : dom( ν) = YC ∧ ν(v) ∈ DC [v] ∧ η ∼ ν ∧ v∈YC

ρ = (η ⊎ ν)|YC ∧ SSC (η ⊎ ν).

It therefore avoids both the invalid global generated-term universe argument and the invalid simplification that would identify the returned projection ρ with the generated assignment without checking the projection equation.

Related documents

• DiaLSM: Towards Write-Stall-Free Performance via Shard-based LSM-tree#919518
• Towards Anticipatory Databases Through Shared Data and Workload Semantics#919519
• Semantic Knowledge Technologies: what the Semantic Web lost sight of, and what it never had#919520
• Specification-Driven Data Architecture Reconstruction: From Physical Code to Logical and Conceptual Specifications#919521
• Numerical Stability of Linear Algebra Operations over Relational Databases#919522