This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by Accattoli and Kesner's linear substitution calculus (LSC). One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, that is the key ingredient for the study of reasonable time cost models for the $\lambda$-calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial cost model for cut elimination with unconstrained exponentials. For the ESC, we also prove untyped confluence and typed strong normalization, showing that it is an alternative to proof nets for an advanced study of cut elimination.


翻译:本文介绍了指数替代微积分(ESC),这是根据证据条款和指数可被视为明显替代的概念,对IMELL的削减去除的一个新表述。这个想法本身不是新的,但在这里它被推到了一个新的水平,受Accattoli和Kesner的线性替代微积分(LSC)的启发。 LSC的关键特性之一是它自然地模拟抽象机器的子术语属性,这是研究美元/升巴元计算的合理时间成本模型的关键成分。新的 ESC随后被用来设计一个与子术语属性的削减消除战略,为用未受限制的指数进行切除提供了第一个多元成本模型。对于 ESC,我们也证明了非型的组合和键入的强烈正常化,表明它是用于高级削减研究的验证网的替代。

0
下载
关闭预览

相关内容

机器学习组合优化
专知会员服务
108+阅读 · 2021年2月16日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
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日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年3月23日
Arxiv
0+阅读 · 2023年3月21日
Arxiv
0+阅读 · 2023年3月21日
Arxiv
14+阅读 · 2020年12月17日
VIP会员
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
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日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员