递归图变换语言UnCAL的代数：完全公理化与迭代范畴语义
计算机科学中的逻辑
2016-09-13 v2 数据库
摘要
本文旨在利用类型论和不动点的范畴语义，为图变换语言UnCAL提供数学基础。大约二十年前，Buneman等人开发了一种图数据库查询语言UnQL，其构建于函数式元语言UnCAL之上，用于描述和操纵图。最近，函数式编程社区对UnCAL重新产生兴趣，因为它提供了一种高效的图变换语言，可用于各种应用，如双向计算。为了使UnCAL对进一步扩展和应用更灵活且富有成果，本文中我们使用范畴语义给出对UnCAL更概念性的理解。本文的总体兴趣在于阐明UnCAL的代数究竟是什么。因此，我们给出了UnCAL的方程公理化与范畴语义，两者都是新的。我们证明了该公理化对于UnCAL原始的互模拟语义是完全的。此外，利用我们的范畴语义，我们给出了对UnCAL计算机制（称为“图上的结构递归”）的清晰刻画。我们展示了由 lambdaG-calculus 给出的UnCAL具体模型，这显示了与惰性函数式编程的有趣联系。
引用
@article{arxiv.1511.08851,
title = {The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics},
author = {Makoto Hamana and Kazutaka Matsuda and Kazuyuki Asada},
journal= {arXiv preprint arXiv:1511.08851},
year = {2016}
}
备注
53 pages, to appear in MSCS