We present a call-by-need $\lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a $\lambda$-term t admits a normal form n in the $\lambda$-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design. In particular, it led us to derive a new description of call-by-need reduction based on inductive rules.


翻译:我们提出了一种需求调用 $\lambda$-演算,它实现了强规约(即在抽象体内进行规约)并保证了参数仅在需要且最多一次时才会被评估。这种演算使用显式替换并取代了现有的强力需求策略,但允许更多的规约序列,通常更短,同时仍保持所需性。该演算在强熄定(即任何正则 $\lambda$-项非规约等价时)方面被证明是正则的:无论 $\lambda$-项 t 是否在 $\lambda$-演算中具有正则形式 n,演算中从 t 开始的任何规约序列最终都会到达正则形式 n 的代表。我们还展示了该演算的限制,该限制具有菱形特性且仅执行最短的规约序列,这使其比现有策略更有效。我们使用 Abella 证明辅助工具来部分形式化了该演算,并讨论了此实验对其设计的影响。特别是,它使我们推导出一种基于归纳规则的新的需求调用规约描述。

0
下载
关闭预览

相关内容

专知会员服务
50+阅读 · 2020年12月14日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
24+阅读 · 2019年5月18日
【泡泡一分钟】基于运动估计的激光雷达和相机标定方法
泡泡机器人SLAM
25+阅读 · 2019年1月17日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
【推荐】免费书(草稿):数据科学的数学基础
机器学习研究会
19+阅读 · 2017年10月1日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年5月15日
Arxiv
0+阅读 · 2023年5月12日
VIP会员
相关VIP内容
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员