基于正则Datalog的认证图视图维护
数据库
2018-04-30 v1 计算机科学中的逻辑
编程语言
摘要
我们采用Coq证明辅助工具，开发了一个机械认证的框架，用于评估图查询并增量维护物化图实例（亦称视图）。我们用于定义查询和视图的语言是正则Datalog（RD）——非递归Datalog的一个显著片段，可表达复杂导航查询，并以传递闭包为原生算子。我们首先设计并编码RD的理论，然后机械化一个RD专用的评估算法，能够进行细粒度、增量的图视图计算，我们证明其相对于声明式RD语义的可靠性。通过使用Coq提取机制，我们在一组初步基准上测试了已验证引擎的Ocaml版本。我们的开发特别侧重于利用现有验证与记号技术以：a) 定义逻辑学家和数据库研究者易理解的机械化性质，以及 b) 以有限代价达成形式验证。我们的工作是迈向动态图查询语言及其评估引擎的统一、机器验证形式框架的第一步。本文正考虑被TPLP接受。
引用
@article{arxiv.1804.10565,
title = {Certified Graph View Maintenance with Regular Datalog},
author = {Angela Bonifati and Stefania Dumbrava and Emilio Jesus Gallego Arias},
journal= {arXiv preprint arXiv:1804.10565},
year = {2018}
}
备注
Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018. 18 pages, LaTeX, (arXiv:YYMM.NNNNN)