Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The paradigm was recently modelled by means of the Bang Calculus, a term language connecting CBPV and Linear Logic. This paper presents a revisited version of the Bang Calculus, called $\lambda !$, enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to non-idempotent types. We provide a quantitative type system for our $\lambda !$-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form \emph{plus} the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from $\lambda$-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a \emph{tight} one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent \emph{exact} measures for them.


翻译:callby- Push- Value (CBPV) 是一个包含 Call- by- Name (CBN) 和 Call- Value (CBV) 语义的编程范式。 这个范式最近由Bang Calculus(一个连接 CBPV 和 Linear 逻辑的术语语言) 来模拟。 本文展示了一个重现版的 Bang Calculus, 名为$\ lumbda $ 。 具有在原始系统中缺失的一些重要属性。 事实上, 新的微积分将通缩转换成解盘值的值 值 。 第二种贡献与非功能性格类型的类型有关。 我们为我们的 $\ lambda 提供了一种定量类型系统, 将一个类型缩放到正常的 \ emphevph{plus 。 此格式的大小与其类型排序有关, 我们还在 CBNB/ CBV 翻译中探索了这个类型系统的属性, 将CBN 和 Cal- blus 格式的原始格式转换为 Cal- cal- cal 。

0
下载
关闭预览

相关内容

【干货书】机器人元素Elements of Robotics ,311页pdf
专知会员服务
34+阅读 · 2021年4月16日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
Twitter大佬在线讲座:GNN through the Lens of Curvature
图与推荐
1+阅读 · 2022年4月12日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
Call for Nominations: 2022 Multimedia Prize Paper Award
CCF多媒体专委会
0+阅读 · 2022年2月12日
【ICIG2021】Latest News & Announcements of the Industry Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年7月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2016年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2022年4月20日
Arxiv
1+阅读 · 2022年4月19日
Arxiv
0+阅读 · 2022年4月18日
Arxiv
0+阅读 · 2022年4月16日
Convergence of the Discrete Minimum Energy Path
Arxiv
0+阅读 · 2022年4月15日
Arxiv
14+阅读 · 2020年12月17日
VIP会员
相关VIP内容
【干货书】机器人元素Elements of Robotics ,311页pdf
专知会员服务
34+阅读 · 2021年4月16日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
Twitter大佬在线讲座:GNN through the Lens of Curvature
图与推荐
1+阅读 · 2022年4月12日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
Call for Nominations: 2022 Multimedia Prize Paper Award
CCF多媒体专委会
0+阅读 · 2022年2月12日
【ICIG2021】Latest News & Announcements of the Industry Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年7月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
相关基金
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2016年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员