Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and a call-by-silly abstract machine implementing the strategy. Moreover, we measure the number of steps taken by the strategy via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.


翻译:λ演算的按需求值可视为融合了按名调用与按值调用的最佳特性,即前者明智的擦除行为与后者明智的复制行为。为深入理解复制与擦除如何结合,我们设计了一个退化演算,称之为按愚蠢调用。该演算与按需求值形成对称关系,它融合了按名调用与按值调用中最糟糕的特性,即按名调用的愚蠢复制与按值调用的愚蠢擦除。通过重写性质与多类型系统,我们验证了按愚蠢调用演算的设计合理性。特别地,我们镜像了关于按需求值的主要定理——即其与按名调用的操作等价性——证明按愚蠢调用与按值调用诱导出相同的上下文等价关系。这一事实揭示了按值调用上下文等价性在效率上的盲目性。我们还定义了按愚蠢调用策略及实现该策略的抽象机。此外,我们通过紧多类型系统度量了该策略所需的步骤数。最后,我们证明按愚蠢调用策略在演算中计算出最大长度的求值序列。

0
下载
关闭预览

相关内容

《大语言模型中的对齐伪造》最新137页
专知会员服务
11+阅读 · 2025年1月27日
机器学习损失函数概述,Loss Functions in Machine Learning
专知会员服务
84+阅读 · 2022年3月19日
关于OKR的反思:OKR是给员工挖坑用的,是变相的KPI?
人人都是产品经理
10+阅读 · 2019年3月5日
Spooftooph - 用于欺骗或克隆蓝牙设备的自动工具
黑白之道
17+阅读 · 2019年2月27日
换个角度看GAN:另一种损失函数
机器之心
16+阅读 · 2019年1月1日
超像素、语义分割、实例分割、全景分割 傻傻分不清?
计算机视觉life
19+阅读 · 2018年11月27日
异常检测的阈值,你怎么选?给你整理好了...
机器学习算法与Python学习
10+阅读 · 2018年9月19日
详解常见的损失函数
七月在线实验室
20+阅读 · 2018年7月12日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Arxiv
0+阅读 · 6月15日
VIP会员
最新内容
ICML 2026 | CFPO:用反事实策略优化提升多模态推理
专知会员服务
1+阅读 · 今天14:45
综述 | 世界动作模型:少做梦,多行动
专知会员服务
1+阅读 · 今天14:43
美以伊冲突:无人机与人工智能的运用
专知会员服务
3+阅读 · 今天14:31
《特种部队在透明战场中的生存力》最新报告
专知会员服务
2+阅读 · 今天14:11
《人工智能生成的零日漏洞:对未来作战的影响》
综述 | 3D场景图:开放挑战与未来方向
专知会员服务
8+阅读 · 6月22日
21世纪的无人机战争
专知会员服务
4+阅读 · 6月22日
《量子技术的军事任务技术适配与利用》
专知会员服务
5+阅读 · 6月22日
相关资讯
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员