An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction
An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction
复制标题
序贯微积分片段与自然演绎推广的同构
DOI：
10.1007/3-540-36078-6_24
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
J. E. Santo
中科院分区：
文献类型：
--
作者：
J. E. Santo
Herbelin的λ-演算的变体，这里统称为Herbelin演算，在基础研究和作为有效表示λ-项的内部语言中都被证明是有用的。这两种应用的一个明显要求是清楚地理解Herbelin演算中的割消元和λ-演算中的正规化之间的关系。然而，这种认识到目前为止还不完全。我们以前的工作表明λ同构于Herbelin演算，这里称为λP，只允许左置换和右置换的割。本文考虑一个广义λ Ph，它允许任何右置换割，证明了存在一个自然演绎系统λ Nh，它保守地扩张I，并且与λPh同构.这个想法是在自然演绎系统中建立应用术语和应用之间的区别，以及头部和尾部应用之间的区别。这是通过检查自然演绎证明如何根据Prawitz的翻译映射到微积分推导而提出的。除了β之外，λ Nh还包括一个简化规则，该规则反映了切割的左置换，但不执行任何列表/刺的附加。
Variants of Herbelin’s λ-calculus, here collectively named Herbelin calculi, have proved useful both in foundational studies and as internal languages for the efficient representation of λ-terms.An obvious requirement of both these two kinds of applications is a clear understanding of the relationship between cut-elimination in Herbelin calculi and normalisation in the λ-calculus. However, this understanding is not complete so far. Our previous work showed that λ is isomorphic to a Herbelin calculus, here named λP,only admitting cuts that are both left- and right-permuted. In this paper we consider a generalisation λPhadmitting any kind of right-permuted cut.We show that there is a natural deduction system λNhwhich conservatively extends I and is isomorphic to λPh. The idea is to build in the natural deduction system a distinction between applicative term and application, together with a distinction between head and tail application. This is suggested by examining how natural deduction proofs are mapped to sequent calculus derivations according to a translation due to Prawitz.In addition to β, λNhincludes a reduction rule that mirrors left permutation of cuts, but without performing any append of lists/spines.