论文标题
重新审视的爆炸演算
The Bang Calculus Revisited
论文作者
论文摘要
呼叫式呼叫值（CBPV）是一种编程范式，涵盖了Callby-Name（CBN）和Call-by-by-value（CBV）语义。该范式的本质由连接CBPV和线性逻辑的（简洁的）术语语言捕获。 本文介绍了一个被重新访问的爆炸微积分，称为$λ！$，享受了原始配方中缺少的一些重要属性。实际上，新的演算将置换性转换集成到解体值重复的同时，同时汇合。第二个贡献与非军事类型有关。我们为我们的$λ！$ - 微积分提供了定量类型系统，我们表明（弱）缩小键入的长度为其正常形式，加上这种正常形式的大小，其类型派生的大小限制。我们还探讨了此类型系统的属性，相对于CBN/CBV翻译。我们将原始的CBN翻译从$λ$ -Calculus到Bang cyculus，它保留了正常形式，并且相对于CBN的（定量）类型系统是合理且完整的。但是，在CBV的情况下，我们同时重新制定了恢复两个主要特性的翻译和类型系统：保存正常形式和完整性。最后但并非最不重要的一点是，定量系统被完善到一个紧密的系统，这将先前的上限在还原到正常形式的长度上，加上其大小为它们的两个独立的精确度量。
Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Callby-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a (concise) term language connecting CBPV and Linear Logic. This paper presents a revisited version of the Bang Calculus, called $λ!$, enjoying some important properties missing in the original formulation. Indeed, the new calculus integrates permutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to nonidempotent types. We provide a quantitative type system for our $λ!$-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form 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 $λ$-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 tight one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent exact measures for them.
