TY - GEN

T1 - A parameterized graph transformation calculus for finite graphs with monadic branches

AU - Asada, Kazuyuki

AU - Hidaka, Soichiro

AU - Kato, Hiroyuki

AU - Hu, Zhenjiang

AU - Nakano, Keisuke

PY - 2013

Y1 - 2013

N2 - We introduce a lambda calculus λFGT for transformations of finite graphs by generalizing and extending an existing calculus UnCAL. Whereas UnCAL can treat only unordered graphs, λFGT can treat a variety of graph models: directed edge-labeled graphs whose branch styles are represented by monads T. For example, λFGT 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 λFGT, 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 λFGT 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.

AB - We introduce a lambda calculus λFGT for transformations of finite graphs by generalizing and extending an existing calculus UnCAL. Whereas UnCAL can treat only unordered graphs, λFGT can treat a variety of graph models: directed edge-labeled graphs whose branch styles are represented by monads T. For example, λFGT 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 λFGT, 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 λFGT 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.

KW - bisimilarity

KW - epsilon edge

KW - graph algebra

KW - graph transformation

KW - monad

KW - structural recursion

UR - http://www.scopus.com/inward/record.url?scp=84885228051&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84885228051&partnerID=8YFLogxK

U2 - 10.1145/2505879.2505903

DO - 10.1145/2505879.2505903

M3 - Conference contribution

AN - SCOPUS:84885228051

SN - 9781450321549

T3 - Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013

SP - 73

EP - 84

BT - Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013

T2 - 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013

Y2 - 16 September 2013 through 18 September 2013

ER -