Abstract
We introduce a call-by-name lambda-calculus \(\lambda J\) with generalized applications which integrates a notion of distant reduction that allows to unblock \(\beta \)-redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization –that we relate to others in the literature–, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus \(\lambda J\) and the well-know calculus \(\varLambda J\) determine equivalent notions of strong normalization. As a consequence, \(\varLambda J\) inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for \(\lambda J\), despite the fact that quantitative subject reduction fails for permutative conversions.
Chapter PDF
Similar content being viewed by others
References
Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. LIPIcs, vol. 15, pp. 6–21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)
Accattoli, B., Kesner, D.: The structural \(\lambda \)-calculus. In: Dawar, A., Veith, H. (eds.) Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6247, pp. 381–395. Springer (2010)
Espírito Santo, J., Frade, M.J., Pinto, L.: Structural proof theory as rewriting. In: Pfenning, F. (ed.) Term Rewriting and Applications. pp. 197–211. Lecture Notes in Computer Science, Springer (2006)
Espírito Santo, J.: Delayed substitutions. In: Lecture Notes in Computer Science, pp. 169–183. Springer Berlin Heidelberg (2007)
Espírito Santo, J.: The call-by-value lambda-calculus with generalized applications. In: CSL. LIPIcs, vol. 152, pp. 35:1–35:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
Espírito Santo, J., Kesner, D., Peyrot, L.: A faithful and quantitative notion of distant reduction for generalized applications. CoRR abs/2201.04156 (2022)
Espírito Santo, J., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculi with cuts. In: Hofmann, M. (ed.) Typed Lambda Calculi and Applications. pp. 286–300. Lecture Notes in Computer Science, Springer (2003)
Joachimski, F., Matthes, R.: Standardization and confluence for a lambda calculus with generalized applications. In: Rewriting Techniques and Applications, pp. 141–155. Springer Berlin Heidelberg (2000)
Kesner, D., Vial, P.: Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci. 16(1) (2020)
Matthes, R.: Characterizing strongly normalizing terms of a calculus with generalized applications via intersection types. In: Rolim, J.D.P., Broder, A.Z., Corradini, A., Gorrieri, R., Heckel, R., Hromkovic, J., Vaccaro, U., Wells, J.B. (eds.) ICALP Workshops 2000, Proceedings of the Satelite Workshops of the 27th International Colloquium on Automata, Languages and Programming, Geneva, Switzerland, July 9-15, 2000. pp. 339–354. Carleton Scientific, Waterloo, Ontario, Canada (2000)
von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Log. 40(7), 541–567 (2001)
van Raamsdonk, F.: Confluence and normalisation for higher-order rewriting. Ph.D. thesis, Vrije Universiteit Amsterdam (May 1996)
Regnier, L.: Une équivalence sur les lambda-termes. Theor. Comput. Sci. 126(2), 281–292 (1994)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Santo, J.E., Kesner, D., Peyrot, L. (2022). A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)