Hostname: page-component-7c8c6479df-r7xzm Total loading time: 0 Render date: 2024-03-27T15:37:45.644Z Has data issue: false hasContentIssue false

Lambda terms for natural deduction, sequent calculus and cut elimination

Published online by Cambridge University Press:  01 January 2000

HENK BARENDREGT
Affiliation:
Department of Computer Science, Catholic University, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands (e-mail: henk@cs.kun.nl)
SILVIA GHILEZAN
Affiliation:
Faculty of Engineering, University of Novi Sad, Trg Dositeja Obradovića 6, 21000 Novi Sad, Yugoslavia (e-mail: gsilvia@uns.ns.ac.yu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λN) and the other to sequent calculus (λL). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a ‘cut-free’ fragment (λLcf). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms possess a normal form.

Type
THEORETICAL PEARL
Copyright
© 2000 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.