A parameterized graph transformation calculus for finite graphs with monadic branches

We introduce a lambda calculus λ T FG for transformations of finite graphs by generalizing and extending an existing calculus UnCAL. Whereas UnCAL can treat only unordered graphs, λ T FG can treat a variety of graph models: directed edge-labeled graphs whose branch styles are represented by monads T . For example, λ T FG 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 λ T FG , 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 λ T FG 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 λ T FG 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 e-edges, which are similar to the e-transitions of automata. We give a suitable general definition of bisimilarity, taking account of e-edges; then we show that the structural recursion is well defined with respect to the bisimilarity.