A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure - Université Pierre et Marie Curie Accéder directement au contenu
Communication Dans Un Congrès Année : 1994

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

Résumé

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.
Fichier principal
Vignette du fichier
csl-Her94-lambda-bar.pdf (203.75 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00381525 , version 1 (05-05-2009)

Identifiants

  • HAL Id : inria-00381525 , version 1

Citer

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⟩
495 Consultations
1253 Téléchargements

Partager

Gmail Facebook X LinkedIn More