一句话：为高阶关系查询到 SQL 的翻译所依赖的重写系统补上强规范化证明，并把证明扩展到集合/多重集合异质查询。
语言集成查询允许数据库查询与普通程序代码安全互操作，其技术依赖嵌套关系演算可被算法翻译为 SQL 的经典结果。高阶嵌套关系演算被用作 Links、F# 等函数式语言中语言集成查询的基础，但把高阶关系查询翻译到 SQL 所依赖的重写系统一直缺少强规范化证明；已有证明尝试未能正确处理复制子项的规则。本文厘清该证明尝试的困难，扩展 Lindley 与 Stark 的 ⊤⊤-lifting 方法以容纳复制型重写，从而给出缺失的强规范化证明，并进一步把证明推广到新近提出的、混合集合与多重集合语义的异质查询演算。
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.