Loading...
Please wait, while we are loading the content...
Similar Documents
Lambda terms for natural deduction, sequent calculus and cut elimination
| Content Provider | Scilit |
|---|---|
| Author | Barendregt, Henk Ghilezan, Silvia |
| Copyright Year | 2000 |
| Description | 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 $(λL^{cf}$). 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. |
| Related Links | http://pdfs.semanticscholar.org/da8a/c9652cf1f6098125c28c8a94a3dafbc92317.pdf https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C94BB5ECFC2E2B3F3EF4F8920A2840BC/S0956796899003524a.pdf/div-class-title-lambda-terms-for-natural-deduction-sequent-calculus-and-cut-elimination-div.pdf |
| Ending Page | 134 |
| Page Count | 14 |
| Starting Page | 121 |
| ISSN | 09567968 |
| e-ISSN | 14697653 |
| DOI | 10.1017/s0956796899003524 |
| Journal | Journal of Functional Programming |
| Issue Number | 1 |
| Volume Number | 10 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | Journal of Functional Programming History and Philosophy of Science Cut Elimination one Correspondence Natural Deduction Derivation Extensionally Equivalent Type Assignment Terms Corresponds Normal Form Untyped Lambda Term Typeable Lambda Term Equivalent Sequent Calculus Derivation Lambda Term Natural Deduction Sequent Calculus |
| Content Type | Text |
| Resource Type | Article |
| Subject | Software |
