The algebraic $\lambda$-calculus is an extension of the ordinary $\lambda$-calculus with linear combinations of terms. We establish that two ordinary $\lambda$-terms are equivalent in the algebraic $\lambda$-calculus iff they are $\beta$-equal. Although this result was originally stated in the early 2000's (in the setting of Ehrhard and Regnier's differential $\lambda$-calculus), the previously proposed proofs were wrong: we explain why previous approaches failed and develop a new proof technique to establish conservativity.


翻译:代数$λ$-演算是普通$λ$-演算的保守扩展 翻译摘要: 代数$λ$-演算是普通$λ$-演算的扩展,其中包含术语的线性组合。我们证明,在代数$λ$-演算中,两个普通$λ$-术语是等价的,当且仅当它们是$\beta$-相等的。虽然这个结论最初在2000年代初期提出(在Ehrhard和Regnier的微分$λ$-演算的背景下),但以前提出的证明是错误的:我们解释为什么以前的方法失败了,并开发了一种新的证明技术来确立保守性。

0
下载
关闭预览

相关内容

专知会员服务
53+阅读 · 2020年10月11日
专知会员服务
61+阅读 · 2020年3月4日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
150+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
25+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
AI界的State of the Art都在这里了
机器之心
12+阅读 · 2018年12月10日
相关性≠因果:概率图模型和do-calculus
论智
31+阅读 · 2018年10月29日
机器之心最干的文章:机器学习中的矩阵、向量求导
深度学习世界
12+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】图像分类必读开创性论文汇总
机器学习研究会
14+阅读 · 2017年8月15日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年6月16日
Arxiv
0+阅读 · 2023年6月15日
Arxiv
16+阅读 · 2022年5月17日
VIP会员
相关VIP内容
专知会员服务
53+阅读 · 2020年10月11日
专知会员服务
61+阅读 · 2020年3月4日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
150+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
25+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
AI界的State of the Art都在这里了
机器之心
12+阅读 · 2018年12月10日
相关性≠因果:概率图模型和do-calculus
论智
31+阅读 · 2018年10月29日
机器之心最干的文章:机器学习中的矩阵、向量求导
深度学习世界
12+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】图像分类必读开创性论文汇总
机器学习研究会
14+阅读 · 2017年8月15日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员