Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/20939
Título: | Towards a canonical classical natural deduction system |
Autor(es): | Espírito Santo, José |
Palavras-chave: | Classical logic Sequent calculus Natural deduction Control operators Let-expressions Eta-reduction |
Data: | 2013 |
Editora: | Elsevier 1 |
Revista: | Annals of Pure and Applied Logic |
Resumo(s): | 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. |
Tipo: | Artigo |
Descrição: | Preprint submitted to Elsevier, 6 July 2012 |
URI: | https://hdl.handle.net/1822/20939 |
DOI: | 10.1016/j.apal.2012.05.008 |
ISSN: | 0168-0072 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
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 |