一句话:提出将 Cypher 图查询与 SQL 关系查询的等价性检查归约为 SQL 查询等价性验证的方法与工具 Graphiti。
本文研究如何自动判定 Cypher 图数据库查询与 SQL 关系查询之间的等价性。由于二者基于不同数据模型,作者首先提出 database transformer 概念,用以在模型之间转换数据库实例并定义“模 transformer 的等价性”。基于此,论文提出一种验证方法:通过语法制导翻译将 Cypher 的一个子集嵌入 SQL,进而把原始跨模型等价问题归约为两个 SQL 查询之间的等价性检查,从而复用已有的 SQL 自动推理技术,避免同时推理两种数据模型。作者实现了工具 Graphiti,并用于检查图查询与关系查询的等价性。实验表明,Graphiti 既能证明等价也能发现不等价,并能揭示 Cypher 教程和学术论文中隐藏的细微错误。
This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitable notion of equivalence in this setting, we introduce the concept of database transformers , which transform database instances between graph and relational models. We then propose a novel verification methodology that checks equivalence modulo a given transformer by reducing the original problem to verifying equivalence between a pair of SQL queries. This reduction is achieved by embedding a subset of Cypher into SQL through syntax-directed translation, allowing us to leverage existing research on automated reasoning for SQL while obviating the need for reasoning simultaneously over two different data models. We have implemented our approach in a tool called Graphiti and used it to check equivalence between graph and relational queries. Our experiments demonstrate that Graphiti is useful both for verification and refutation and that it can uncover subtle bugs, including those found in Cypher tutorials and academic papers.
@article{paperbot3124,
title = {Graphiti: Bridging Graph and Relational Database Queries},
author = {Yang He and Ruijie Fang and Işıl Dillig and Yuepeng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729319}
}