A parameterized graph transformation calculus for finite graphs with monadic branches

We introduce a lambda calculus λ_FG^T for transformations of finite graphs by generalizing and extending an existing calculus UnCAL. Whereas UnCAL can treat only unordered graphs, λ_FG^T can treat a variety of graph models: directed edge-labeled graphs whose branch styles are represented by monads T. For example, λ_FG^T can treat unordered graphs, ordered graphs, weighted graphs, probability graphs, and so on, by using the powerset monad, list monad, multiset monad, probability monad, respectively. In λ_FG^T, graphs are considered as extension of tree data structures, i.e. as infinite (regular) trees, so the semantics is given with bisimilarity. A remarkable feature of UnCAL and λ_FG ^T is structural recursion for graphs, which gives a systematic programming basis like that for trees. Despite the non-well-foundedness of graphs, by suitably restricting the structural recursion, UnCAL and λ_FG^T ensures that there is a termination property and that all transformations preserve the finiteness of the graphs. The structural recursion is defined in a "divide-and-aggregate" way; "aggregation" is done by connecting graphs with ε-edges, which are similar to the -transitions of automata. We give a suitable general definition of bisimilarity, taking account of ε-edges; then we show that the structural recursion is well defined with respect to the bisimilarity.