Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications

dc.contributor.author Maria João Frade en
dc.contributor.other 5605 en
dc.date.accessioned 2023-11-15T21:47:15Z
dc.date.available 2023-11-15T21:47:15Z
dc.date.issued 2023 en
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.(c) 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/). en
dc.identifier P-00X-G3D en
dc.identifier.uri https://repositorio.inesctec.pt/handle/123456789/14536
dc.language eng en
dc.rights info:eu-repo/semantics/openAccess en
dc.title Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications en
dc.type en
dc.type Publication en
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
P-00X-G3D.pdf
Size:
465.78 KB
Format:
Adobe Portable Document Format
Description: