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 monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and 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 there is no published proof of the central strong normalization property for higher-order nested relational queries: 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.
翻译:语言整合查询是一个强大的编程结构,允许数据库查询和普通程序代码进行无缝和安全的互操作。语言整合查询技术依赖于蒙亚克理解计算学的古典结果,包括嵌入关系计算学的保守性理论。 保守性意味着查询表达方式可以自由使用嵌套和脱网,但只要查询结果类型是平和的,这些能力不会导致对平坦关系查询的表达性增强。黄方展示了如何通过建设性的重写算法将这类查询翻译成SQL,而库珀和其他人则倡导将高阶嵌入关系计算法作为功能语言整合查询的基础,例如链接和F#。 但是,没有公布证据证明更有序的嵌入式关系查询具有核心的强度正常化属性:以前的举证尝试并不正确处理重复子术语的重写规则。 本文填补了文献中的空白,解释了先前的举证尝试的困难,并展示了如何将Lindley和Stark的解压缩方法扩展至最近版本的版本。