Time and space complexity of rule-based graph programs

This thesis concerns the time and space efficiency of programs in GP 2, a rule-based graph transformation language that facilitates formal program analysis. Such programs are a sequence of control structures in which rules are called. A rule describes how part of a host graph is changed to another by specifying a subgraph that is to be replaced. We call the process of finding the specified subgraph in the host graph matching, which takes polynomial time in general. In practise however, we often want rule application to take constant time since it likely corresponds to a single step in a classical algorithm. Several case studies show that the time complexity of GP 2 programs can be on the same level as that of their imperative counterparts. We give linear-time programs for connectedness checking, DAG recognition, and topological sorting, as well as an efficient implementation of Boruvka’s algorithm for finding minimum spanning trees. This efficiency is achieved via roots, which are special nodes in rules and graphs that can be accessed in constant time and allow matching to happen locally around them. The given programs also use depth-first search to traverse graphs in linear time instead of iterating over nodes because GP 2 abstracts away from internal graph data structures. In the spirit of formal program analysis, we give a framework in which to describe the time complexity of these efficient programs. This framework is underpinned by a formal semantics that describes program execution in a sequence of steps that do not cover more than one rule application. On the topic of space efficiency, we give a theoretical result that shows GP 2, like some graph-based machine models, can simulate Turing machines using less space and only quadratic time overhead