Language-integrated query is a popular and 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 the previous 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,只要其结果类型是平坦的。Cooper 和其他人主张将更高层次的嵌入关系微积分作为语言集成查询的基础,如链接和F#。然而,将较高顺序关系查询转换到 SQL 依赖于一个重写系统,而该系统没有公布强有力的正常化证据:以前的举证尝试没有正确处理重复子术语的重写规则。本文填补了文献中的空白,解释了以往尝试的困难,并展示了如何扩大Lindley 和 Stark 的“$top\top$-lifting” 方法,以容纳重复的重写器等。我们还演示了如何将证据推广到最近推出的用于混合查询和多谱拼拼的计算器。