Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11174
Título: | The lambda-calculus and the unity of structural proof theory |
Autor(es): | Espírito Santo, José |
Data: | 5-Fev-2009 |
Editora: | Springer |
Revista: | Theory of Computing Systems |
Citação: | "Theory of Computing Systems". ISSN 1432-4350. 45 (Febr. 2009) 963-994. |
Resumo(s): | In the context of intuitionistic implicational logic, we achieve a perfect correspondence (technically an isomorphism) between sequent calculus and natural deduction, based on perfect correspondences between left-introduction and elimination, cut and substitution, and cut-elimination and normalisation. This requires an enlarged system of natural deduction that refines von Plato's calculus. It is a calculus with modus ponens and primitive substitution; it is also a ``coercion calculus'', in the sense of Cervesato and Pfenning. Both sequent calculus and natural deduction are presented as typing systems for appropriate extensions of the $\lambda$-calculus. The whole difference between the two calculi is reduced to the associativity of applicative terms (sequent calculus = right associative, natural deduction = left associative), and in fact the achieved isomorphism may be described as the mere inversion of that associativity. The novel natural deduction system is a ``multiary'' calculus, because ``applicative terms'' may exhibit a list of several arguments. But the combination of ``multiarity'' and left-associativity seems simply wrong, leading necessarily to non-local reduction rules (reason: nomalisation, like cut-elimination, acts at the head of applicative terms, but natural deduction focuses at the tail of such terms). A solution is to extend natural deduction even further to a calculus that unifies sequent calculus and natural deduction, based on the unification of cut and substitution. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/11174 |
DOI: | 10.1007/s00224-009-9183-9 |
ISSN: | 1432-4350 |
Versão da editora: | www.springerlink.com |
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 | |
---|---|---|---|---|
LambdaUnity(update2).pdf | 298,24 kB | Adobe PDF | Ver/Abrir |