论文标题
功能性珍珠：分配$λ$ -calculus
Functional Pearl: The Distributive $λ$-Calculus
论文作者
论文摘要
我们介绍了与成对的$λ$ -calculus的简单扩展---称为分配$λ$ -calculus ---通过添加对有效分布的同构$ a \ rightarrow（b \ wedge c）\ \\\\\\\\\\\\\\\\\ equiv equiv equiv \\ \ \ \ \ \ \ \ righterar $ primear的计算解释来获得的计算解释。我们将微积分研究视为一个未型的和简单的打字设置。未型演算的关键特征是汇合，没有构造冲突，即评估永远不会卡住，而最左边的归一化定理是通过直接证明获得的。关于简单类型，我们表明，如果将类型视为分布式同构，则新规则可以减少主题。主要结果是对分布率的简单类型的强范围。证明是对$λ$ -Calculus的平滑变化，具有对和简单的类型。
We introduce a simple extension of the $λ$-calculus with pairs---called the distributive $λ$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A \Rightarrow (B\wedge C)\ \ \equiv\ \ (A\Rightarrow B) \wedge (A\Rightarrow C)$ of simple types. We study the calculus both as an untyped and as a simply typed setting. Key features of the untyped calculus are confluence, the absence of clashes of constructs, that is, evaluation never gets stuck, and a leftmost-outermost normalization theorem, obtained with straightforward proofs. With respect to simple types, we show that the new rules satisfy subject reduction if types are considered up to the distributivity isomorphism. The main result is strong normalization for simple types up to distributivity. The proof is a smooth variation over the one for the $λ$-calculus with pairs and simple types.
