Jumbo λ-calculus
Jumbo λ-calculus
复制标题
巨型 λ 演算
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Levy
中科院分区：
文献类型：
--
作者：
P. Levy
我们认为，对于任何涉及发散或延续等计算效应的研究，简单类型的lambda演算的传统语法不能被认为是规范的，因为标准的正则性论点依赖于同构，而同构可能不存在于有效的环境中。为了解决这个问题，我们定义了一个“巨型lambda演算”，它将传统的连接词融合成更一般的连接词，即所谓的“巨型连接词”。我们为我们的论点提供了两个证据，证明巨型公式是有利的
首先，我们证明了巨型Lambda演算提供了一个“完整”的连接词范围，在这个意义上，它包括了在beta-eta理论中具有可逆规则的所有可能的连接词
其次，在存在影响的情况下，我们证明了不存在将巨型连接词分解成既适用于按值调用又适用于按名称调用的非巨型连接词
We make an argument that, for any study involving computational effects such as divergence or continuations, the traditional syntax of simply typed lambda-calculus cannot be regarded as canonical, because standard arguments for canonicity rely on isomorphisms that may not exist in an effectful setting. To remedy this, we define a “jumbo lambda-calculus” that fuses the traditional connectives together into more general ones, so-called “jumbo connectives”. We provide two pieces of evidence for our thesis that the jumbo formulation is advantageous
Firstly, we show that the jumbo lambda-calculus provides a “complete” range of connectives, in the sense of including every possible connective that, within the beta-eta theory, possesses a reversible rule
Secondly, in the presence of effects, we show that there is no decomposition of jumbo connectives into non-jumbo ones that is valid in both call-by-value and call-by-name