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.
Type de document :
Communication dans un congrès
Leszek Pacholski and Jerzy Tiuryn. Computer Science Logic, Sep 1994, Kazimierz, Poland. 933, pp.61--75, 1994, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00381525
Contributeur : Hugo Herbelin <>
Soumis le : mardi 5 mai 2009 - 16:39:36
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : jeudi 10 juin 2010 - 22:46:37

Fichiers

csl-Her94-lambda-bar.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00381525, version 1

Collections

Citation

Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure. Leszek Pacholski and Jerzy Tiuryn. Computer Science Logic, Sep 1994, Kazimierz, Poland. 933, pp.61--75, 1994, Lecture Notes in Computer Science. 〈inria-00381525〉

Partager

Métriques

Consultations de la notice

310

Téléchargements de fichiers

503