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的解压缩方法扩展至最近版本的版本。

0
下载
关闭预览

相关内容

在数学中,多重集是对集的概念的修改,与集不同,集对每个元素允许多个实例。 为每个元素提供的实例的正整数个数称为该元素在多重集中的多重性。 结果存在无限多个多重集,它们仅包含元素a和b,但因元素的多样性而变化:(1)集{a,b}仅包含元素a和b,当将{a,b}视为多集时,每个元素的多重性为1;(2)在多重集{a,a,b}中,元素a具有多重性2,而b具有多重性1;(3)在多集{a,a,a,b,b,b}中,a和b都具有多重性3。
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
生物探索
3+阅读 · 2018年2月10日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年1月19日
Arxiv
0+阅读 · 2021年1月15日
Embedding Logical Queries on Knowledge Graphs
Arxiv
5+阅读 · 2018年9月6日
VIP会员
相关VIP内容
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
生物探索
3+阅读 · 2018年2月10日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员