高阶关系查询的强正规化
摘要：语言集成查询是一种强大的编程结构，允许数据库查询和普通程序代码无缝安全地互操作。语言集成查询技术依赖于关于嵌套关系演算的经典结果，该结果表明只要查询的结果类型是一个扁平关系，就可以将其算法地转换成SQL。Cooper和其他人提倡将高阶嵌套关系演算作为函数式语言（如Links和F#）中语言集成查询的基础。然而，将高阶关系查询转换成SQL依赖于一个重写系统，该系统还没有发表任何关于它的强归约证明：先前的证明尝试没有正确处理重写规则中重复子术语的问题。本文填补了文献中的空白，解释了先前证明尝试的困难，并展示了如何扩展Lindley和Stark的$ op op$-lifting方法以适应重写的复制。我们还展示了如何将证明扩展到最近引入的混合使用集合和多重集语义的异构查询演算中。
作者：Wilmer Ricciotti and James Cheney
论文ID：2011.13451
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22