Łukasiewicz 逻辑极小片段的 Curry-Howard 对应

在本文中，我们引入了一个项演算 ${\cal B}$，它在带有配对操作的仿射 $\lambda$-演算基础上增加了一种新的构造，允许一种受限的收缩形式。我们建立了 ${\cal B}$ 与一种子结构逻辑系统之间的 Curry-Howard 对应，我们称之为“极小 Łukasiewicz 逻辑”，在文献中也被称为 hoop 逻辑（MV-代数的推广）。该逻辑严格位于仿射极小逻辑与标准极小逻辑之间。我们证明 ${\cal B}$ 是强规范化的且具有 Church-Rosser 性质。我们还给出了 ${\cal B}$ 中对应于我们及文献中一些重要推导的项示例。最后，我们讨论了 ${\cal B}$ 中的规范化与极小 Łukasiewicz 逻辑的 Gentzen 风格表述的割消之间的关联。