Author(s):
Espírito Santo, José 
Date: 2002
Persistent ID: http://hdl.handle.net/1822/3863
Origin: RepositóriUM - Universidade do Minho
Subject(s): Cut-elimination; Normalisation; $\lambda$-calculus
Document details
An isomorphism between a fragment of sequent calculus and an extension of natur...
Description
Variants of Herbelin's $\lambda$-calculus, here collectively named Herbelin calculi, have proved useful both in foundational studies and as internal languages for the efficient representation of $\lambda$-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 $\lambda$-calculus. However, this understanding is not complete so far. Our previous work showed that $\lambda$ is isomorphic to a Herbelin calculus, here named lambda-P, only admitting cuts that are both left- and right-permuted. In this paper we consider a generalisation lambda-Ph admitting any kind of right-permuted cut. We show that there is a natural deduction system lambda-Nh which conservatively extends $\lambda$ and is isomorphic to lambda-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 $\beta$, lambda-Nh includes a reduction rule that mirrors left permutation of cuts, but without performing any append of lists/spines.
Variants of Herbelin's $\lambda$-calculus, here collectively named Herbelin calculi, have proved useful both in foundational studies and as internal languages for the efficient representation of $\lambda$-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 $\lambda$-calculus. However, this understanding is not complete so far. Our previous work showed that $\lambda$ is isomorphic to a Herbelin calculus, here named lambda-P, only admitting cuts that are both left- and right-permuted. In this paper we consider a generalisation lambda-Ph admitting any kind of right-permuted cut. We show that there is a natural deduction system lambda-Nh which conservatively extends $\lambda$ and is isomorphic to lambda-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 $\beta$, lambda-Nh includes a reduction rule that mirrors left permutation of cuts, but without performing any append of lists/spines.
Document Type
Conference Object
Language English
Language English
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||