×

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. (English) Zbl 07649237

Summary: 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.

MSC:

03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
68N18 Functional programming and lambda calculus

References:

[1] Joachimski, F.; Matthes, R., Standardization and confluence for a lambda calculus with generalized applications, (Proc. of RTA’00. Proc. of RTA’00, Lecture Notes in Computer Science, vol. 1833 (2000), Springer), 141-155 · Zbl 0964.03014
[2] von Plato, J., Natural deduction with general elimination rules, Ann. Math. Log., 40, 7, 541-567 (2001) · Zbl 1021.03050
[3] Dyckhoff, R.; Pinto, L., Permutability of proofs in intuitionistic sequent calculi, Theor. Comput. Sci., 212, 141-155 (1999) · Zbl 0913.68110
[4] Zucker, J., The correspondence between cut-elimination and normalization, Ann. Math. Log., 7, 1-112 (1974) · Zbl 0298.02023
[5] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and Types (1989), Cambridge Univ. Press · Zbl 0671.68002
[6] Mints, G., Normal forms for sequent derivations, (Odifreddi, P., Kreiseliana (1996), A.K. Peters: A.K. Peters Wellesley, Massachusetts), 469-492 · Zbl 0897.03053
[7] Herbelin, H., A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure, (Proc. of CSL’94. Proc. of CSL’94, Lecture Notes in Computer Science, vol. 933 (1995), Springer), 61-75 · Zbl 1044.03509
[8] Santo, J. Espírito, Revisiting the correspondence between cut-elimination and normalisation, (Proceedings of ICALP’2000. Proceedings of ICALP’2000, Lecture Notes in Computer Science, vol. 1853 (2000), Springer-Verlag) · Zbl 0973.03073
[9] Espírito Santo, J.; Pinto, L., Permutative conversions in intuitionistic multiary sequent calculus with cuts, (Hoffman, M., Proc. of TLCA’03. Proc. of TLCA’03, Lecture Notes in Computer Science, vol. 2701 (2003), Springer), 286-300 · Zbl 1041.03040
[10] Espírito Santo, J.; Pinto, L., Confluence and strong normalisation of the generalised multiary λ-calculus, (Revised selected papers from TYPES’03. Revised selected papers from TYPES’03, Lecture Notes in Computer Science, vol. 3085 (2004), Springer), 286-300 · Zbl 1100.03513
[11] Espírito Santo, J.; Frade, M. J.; Pinto, L., Structural proof theory as rewriting, (Proc. of RTA’06. Proc. of RTA’06, Lecture Notes in Computer Science, vol. 4098 (2006), Springer), 197-211 · Zbl 1151.03347
[12] Espírito Santo, J.; Pinto, L., A calculus of multiary sequent terms, ACM Trans. Comput. Log., 12, 3, 22 (2011) · Zbl 1352.03063
[13] Espírito Santo, J.; Frade, M. J.; Pinto, L., Permutability in proof terms for intuitionistic sequent calculus with cuts, (Proc. of TYPES’16. Proc. of TYPES’16, LIPIcs, vol. 97 (2018), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 10:1-10:27
[14] Schwichtenberg, H., Termination of permutative conversions in intuitionistic Gentzen calculi, Theor. Comput. Sci., 212, 1-2, 247-260 (1999) · Zbl 0913.68135
[15] Santo, J. Espírito, The call-by-value lambda-calculus with generalized applications, (Fernández, M.; Muscholl, A., 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020. 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, LIPIcs, vol. 152 (2020), Schloss Dagstuhl - Leibniz-Zentrum für Informatik: Schloss Dagstuhl - Leibniz-Zentrum für Informatik Barcelona, Spain), 35:1-35:12
[16] Prawitz, D., Natural Deduction. A Proof-Theoretical Study (1965), Almquist and Wiksell · Zbl 0173.00205
[17] Gentzen, G., Investigations into logical deduction, (Szabo, M. E., The Collected Papers of Gerhard Gentzen (1969), North Holland) · Zbl 0209.30001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.