A Rule-based Operational Semantics of Graph Query Languages

TL;DR

This paper introduces a formal, rule-based semantics for a core graph query language, providing a sound and complete calculus for pattern solving adaptable to various graph databases.

Contribution

It defines a graph query algebra, introduces recursive patterns, and develops a generic rewriting calculus for pattern solving with formal semantics.

Findings

The calculus is sound and complete for pattern solving.

It develops only one derivation per pattern, improving efficiency.

The approach is adaptable to different graph database models.

Abstract

We consider a core language of graph queries. These queries are seen as formulas to be solved with respect to graph-oriented databases. For this purpose, we first define a graph query algebra where some operations over graphs and sets of graph homomorphisms are specified. Then, the notion of pattern is introduced to represent a kind of recursively defined formula over graphs. The syntax and formal semantics of patterns are provided. Afterwards, we propose a new sound and complete calculus to solve patterns. This calculus, which is based on a rewriting system, develops only one derivation per pattern to be solved. Our calculus is generic in the sense that it can be adapted to different kinds of graph databases provided that the notions of graph and graph homomorphism (match) are well defined.