Skip to Main content Skip to Navigation
Conference papers

A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure

Abstract : We consider a lambda-calculus for which applicative terms have no longer the form (...((u u_1) u_2) ... u_n) but the form (u [u_1 ; ... ; u_n]), for which [u_1 ; ... ; u_n] is a list of terms. While the structure of the usual lambda-calculus is isomorphic to the structure of natural deduction, this new structure is isomorphic to the structure of Gentzen-style sequent calculus. To express the basis of the isomorphism, we consider intuitionistic logic with the implication as sole connective. However we do not consider Gentzen's calculus LJ, but a calculus LJT which leads to restrict the notion of cut-free proofs in LJ. We need also to explicitly consider, in a simply typed version of this lambda-calculus, a substitution operator and a list concatenation operator. By this way, each elementary step of cut-elimination exactly matches with a beta-reduction, a substitution propagation step or a concatenation computation step. Though it is possible to extend the isomorphism to classical logic and to other connectives, we do not treat of it in this paper.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00381525
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 5, 2009 - 4:39:36 PM
Last modification on : Wednesday, December 9, 2020 - 3:10:46 PM
Long-term archiving on: : Thursday, June 10, 2010 - 10:46:37 PM

Files

csl-Her94-lambda-bar.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00381525, version 1

Citation

Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure. Computer Science Logic, Sep 1994, Kazimierz, Poland. pp.61--75. ⟨inria-00381525⟩

Share

Metrics

Record views

409

Files downloads

1243