The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics
The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics
复制标题
递归图变换语言UnCAL的代数：完整公理化和迭代范畴语义
DOI：
10.1017/s096012951600027x
复制
发表时间：
2018
影响因子：
0.5
通讯作者：
K. Matsuda and K. Asada
中科院分区：
文献类型：
--
作者：
M. Hamana;K. Matsuda and K. Asada
本文的目的是利用类型论的范畴语义和不动点，提供一种称为UnCAL的图变换语言的数学基础。大约20年前，Buneman等人在函数元语言UnCAL的基础上开发了一种图数据库查询语言UnQL，用于描述和操作图。最近，函数式编程社区对UnCAL重新产生了兴趣，因为它提供了一种高效的图形转换语言，对各种应用程序（如双向计算）都很有用。为了使UnCAL在进一步的扩展和应用中更加灵活和富有成效，本文使用范畴语义对UnCAL进行了更概念化的理解。本文的主要目的是阐明什么是UnCAL的代数。因此，我们给出了UnCAL的等式公理化和范畴语义，两者都是新的。我们证明了UnCAL的原始双模拟语义的公理化是完全的。此外，我们使用我们的分类语义提供了UnCAL计算机制的清晰特征，称为“图上的结构递归”。我们给出了一个由λ g微积分给出的UnCAL的具体模型，它显示了与惰性函数式编程的有趣联系。
The aim of this paper is to provide mathematical foundations of a graph transformation language, called UnCAL, using categorical semantics of type theory and fixed points. About 20 years ago, Buneman et al. developed a graph database query language UnQL on the top of a functional meta-language UnCAL for describing and manipulating graphs. Recently, the functional programming community has shown renewed interest in UnCAL, because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation.In order to make UnCAL more flexible and fruitful for further extensions and applications, in this paper, we give a more conceptual understanding of UnCAL using categorical semantics. Our general interest of this paper is to clarify what is the algebra of UnCAL. Thus, we give an equational axiomatisation and categorical semantics of UnCAL, both of which are new. We show that the axiomatisation is complete for the original bisimulation semantics of UnCAL. Moreover, we provide a clean characterisation of the computation mechanism of UnCAL called ‘structural recursion on graphs’ using our categorical semantics. We show a concrete model of UnCAL given by the λG-calculus, which shows an interesting connection to lazy functional programming.