AI 中文总结
MGQL是首个基于ISO/IEC 39075标准的GQL机械化小步操作语义，解决了现有形式化方法的不足，为GQL规范与机械化实现搭建桥梁，可对查询正确性进行形式化推理。
AI 中文摘要
ISO图形查询语言（GQL）是首个基于属性图的图查询语言国际标准，于2024年被标准化为ISO/IEC 39075。然而，ISO/IEC 39075在600多页的散文中非正式地规定了其语义，这使得难以对该标准进行形式化推理，也难以实现符合标准的实现。现有的形式化方法并不充分，因为它们要么：（1）通过省略包语义、模式和多图上的复合查询来大幅降低语义复杂性；（2）或者仅考虑孤立的片段（如模式匹配）来大幅降低句法复杂性，而未将完整的查询管道形式化。正是这些语义-句法特征使得GQL的形式化并非易事。我们提出了MGQL，这是首个基于ISO/IEC 39075标准的、针对GQL重要只读片段的机械化小步操作语义。我们的形式化模型具有混合边方向性的多图属性图，并支持GQL的大部分模式构造：量化路径和边、有向和无向匹配、标签表达式、模式列表以及复合查询。该语义由感知模式的类型系统提供支持，该系统通过闭图模式细化变量类型、跟踪空值性、支持多种复合查询运算符，并通过列表类型对量化路径绑定进行建模。我们证明了我们的类型系统是可靠的，确保格式良好的查询能够产生符合其声明模式的结果的端到端保证。MGQL在GQL的非正式规范与机械化实现之间架起了首座桥梁，能够对正确性进行形式化推理。
英文摘要
ISO Graph Query Language (GQL) is the first international standard for property graph-based graph query languages, standardized as ISO/IEC 39075 in 2024. However, ISO/IEC 39075 codifies its semantics informally across 600+ pages of prose, making it difficult to formally reason about the standard or for a standard-faithful implementation. Existing formalizations are not adequate because they either: (1) significantly reduce the semantic complexity by omitting bag semantics, schemas, and composite queries on multiple graphs; (2) or significantly reduce the syntactic complexity by only considering isolated fragments such as pattern-matching, leaving the full query pipeline unformalized. Yet it is these semantic-syntactic features that make formalizing GQL non-trivial. We present MGQL, the first mechanized, small-step operational semantics for a substantial read-only fragment of GQL that is grounded in the ISO/IEC 39075 standard. Our formalization models multi-graph property graphs with mixed edge directionality and supports a large fraction of GQL pattern constructs: quantified paths and edges, directional and undirected matching, label expressions, pattern lists, and composite queries. The semantics is supported by a schema-aware type system that refines variable types via closed-graph schemas, tracks nullability, supports multiple composite query operators, and models quantified-path bindings with list types. We prove that our type system is sound, ensuring an end-to-end guarantee of well-formed queries yielding results that conform to their declared schemas. MGQL provides the first bridge between GQL's informal specification and a mechanized implementation, enabling formal reasoning about correctness.
CommentsAccepted at OOPSLA 2026
DOI：10.1145/3839459
