A \(\lambda\)-caclulus structure isomorphic to Gentzen-style sequent calculus structure. (English) Zbl 1044.03509

Pacholski, Leszek (ed.) et al., Computer science logic. 8th workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994. Selected papers. Berlin: Springer-Verlag (ISBN 3-540-60017-5). Lect. Notes Comput. Sci. 933, 61-75 (1995).
Summary: We consider a \(\lambda\)-calculus for which applicative terms have no longer the form \((\dots((u\,u_1)u_2)\dots u_n)\) but the form \((u [u_1;\dots;u_n])\), for which \([u_1;\dots;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 ot 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 it in this paper.
For the entire collection see [Zbl 0847.00048].


03B40 Combinatory logic and lambda calculus
03F50 Metamathematics of constructive systems