Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11174
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | - |
dc.date.accessioned | 2010-12-03T17:02:22Z | - |
dc.date.available | 2010-12-03T17:02:22Z | - |
dc.date.issued | 2009-02-05 | - |
dc.identifier.citation | "Theory of Computing Systems". ISSN 1432-4350. 45 (Febr. 2009) 963-994. | por |
dc.identifier.issn | 1432-4350 | por |
dc.identifier.uri | https://hdl.handle.net/1822/11174 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | Fundação para a Ciência e Tecnologia (FCT) | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.rights | openAccess | por |
dc.title | The lambda-calculus and the unity of structural proof theory | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | www.springerlink.com | por |
sdum.pagination | 963-994 | por |
sdum.publicationstatus | published | por |
sdum.volume | 45 | por |
oaire.citationStartPage | 963 | por |
oaire.citationEndPage | 994 | por |
oaire.citationIssue | 4 | por |
oaire.citationVolume | 45 | por |
dc.identifier.doi | 10.1007/s00224-009-9183-9 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Theory of Computing Systems | por |
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 |