TY - JOUR

T1 - The algebra of recursive graph transformation language UnCAL

T2 - Complete axiomatisation and iteration categorical semantics

AU - Hamana, Makoto

AU - Matsuda, Kazutaka

AU - Asada, Kazuyuki

N1 - Funding Information:
We are grateful to Zhenjiang Hu and the members of the Bidirectional Graph Transformation Project at NII for various discussions on topics related to UnQL/UnCAL. We also acknowledge the stimulated discussion in the meeting of the Cooperative Research Project 'Logical Approach to Metaprogramming' (2013-2015) at RIEC, Tohoku University. We are especially grateful to Atsusi Ohori for his comments on relevance to object-oriented database. This work was supported in part by JSPS KAKENHI Grant Number 24300001 and 25540002 (Hamana), 15K15966 (Matsuda), 23220001, and 15H05706 (Asada).
Publisher Copyright:
© Copyright Cambridge University Press 2016.

PY - 2018/2/1

Y1 - 2018/2/1

N2 - 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.

AB - 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.

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

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

U2 - 10.1017/S096012951600027X

DO - 10.1017/S096012951600027X

M3 - Article

AN - SCOPUS:84992035010

VL - 28

SP - 287

EP - 337

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 2

ER -