An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction

Abstract

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 λPh admitting any kind of right-permuted cut.

We show that there is a natural deduction system λNh which 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 β, λNh includes a reduction rule that mirrors left permutation of cuts, but without performing any append of lists/spines.