强规范化高阶关系查询
Strongly-Normalizing Higher-Order Relational Queries
AI总结：
本文解决了高阶关系查询到SQL翻译中重写系统强规范化证明缺失的问题，通过扩展Lindley和Stark的$\ op\ op$-提升方法以处理复制性重写，并推广至混合集合与多重集合语义的异构查询演算。
摘要：
语言集成查询是一种强大的编程构造，允许数据库查询与普通程序代码无缝且安全地互操作。语言集成查询技术依赖于关于嵌套关系演算的经典结果，该结果指出，只要查询的结果类型是平面关系，就可以通过算法将其翻译为SQL。Cooper等人提倡将高阶嵌套关系演算作为Links和F#等函数式语言中语言集成查询的基础。然而，高阶关系查询到SQL的翻译依赖于一个重写系统，而该系统的强规范化证明尚未发表：先前的证明尝试未能正确处理复制子项的重写规则。本文填补了文献中的这一空白，解释了先前证明尝试的困难所在，并展示了如何扩展Lindley和Stark的$\ op\ op$-提升方法以适应复制性重写。我们还展示了如何将该证明扩展到最近引入的、混合集合语义与多重集合语义的异构查询演算。
英文摘要：
Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about the nested relational calculus, stating that its queries can be algorithmically translated to SQL, as long as their result type is a flat relation. Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However, the translation of higher-order relational queries to SQL relies on a rewrite system for which no strong normalization proof has been published: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the $\top\top$-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also show how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
