Confluence Analysis for a Graph Programming Language

GP 2 is a high-level domain-specific language for programming with graphs.
Users write a set of graph transformation rules and organise them with imperative-style control constructs to perform a desired computation on an input graph.
As rule selection and matching are non-deterministic, there might be different graphs resulting from program execution.
Confluence is a property that establishes the global determinism of a computation despite possible local non-determinism.
Conventional confluence analysis is done via so-called critical pairs, which are conflicts in minimal context.
A key challenge is extending critical pairs to the setting of GP 2.

This thesis concerns the development of confluence analysis for GP 2.
First, we extend the notion of conflict to GP 2 rules, and prove that non-conflicting rule applications commute.
Second, we define symbolic critical pairs and establish their properties, namely that there are only finitely many of them and that they represent all possible conflicts.
We give an effective procedure for their construction.
Third, we solve the problem of unifying GP 2 list expressions, which arises during the construction of critical pairs, by giving a unification procedure which terminates with a finite and complete set of unifiers (under certain restrictions).
Last but not least, we specify a confluence analysis algorithm based on symbolic critical pairs, and show its soundness by proving the Local Confluence Theorem.
Several existing programs are analysed for confluence to demonstrate how the analysis handles several GP 2 features at the same time, and to demonstrate the merit of the used techniques.