{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:18:11Z","timestamp":1712369891267},"reference-count":66,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T00:00:00Z","timestamp":1477267200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,2]]},"abstract":"<jats:p>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<jats:italic>et al<\/jats:italic>. 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.<\/jats:p><jats:p>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 \u2018structural recursion on graphs\u2019 using our categorical semantics. We show a concrete model of UnCAL given by the \u03bbG-calculus, which shows an interesting connection to lazy functional programming.<\/jats:p>","DOI":"10.1017\/s096012951600027x","type":"journal-article","created":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T07:47:22Z","timestamp":1477295242000},"page":"287-337","source":"Crossref","is-referenced-by-count":1,"title":["The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics"],"prefix":"10.1017","volume":"28","author":[{"given":"MAKOTO","family":"HAMANA","sequence":"first","affiliation":[]},{"given":"KAZUTAKA","family":"MATSUDA","sequence":"additional","affiliation":[]},{"given":"KAZUYUKI","family":"ASADA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,10,24]]},"reference":[{"key":"S096012951600027X_ref62","unstructured":"Sewell P.M. (1995). The Algebra of Finite State Processes, Ph.D. thesis, University of Edinburgh. Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328."},{"key":"S096012951600027X_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"S096012951600027X_ref8","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2003020"},{"key":"S096012951600027X_ref22","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2746"},{"key":"S096012951600027X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00728-4"},{"key":"S096012951600027X_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90023-0"},{"key":"S096012951600027X_ref39","unstructured":"Hidaka S. , Hu Z. , Inaba K. , Kato H. , Matsuda K. , Nakano K. and Sasano I. (2011). Marker-directed optimization of UnCAL graph transformations. In: Proceedings of LOPSTR'11 123\u2013138."},{"key":"S096012951600027X_ref64","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(1:13)2011"},{"key":"S096012951600027X_ref38","doi-asserted-by":"crossref","unstructured":"Hidaka S. , Hu Z. , Inaba K. , Kato H. , Matsuda K. and Nakano K. (2010). Bidirectionalizing graph transformations. In: Proceedings of ICFP 2010 205\u2013216.","DOI":"10.1145\/1863543.1863573"},{"key":"S096012951600027X_ref24","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.2.271"},{"key":"S096012951600027X_ref19","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008647417502"},{"key":"S096012951600027X_ref15","doi-asserted-by":"crossref","unstructured":"Buneman P. , Davidson S. , Hillebrand G. and Suciu D. (1996). A query language and optimization techniques for unstructured data. In: Proceedings of ACM-SIGMOD'96 505\u2013516.","DOI":"10.1145\/233269.233368"},{"key":"S096012951600027X_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004743"},{"key":"S096012951600027X_ref51","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S096012951600027X_ref31","unstructured":"Hamana M. (2012). Correct looping arrows from cyclic terms: Traced categorical interpretation in Haskell. In: Proceedings of FLOPS'12. Lecture Notes in Computer Science, 7294 136\u2013150."},{"key":"S096012951600027X_ref28","unstructured":"Gibbons J. (1995). An initial-algebra approach to directed acyclic graphs. In: MPC'95 282\u2013303."},{"key":"S096012951600027X_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"S096012951600027X_ref18","unstructured":"Coquand T. (1992). Pattern matching with dependent types. In: Proceedings of the 3rd Work. on Types for Proofs and Programs 66\u201379."},{"key":"S096012951600027X_ref13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1001"},{"key":"S096012951600027X_ref14","unstructured":"Buneman P. (2015). Database and programming: Two subjects divided by a common language? (invited talk). In: POPL'15 487\u2013487."},{"key":"S096012951600027X_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00347-9"},{"key":"S096012951600027X_ref6","doi-asserted-by":"crossref","unstructured":"Asada K. , Hidaka S. , Kato H. , Hu Z. and Nakano K. (2013). A parameterized graph transformation calculus for finite graphs with monadic branches. In: Proceedings of PPDP '13 73\u201384.","DOI":"10.1145\/2505879.2505903"},{"key":"S096012951600027X_ref25","doi-asserted-by":"crossref","unstructured":"Fiore M.P. and Campos M.D. (2013). The algebra of directed acyclic graphs. In: Coecke B. , Ong L. and Panangaden P. (eds.) Computation, Logic, Games, and Quantum Foundations. Lecture Notes in Computer Science 7860, 37\u201351.","DOI":"10.1007\/978-3-642-38164-5_4"},{"key":"S096012951600027X_ref11","volume-title":"Iteration Theories - The Equational Logic of Iterative Processes","author":"Bloom","year":"1993"},{"key":"S096012951600027X_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"S096012951600027X_ref42","unstructured":"Klop J. (1980). Combinatory Reduction Systems, Ph.D. thesis, CWI, Amsterdam. volume 127 of Mathematical Centre Tracts."},{"key":"S096012951600027X_ref21","first-page":"65","article-title":"Axiomatizing iteration categories","volume":"14","author":"\u00c9sik","year":"1999","journal-title":"Acta Cybernetica"},{"key":"S096012951600027X_ref65","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel","year":"1993"},{"key":"S096012951600027X_ref57","doi-asserted-by":"crossref","unstructured":"Nishimura S. , Ohori A. and Tajima K. (1996). An equational object-oriented data model and its data-parallel query language. In: Proceedings of ACM SIGPLAN Object-Oriented Programming Systems, Languages & Applications (OOPSLA'96) 1\u201317.","DOI":"10.1145\/236337.236339"},{"key":"S096012951600027X_ref23","unstructured":"\u00c9sik Z. (2000). Axiomatizing the least fixed point operation and binary supremum. In: Proceedings of Computer Science Logic 2000. Lecture Notes in Computer Science, 1862 302\u2013316."},{"key":"S096012951600027X_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/10721975_4"},{"key":"S096012951600027X_ref55","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990219"},{"key":"S096012951600027X_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.07.003"},{"key":"S096012951600027X_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211391"},{"key":"S096012951600027X_ref66","doi-asserted-by":"crossref","unstructured":"Yu Y. , Lin Y. , Hu Z. , Hidaka S. , Kato H. and Montrieux L. (2012). Maintaining invariant traceability through bidirectional transformations. In: Proceedings of International Conference on Software Engineering, ICSE 2012 540\u2013550.","DOI":"10.1109\/ICSE.2012.6227162"},{"key":"S096012951600027X_ref40","doi-asserted-by":"publisher","DOI":"10.1137\/0216051"},{"key":"S096012951600027X_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504"},{"key":"S096012951600027X_ref1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky","year":"1994"},{"key":"S096012951600027X_ref63","doi-asserted-by":"crossref","unstructured":"Simpson A.K. and Plotkin G.D. (2000). Complete axioms for categorical fixed-point operators. In: Proceedings of LICS'00 30\u201341.","DOI":"10.1109\/LICS.2000.855753"},{"key":"S096012951600027X_ref58","doi-asserted-by":"crossref","unstructured":"Paterson R. (2001). A new notation for arrows. In: Proceedings of ICFP'07 229\u2013240.","DOI":"10.1145\/507635.507664"},{"key":"S096012951600027X_ref12","doi-asserted-by":"crossref","unstructured":"Bloom S.L. and \u00c9sik Z. (1994). Solving polynomial fixed point equations. In: Proceedings of MFCS'94. Lecture Notes in Computer Science, 841, 52\u201367.","DOI":"10.1007\/3-540-58338-6_58"},{"key":"S096012951600027X_ref59","unstructured":"Plotkin G. (2012). An algebraic view of bigraphs. A talk at Milner Symposium 2012, University of Edinburgh."},{"key":"S096012951600027X_ref56","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003457"},{"key":"S096012951600027X_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050067"},{"key":"S096012951600027X_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014548"},{"key":"S096012951600027X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s007780050084"},{"key":"S096012951600027X_ref47","volume-title":"Categories for the Working Mathematician","author":"MacAAAALane","year":"1971"},{"key":"S096012951600027X_ref20","volume-title":"Categories for Types","author":"Crole","year":"1993"},{"key":"S096012951600027X_ref46","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1965-11234-4"},{"key":"S096012951600027X_ref32","doi-asserted-by":"crossref","unstructured":"Hamana M. (2015). Iteration algebras for UnQL graphs and completeness for bisimulation. In: Proceedings of Fixed Points in Computer Science (FICS'15). Electronic Proceedings in Theoretical Computer Science, 191 75\u201389.","DOI":"10.4204\/EPTCS.191.8"},{"key":"S096012951600027X_ref37","doi-asserted-by":"publisher","DOI":"10.2201\/NiiPi.2013.10.7"},{"key":"S096012951600027X_ref34","doi-asserted-by":"crossref","unstructured":"Hasegawa M. (1997a). Models of Sharing Graphs: A Categorical Semantics of let and letrec , Ph.D. thesis, University of Edinburgh. Distinguished Dissertation Series, Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0865-8"},{"key":"S096012951600027X_ref36","doi-asserted-by":"crossref","unstructured":"Hidaka S. , Asada K. , Hu Z. , Kato H. and Nakano K. (2013a). Structural recursion for querying ordered graphs. In: Proceedings of ACM SIGPLAN ICFP'13, 305\u2013318.","DOI":"10.1145\/2500365.2500608"},{"key":"S096012951600027X_ref45","doi-asserted-by":"crossref","unstructured":"Launchbury J. (1993). A natural semantics for lazy evaluation. In: Proceedings of POPL'93 144\u2013154.","DOI":"10.1145\/158511.158618"},{"key":"S096012951600027X_ref16","doi-asserted-by":"crossref","unstructured":"Buneman P. , Davidson S.B. , Fernandez M.F. and Suciu D. (1997). Adding structure to unstructured data. In: Proceedings of ICDT '97 336\u2013350.","DOI":"10.1007\/3-540-62222-5_55"},{"key":"S096012951600027X_ref60","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"S096012951600027X_ref44","volume-title":"Introduction to Higher Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"S096012951600027X_ref35","doi-asserted-by":"crossref","unstructured":"Hasegawa M. (1997b). Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. In: Proceedings of TLCA'97 196\u2013213.","DOI":"10.1007\/3-540-62688-3_37"},{"key":"S096012951600027X_ref5","doi-asserted-by":"crossref","first-page":"207","DOI":"10.3233\/FI-1996-263401","article-title":"Equational term graph rewriting","volume":"26","author":"Ariola","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"S096012951600027X_ref30","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:15)2010"},{"key":"S096012951600027X_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000189"},{"key":"S096012951600027X_ref53","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004809"},{"key":"S096012951600027X_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S096012951600027X_ref33","unstructured":"Hamana M. (2016). Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories. In: Proceedings of Formal Structures for Computation and Deduction (FSCD'16), Leibniz International Proceedings in Informatics (LIPIcs), 52 1\u201318."},{"key":"S096012951600027X_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18508-9_24"},{"key":"S096012951600027X_ref48","unstructured":"Matsuda K. and Asada K. (2015). Graph transformation as graph reduction: A functional reformulation of graph-transformation language UnCAL. Technical Report GRACE-TR 2015-01, National Institute of Informatics. Available at http:\/\/grace-center.jp\/rsc_tr-html"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951600027X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,26]],"date-time":"2020-09-26T21:56:19Z","timestamp":1601157379000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951600027X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,24]]},"references-count":66,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["S096012951600027X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951600027x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,24]]}}}