Iteration Algebras for UnQL Graphs and Completeness for Bisimulation

TL;DR

This paper develops an algebraic semantics for UnCAL graph query language using iteration algebras, proving completeness for bisimulation and providing a clear framework for structural recursion on graphs.

Contribution

It introduces an equational axiomatisation and algebraic semantics for UnCAL graphs, establishing completeness for bisimulation using iteration algebras.

Findings

Proves completeness of axioms for UnCAL bisimulation.

Provides algebraic semantics for UnCAL graphs.

Characterizes structural recursion on graphs algebraically.

Abstract

This paper shows an application of Bloom and Esik's iteration algebras to model graph data in a graph database query language. About twenty years ago, Buneman et al. developed a graph database query language UnQL on the top of a functional meta-language UnCAL for describing and manipulating graphs. Recently, the functional programming community has shown renewed interest in UnCAL, because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation. However, no mathematical semantics of UnQL/UnCAL graphs has been developed. In this paper, we give an equational axiomatisation and algebraic semantics of UnCAL graphs. The main result of this paper is to prove that completeness of our equational axioms for UnCAL for the original bisimulation of UnCAL graphs via iteration algebras. Another benefit of algebraic semantics is a clean characterisation of structural recursion on graphs using free iteration algebra.