Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/87622
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Frade, M. J. | por |
dc.contributor.author | Pinto, Luís F. | por |
dc.date.accessioned | 2023-12-20T11:45:57Z | - |
dc.date.available | 2024-02-01T07:00:38Z | - |
dc.date.issued | 2023 | - |
dc.identifier.citation | Espírito Santo, J., Frade, M. J., & Pinto, L. (2023, February). Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. Journal of Logical and Algebraic Methods in Programming. Elsevier BV. http://doi.org/10.1016/j.jlamp.2022.100830 | - |
dc.identifier.issn | 2352-2208 | por |
dc.identifier.uri | https://hdl.handle.net/1822/87622 | - |
dc.description.abstract | In the context of intuitionistic sequent calculus, “naturality” means permutation-freeness (the terminology is essentially due to Mints). We study naturality in the context of the lambda-calculus with generalized applications and its multiary extension, to cover, under the Curry-Howard correspondence, proof systems ranging from natural deduction (with and without general elimination rules) to a fragment of sequent calculus with an iterable left-introduction rule, and which can still be recognized as a call-by-name lambda-calculus. In this context, naturality consists of a certain restricted use of generalized applications. We consider the further restriction obtained by the combination of naturality with normality w.r.t. the commutative conversion engendered by generalized applications. This combination sheds light on the interpretation of naturality as a vectorization mechanism, allowing a multitude of different ways of structuring lambda-terms, and the structuring of a multitude of interesting fragments of the systems under study. We also consider a relaxation of naturality, called weak naturality: this not only brings similar structural benefits, but also suggests a new “weak” system of natural deduction with generalized applications which is exempt from commutative conversions. In the end, we use all of this evidence as a stepping stone to propose a computational interpretation of generalized application (whether multiary or not, and without any restriction): it includes, alongside the argument(s) for the function, a general list – a new, very general, vectorization mechanism, that structures the continuation of the computation. | por |
dc.description.sponsorship | The authors were financed by Portuguese Funds through FCT (Fundação para a Ciência e Tecnologia) within the projects UIDB/00013/2020, UIDP/00013/2020 and UIDB/50014/2020. | por |
dc.language.iso | eng | por |
dc.publisher | Elsevier 1 | por |
dc.relation | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00013%2F2020/PT | por |
dc.relation | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDP%2F00013%2F2020/PT | por |
dc.relation | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F50014%2F2020/PT | por |
dc.rights | openAccess | por |
dc.subject | Commutative conversion | por |
dc.subject | Natural deduction | por |
dc.subject | Normal and natural proofs | por |
dc.subject | Permutative conversion | por |
dc.subject | Sequent calculus | por |
dc.subject | Vector notation | por |
dc.title | Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications | por |
dc.type | article | - |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://doi.org/10.1016/j.jlamp.2022.100830 | por |
oaire.citationVolume | 131 | por |
dc.date.updated | 2023-12-19T15:12:19Z | - |
dc.identifier.eissn | 2352-2216 | por |
dc.identifier.doi | 10.1016/j.jlamp.2022.100830 | por |
dc.subject.wos | Science & Technology | - |
sdum.export.identifier | 12948 | - |
sdum.journal | Journal of Logical and Algebraic Methods in Programming | por |
dc.identifier.articlenumber | 100830 | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals HASLab - Artigos em revistas internacionais |