Graphiti: Bridging Graph and Relational Database Queries

1 Introduction

• Graph and relational queries require a formal correspondence because their different data models complicate both equivalence definitions and verification.Relational systems use tables, rows, and joins, whereas graph systems use nodes, edges, and traversals.Source: §1 · pp. 1–2
• Graphiti embeds a Cypher subset into SQL through syntax-directed, correct-by-construction transpilation, mapping graph paths to relational joins over an induced schema.The translation must carefully preserve semantics for simple and complex multi-step pattern matching.Source: §1 · p. 2
• Database transformers map graph instances to relational instances, providing the foundation for defining equivalence across arbitrary schemas.The paper adapts this concept from schema mappings and uses it as a correctness specification.Source: §1 · pp. 2–3
• For arbitrary target schemas, Graphiti computes a residual transformer after schema differencing and reduces equivalence to SQL-query equivalence checked by existing tools.This avoids simultaneously encoding graph and relational structures in SMT reasoning.Source: §1 · pp. 2–3
• Graphiti evaluated 410 benchmarks, finding violations in 34 cases, verifying about 80% of supported aggregation-free queries unboundedly, and producing SQL competitive with manual queries.The bounded evaluation included 45 public, 160 student-translated, and 205 ChatGPT-translated benchmarks.Source: §1 · p. 3

CONCEPT PA SENTENCE :CS :SP

• The graph schema contains CONCEPT, PA, and SENTENCE node types with CS and SP relationships between them.The figure caption identifies the pair as relational and graph schemas; the graph elements are named in the accompanying schema description.Source: Figure 2 · p. 4, CONCEPT PA SENTENCE :CS :SP · p. 4
• The paper’s contributions include a formal graph–relational equivalence foundation, a standard database transformer, and automated verification and falsification through Graphiti.These contributions establish the framework and its empirical tool implementation.Source: CONCEPT PA SENTENCE :CS :SP · p. 4

2 Motivating Example

• The SQL and Cypher queries agree on related concept identifiers but produce different relationship frequencies, demonstrating non-equivalence.The discrepancy appears in the Count column when both queries run on the example database instances.Source: §2 · p. 5, Figure 4 · p. 5
• A standard database transformer specifies how graph nodes and edges generate rows in the induced relational schema.Its rules relate graph elements such as CONCEPT, CS, and PA to relational tables such as Concept and Cs.Source: §2 · p. 5, Figure 5 · p. 5
• The example represents graph nodes and edges as relational tables, with additional source and target attributes encoding graph incidence through foreign keys.The induced schema maps node and edge types to tables and uses functional dependencies and foreign keys to preserve graph structure.Source: §2 · p. 6, Figure 6 · p. 6
• Syntax-directed transpilation maps Cypher path patterns to joins and translates clauses such as WITH and aggregation into intermediate SQL operations.Shared variables induce joins between intermediate results, while the final RETURN aggregation becomes a GroupBy operation.Source: §2 · p. 6, Figure 7 · p. 6
• For arbitrary target schemas, the method infers a residual transformer and delegates equivalence checking between the resulting SQL queries to existing SQL reasoning tools.This extends correct-by-construction transpilation beyond the induced schema and supports refutation with counterexamples.Source: Figure 8 · p. 6, §2 · p. 7

3.1 Background on Graph Databases

• A property graph contains typed nodes and edges carrying key-value properties, and its schema comprises uniquely labeled node and edge types.Node and edge types specify labels, endpoint types, and property keys; the first node key serves as a globally unique default key.Source: §3.1 · p. 7
• Graph database instances are formally represented by node and edge sets, property values, and a typing function constrained by the graph schema.Edges are pairs of nodes, while the property function assigns values to nodes and edges.Source: §3.1 · pp. 7–8

3.2 Query Language for Graph Databases

• Featherweight Cypher supports return queries, ordering, pattern matching, expressions, unions, and aggregation, while excluding unbounded paths and reachability primitives.The restricted fragment is chosen because its constructs are expressible in the core SQL fragment used by the paper.Source: §3.2 · p. 8, Figure 9 · p. 8
• A Featherweight Cypher MATCH pattern retrieves graph paths, and RETURN reshapes the matched paths into a table with projected properties and aggregates.The example counts employees connected to departments through WORK_AT edges and returns department names with counts.Source: §3.2 · p. 8

3.3 Relational Databases

• Relational schemas specify relation-to-attribute mappings and integrity constraints, including primary keys, foreign keys, and not-null conditions.Relational instances are collections of attribute-value tuples, and the considered SQL fragment extends relational algebra with grouping, ordering, and WITH clauses.Source: §3.3 · pp. 8–9

4.1 Language for Database Transformers

• A database transformer is expressed as universally quantified first-order rules whose predicates describe graph or relational elements and generate predicates in another instance.The DSL uses rules of the form P1, ..., Pn → P0, with variables, constants, and fresh-variable underscores.Source: §4.1 · pp. 9–10, Figure 12 · p. 10
• The transformer semantics encode database instances as ground predicates and evaluate rules under Herbrand semantics.The function C maps relational records, graph nodes, and graph edges into predicate sets representing database structure and contents.Source: §4.1 · p. 10

4.2 Equivalence Checking Problem

• Database instances are equivalent modulo Φ when applying Φ to one instance yields the other, establishing the data correspondence needed across graph and relational models.For the example transformer, Φ(G) = R.Source: §4.1 · p. 10, §4.2 · p. 11
• Two query outputs are table-equivalent when a bijection matches their columns and preserves tuple multiplicities, disregarding column names and order.This makes equivalence robust to attribute renaming and reordering.Source: §4.2 · p. 11
• Graph-relational query equivalence holds when queries over schemas ΨG and ΨR produce table-equivalent outputs on database instances related by transformer Φ.The equivalence-checking problem is to decide whether Q ≃Φ Q′.Source: §4.2 · pp. 10–11

5 Equivalence Checking Algorithm

• The three-step algorithm infers an induced schema and standard transformer, transpiles Cypher, and checks the resulting SQL query against the target SQL query.The final comparison uses a residual transformer connecting the induced and desired relational schemas.Source: §5 · pp. 11–12, §5.3 · p. 16

5.1 Induced Relational Schema and Standard Transformer Inference

• The induced relational schema represents each node and edge type as a table, using node keys as primary keys and edge endpoints as foreign keys.The standard transformer maps graph nodes and edges, including their attributes, into tuples in the corresponding relational tables.Source: §5.1 · pp. 12–13

5.2 Syntax-Directed Transpilation

• Syntax-directed transpilation maps Cypher path patterns to SQL joins, with Match using inner joins and OptionalMatch using left outer joins.Shared variables are joined on primary keys so repeated graph variables refer to the same relational tuple.Source: §5.2 · pp. 13–15
• Cypher returns with aggregation are translated into SQL GroupBy queries, using non-aggregated expressions as grouping keys.The worked example translates Count(n.id) grouped by m.dname and renames the projected outputs.Source: §5.2 · p. 14
• The translation is sound and complete for the supported Cypher grammar, yielding an equivalent SQL query over the induced schema.The soundness and completeness theorems establish both correctness of produced translations and existence of a translation for every accepted query.Source: §5.2 · p. 16

5.3 Reduction to SQL Equivalence Checking

• The reduction substitutes standard-transformer predicates into the user transformer, then applies SQL equivalence checking to the resulting query pair.The soundness and completeness results connect the reduced SQL check with equivalence of the original Cypher and SQL queries modulo the given transformer.Source: §5.3 · pp. 16–17, F Proofs · p. 43

6.1 Evaluation of Graphiti with BMC backend

• 34 of 410 benchmarks were refuted in an average of 23.4 seconds, while the remaining 376 received bounded verification at average symbolic-table size 19.6.All 34 counterexamples were manually confirmed as true positives.Source: §6.1 · p. 18
• Graphiti found counterexamples in 13% of GPT-transpiled queries and also uncovered incorrect translations in expert-written, tutorial, academic, and VeriEQL benchmarks.The reported examples include a faulty equivalence claim in a Neo4j tutorial.Source: §6.1 · pp. 18–19

6.2 Evaluation of Graphiti with Deductive Verifier

• Among 196 benchmarks supported by Mediator, Graphiti proved equivalence for 77.6% with an average runtime of 16.8 seconds.The remaining cases were either refuted by VeriEQL, timed out, or returned Unknown because Mediator could not infer suitable invariants.Source: §6.2 · pp. 19–20

6.3 Evaluation of Transpilation

• Graphiti transpiled all 410 queries, with average, median, and maximum times of 6.3, 3.0, and 180.2 milliseconds.These measurements support the paper’s conclusion that transpilation is fast in practice.Source: §6.3 · pp. 20–21
• 33.3% of transpiled queries were faster than manually written SQL, while 51.1% were within a 1.2x slowdown.The remaining benchmarks had slowdowns above 1.2x or between the reported smaller slowdown ranges.Source: §6.3 · pp. 20–21

Automated reasoning for SQL

• SQL verification offers decision procedures, sound incomplete methods, and bounded bug-finding tools, which Graphiti can reuse after reducing graph–relational equivalence to SQL equivalence.The approach can benefit from future advances in automated SQL reasoning.Source: §7 · p. 21

Migration between database instances

• Existing graph–relational migration work can transform database contents, but Dynamite cannot transpile queries, while this paper formalizes Cypher-to-SQL transpilation for equivalence checking.The paper positions its database-transformer framework as related to, but distinct from, prior migration work.Source: §7 · p. 21

Data representation refactoring

• Graphiti treats query translation as data-representation refactoring and introduces an auxiliary relational representation to simplify syntax-directed translation and verification.The authors state that this layer-of-indirection methodology had not previously been explored for this context.Source: §7 · p. 21

Graph database query languages

• Graph-query semantics research motivates viewing graph schemas as graphical representations of relational schemas, and the authors suggest adapting the methodology beyond Cypher.The proposed extension is based on semantic and syntactic similarities among graph query languages.Source: §7 · pp. 21–22

Testing database queries

• Testing techniques are complementary to Graphiti because its SQL-based verification pipeline can use or benefit from advances in SQL query testing.The related work includes differential, metamorphic, mutation-based, and provenance-based testing.Source: §7 · p. 22

Transpiling Cypher queries

• Existing Cypher transpilers either support limited subsets without soundness guarantees or execute an intermediate representation instead of emitting SQL.Graphiti is distinguished by sound transpilation for a broader Cypher subset and by producing SQL queries.Source: §7 · p. 22

• Graphiti does not yet cover modern features such as variable-length pattern matching in Cypher.The authors regard the selected fragments as a foundation and report that benchmarks, including real-world queries, show practical expressiveness.Source: §8 · p. 22

• The paper defines graph-relational query equivalence, transpiles Cypher to SQL over an induced relational schema, and leverages SQL equivalence reasoning.The approach also checks graph and SQL queries over arbitrary schemas.Source: §9 · p. 22
• Graphiti uncovers subtle bugs in supposedly equivalent Cypher queries and verifies full equivalence between Cypher and SQL queries.Source: §9 · p. 22
• Future work includes a graphical interface for specifying database transformers to reduce manual verification effort.The planned interface is inspired by schema-mapping visualization work.Source: §9 · p. 22

A Semantics of Cypher Queries

• A Cypher query maps a property graph instance to a table, with Return evaluating clauses into rows and named columns.Union, UnionAll, and OrderBy have semantics analogous to SQL.Source: A Semantics of Cypher Queries · pp. 26–27
• Cypher clauses produce lists of matched subgraphs; Match combines patterns and predicates, OptMatch supplies nulls for missing patterns, and With renames bindings.Source: A Semantics of Cypher Queries · pp. 26–27
• Path matching returns subgraphs for node or directed edge patterns, while expressions evaluate properties, values, aggregates, casts, and arithmetic over matched subgraphs.Predicates use SQL-style three-valued logic with Null.Source: A Semantics of Cypher Queries · pp. 26, 28

B Transpilation of Cypher Predicates and Expressions

• Existential Cypher predicates translate patterns into SQL subqueries and test membership using projected primary-key attributes.This implements whether the graph pattern has a match.Source: B Transpilation of Cypher Predicates… · pp. 28–29

C An Equivalent Cypher Query of Motivating Example

• Moving filtering into an EXISTS condition restores equivalence by restricting each SENTENCE node before the second MATCH and preventing double counting.The original WITH filter did not constrain individual matches in the later pattern.Source: C An Equivalent Cypher Query of… · p. 29

• Manually written bugs commonly arise from nested matches replacing existential patterns and from misusing path patterns for OPTIONAL MATCH.Source: D Qualitative Analysis of… · p. 29
• Graphiti's bug analysis covers additional query examples from tutorials and benchmark datasets, including VeriEQL-derived queries.Source: D Qualitative Analysis of… · pp. 29–30, Table 5 · p. 30
• A Cypher translation can miss the left-outer-join behavior of SQL when an OPTIONAL MATCH path omits the missing product case.The analyzed tutorial query therefore differs from the SQL query's treatment of absent products.Source: D Qualitative Analysis of… · p. 29
• Reusing a node variable instead of introducing a distinct DEPT node makes the Cypher query non-equivalent to its SQL counterpart.Graphiti finds that the SQL returns (10,5,10) while the Cypher query returns an empty result.Source: D Qualitative Analysis of… · p. 30, Figure 23 · p. 30

• 284 of 410 queries (69%) fall outside OpenCypherTranspiler’s supported Cypher fragment, leaving only 126 benchmarks for comparison.Source: E Comparing Graphiti’s Transpiler with… · p. 30
• Among the 126 supported benchmarks, OpenCypherTranspiler produces syntactically invalid SQL for 2 queries and semantically incorrect SQL for 2 others.Source: E Comparing Graphiti’s Transpiler with… · p. 30
• Graphiti correctly transpiles all 410 Cypher queries used in the evaluation.Source: E Comparing Graphiti’s Transpiler with… · p. 30
• The examples expose unsupported aggregate expressions, undefined SQL table names, and incorrect handling of an optional match.OpenCypherTranspiler does not support Count(*) or Avg(*), can emit SQL referencing an undefined table U, and generates an incorrect translation for a query whose correct SQL uses a left join.Source: E Comparing Graphiti’s Transpiler with… · p. 31

Theorem F.1

• Theorem F.1 proves soundness: translating any Cypher query over a graph schema yields an SQL query equivalent modulo the standard database transformer Φsdt.The proof proceeds by structural induction over Return, OrderBy, Union, and UnionAll, preserving grouping, ordering, duplicate elimination, and concatenation.Source: F Proofs · pp. 31–33

Lemma F.2

• Lemma F.2 establishes clause-level correspondence under Φsdt for Match, chained MATCH, OptMatch, and With translations.The proof aligns graph filtering and merging with SQL selection and joins, represents optional matches using nullified tuples, and maps variable renaming to SQL projection aliases.Source: F Proofs · pp. 33–35

Lemma F.3

• Lemma F.3 shows that translated Cypher patterns correspond to relational joins over labeled node and edge tables under Φsdt.The induction handles node patterns and chained patterns by matching shared variables and link predicates, with graph merging corresponding to relational join composition.Source: F Proofs · pp. 35–36

Lemma F.4

• Lemma F.4 proves expression-level correspondence for property lookup, constants, casts, counts, sums, averages, and minima between graph and relational semantics.The cases preserve null behavior and aggregate evaluation across corresponding graph lists and relational tuples.Source: F Proofs · pp. 36–37

Query translation

• Theorem F.6 states that every Cypher query accepted by the specified grammar has a corresponding SQL query over the induced relational schema.The proof proceeds by structural induction on the query syntax.Source: F Proofs · p. 39

Clause translation

• Lemma F.7 establishes that every accepted Cypher clause can be translated into a SQL query under the standard database transformer.The proof covers Match, OptMatch, and With clauses, using selection, joins, and projection.Source: F Proofs · p. 40

Pattern translation

• The proof uses structural induction and, for a three-part pattern, constructs a SQL expression by joining Q1, Q2, and Q3 with link predicates ϕ1 and ϕ2.The predicates ϕ1 and ϕ2 join the relations Λ(l1) with Λ(l2), and Λ(l2) with Λ(l3), respectively.Source: F Proofs · p. 41

Expression and predicate translation

• Lemmas F.9 and F.10 show that every grammar-accepted Cypher expression and predicate has a corresponding SQL expression or predicate under the specified schema mappings.The expression result is proved by structural induction, including Count, Max, Min, Avg, and Sum; each Cypher aggregation function has an equivalent SQL counterpart.Source: F Proofs · pp. 40–41

• The residual database transformer generated by Algorithm 2 preserves correspondence between transformed node and edge relations and their original relational tables.The proof handles node-label and edge-label substitutions syntactically, showing that the resulting residual transformer maps induced relations back to the corresponding tables.Source: F Proofs · pp. 42–43
• Lemma F.12 shows that if a graph query and SQL query are equivalent under a database transformer, their translated SQL query is equivalent under the residual transformer.This follows by combining translation correctness with the residual-transformer relationship between induced relational instances and the original relational database.Source: F Proofs · p. 43
• The equivalence-checking procedure is sound: whenever CheckEquivalence returns ⊤, the original Cypher and SQL queries are equivalent under their database transformer.Soundness is obtained by reducing the translated Cypher query and the SQL query to SQL equivalence under the residual transformer.Source: F Proofs · p. 43
• The procedure is complete: if the original Cypher and SQL queries are equivalent under the database transformer, CheckEquivalence returns ⊤.Completeness follows from Lemma F.12 and completeness of the underlying SQL equivalence checker.Source: F Proofs · pp. 43–44