Saved in:
Bibliographic Details
Main Authors: Tang, Lei, Dou, Wensheng, Zheng, Yingying, Xu, Lijie, Wang, Wei, Wei, Jun, Huang, Tao
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2504.15742
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917994713579520
author Tang, Lei
Dou, Wensheng
Zheng, Yingying
Xu, Lijie
Wang, Wei
Wei, Jun
Huang, Tao
author_facet Tang, Lei
Dou, Wensheng
Zheng, Yingying
Xu, Lijie
Wang, Wei
Wei, Jun
Huang, Tao
contents Graph database systems store graph data as nodes and relationships, and utilize graph query languages (e.g., Cypher) for efficiently querying graph data. Proving the equivalence of graph queries is an important foundation for optimizing graph query performance, ensuring graph query reliability, etc. Although researchers have proposed many SQL query equivalence provers for relational database systems, these provers cannot be directly applied to prove the equivalence of graph queries. The difficulty lies in the fact that graph query languages (e.g., Cypher) adopt significantly different data models (property graph model vs. relational model) and query patterns (graph pattern matching vs. tabular tuple calculus) from SQL. In this paper, we propose GraphQE, an automated prover to determine whether two Cypher queries are semantically equivalent. We design a U-semiring based Cypher algebraic representation to model the semantics of Cypher queries. Our Cypher algebraic representation is built on the algebraic structure of unbounded semirings, and can sufficiently express nodes and relationships in property graphs and complex Cypher queries. Then, determining the equivalence of two Cypher queries is transformed into determining the equivalence of the corresponding Cypher algebraic representations, which can be verified by SMT solvers. To evaluate the effectiveness of GraphQE, we construct a dataset consisting of 148 pairs of equivalent Cypher queries. Among them, we have successfully proven 138 pairs of equivalent Cypher queries, demonstrating the effectiveness of GraphQE.
format Preprint
id arxiv_https___arxiv_org_abs_2504_15742
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Proving Cypher Query Equivalence
Tang, Lei
Dou, Wensheng
Zheng, Yingying
Xu, Lijie
Wang, Wei
Wei, Jun
Huang, Tao
Databases
Software Engineering
Graph database systems store graph data as nodes and relationships, and utilize graph query languages (e.g., Cypher) for efficiently querying graph data. Proving the equivalence of graph queries is an important foundation for optimizing graph query performance, ensuring graph query reliability, etc. Although researchers have proposed many SQL query equivalence provers for relational database systems, these provers cannot be directly applied to prove the equivalence of graph queries. The difficulty lies in the fact that graph query languages (e.g., Cypher) adopt significantly different data models (property graph model vs. relational model) and query patterns (graph pattern matching vs. tabular tuple calculus) from SQL. In this paper, we propose GraphQE, an automated prover to determine whether two Cypher queries are semantically equivalent. We design a U-semiring based Cypher algebraic representation to model the semantics of Cypher queries. Our Cypher algebraic representation is built on the algebraic structure of unbounded semirings, and can sufficiently express nodes and relationships in property graphs and complex Cypher queries. Then, determining the equivalence of two Cypher queries is transformed into determining the equivalence of the corresponding Cypher algebraic representations, which can be verified by SMT solvers. To evaluate the effectiveness of GraphQE, we construct a dataset consisting of 148 pairs of equivalent Cypher queries. Among them, we have successfully proven 138 pairs of equivalent Cypher queries, demonstrating the effectiveness of GraphQE.
title Proving Cypher Query Equivalence
topic Databases
Software Engineering
url https://arxiv.org/abs/2504.15742