Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/20939
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | - |
dc.date.accessioned | 2012-11-23T16:54:53Z | - |
dc.date.available | 2012-11-23T16:54:53Z | - |
dc.date.issued | 2013 | - |
dc.date.submitted | 2011-04-02 | - |
dc.identifier.issn | 0168-0072 | por |
dc.identifier.uri | https://hdl.handle.net/1822/20939 | - |
dc.description | Preprint submitted to Elsevier, 6 July 2012 | por |
dc.description.abstract | This paper studies a new classical natural deduction system, presented as a typed calculus named lambda-mu- let. It is designed to be isomorphic to Curien and Herbelin's lambda-mu-mu~-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigot's lambda-mu -calculus with the idea of "coercion calculus" due to Cervesato and Pfenning, accommodating let-expressions in a surprising way: they expand Parigot's syntactic class of named terms. This calculus and the mentioned isomorphism Theta offer three missing components of the proof theory of classical logic: a canonical natural deduction system; a robust process of "read-back" of calculi in the sequent calculus format into natural deduction syntax; a formalization of the usual semantics of the lambda-mu-mu~-calculus, that explains co-terms and cuts as, respectively, contexts and hole- filling instructions. lambda-mu-let is not yet another classical calculus, but rather a canonical reflection in natural deduction of the impeccable treatment of classical logic by sequent calculus; and provides the "read-back" map and the formalized semantics, based on the precise notions of context and "hole-expression" provided by lambda-mu-let. We use "read-back" to achieve a precise connection with Parigot's lambda-mu , and to derive lambda-calculi for call-by-value combining control and let-expressions in a logically founded way. Finally, the semantics , when fully developed, can be inverted at each syntactic category. This development gives us license to see sequent calculus as the semantics of natural deduction; and uncovers a new syntactic concept in lambda-mu-mu~ ("co-context"), with which one can give a new de nition of eta-reduction. | por |
dc.language.iso | eng | por |
dc.publisher | Elsevier 1 | por |
dc.rights | openAccess | por |
dc.subject | Classical logic | por |
dc.subject | Sequent calculus | por |
dc.subject | Natural deduction | por |
dc.subject | Control operators | por |
dc.subject | Let-expressions | por |
dc.subject | Eta-reduction | por |
dc.title | Towards a canonical classical natural deduction system | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
sdum.publicationstatus | submitted | por |
oaire.citationStartPage | 618 | por |
oaire.citationEndPage | 650 | por |
oaire.citationIssue | 6 | por |
oaire.citationTitle | Annals of Pure and Applied Logic | por |
oaire.citationVolume | 164 | por |
dc.identifier.doi | 10.1016/j.apal.2012.05.008 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Annals of Pure and Applied Logic | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
TowardsClassicalNatDed.pdf | 375,86 kB | Adobe PDF | Ver/Abrir |