重访Bang演算
The Bang Calculus Revisited
AI总结：
本文提出修订版Bang演算$\lambda!$，整合置换转换且保持合流性，构建其定量类型系统并证明归约相关上界，调整CBV翻译与类型系统以恢复范式保持和完备性，还细化出紧系统给出两项精确度量。
摘要：
按推调用（Call-by-Push-Value, CBPV）是一种同时涵盖按名调用（Call-by-Name, CBN）和按值调用（Call-by-Value, CBV）语义的编程范式。该范式的核心由Bang演算刻画，这是一种连接CBPV与线性逻辑的简洁项语言。\n本文提出了Bang演算的一个修订版本，名为$\lambda!$，它具备原始公式所缺失的若干重要性质。具体而言，新演算整合了置换转换以解除值归约式的阻塞，同时保持合流性。第二项贡献与非幂等类型相关。我们为$\lambda!$演算提供了一个定量类型系统，并证明：带类型项到其范式的（弱）归约长度加上该范式的大小，受限于其类型推导的大小。我们还探究了该类型系统相对于CBN/CBV翻译的性质。我们保留了从$\lambda$演算到Bang演算的原始CBN翻译，该翻译保持范式，且相对于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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
