Normalization by Evaluation for Typed Weak lambda-Reduction
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction.
In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.
normalization
lambda-calculus
reduction
term-rewriting
Agda
Theory of computation~Lambda calculus
6:1-6:17
Regular Paper
https://github.com/fsestini/nbe-weak-stlc
We thank Maria Emilia Maietti, Claudio Sacerdoti Coen, Thorsten Altenkirch, Andreas Abel, and Delia Kesner for helpful discussions and feedback on this work.
Filippo
Sestini
Filippo Sestini
Functional Programming Laboratory, University of Nottingham, United Kingdom
http://www.cs.nott.ac.uk/~psxfs5
10.4230/LIPIcs.TYPES.2018.6
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, October 1991.
A. Abel. Normalization by Evaluation, Dependent Types and Impredicativity. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 2013.
Andreas Abel, Klaus Aehlig, and Peter Dybjer. Normalization by Evaluation for Martin-Löf Type Theory with One Universe. Electronic Notes in Theoretical Computer Science, 173:17–39, April 2007.
Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1990.
Klaus Aehlig and Felix Joachimski. Operational aspects of untyped Normalisation by Evaluation. Mathematical Structures in Computer Science, 14(4):587–611, 2004.
Yohji Akama. A λ-to-CL translation for strong normalization. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, pages 1-10, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.
Thorsten Altenkirch and James Chapman. Big-step Normalisation. J. Funct. Program., 19(3–4):311–333, July 2009.
Thorsten Altenkirch and Ambrus Kaposi. Type Theory in Type Theory Using Quotient Inductive Types. SIGPLAN Not., 51(1):18-29, January 2016. URL: https://doi.org/10.1145/2914770.2837638.
https://doi.org/10.1145/2914770.2837638
Hendrik Pieter Barendregt. The lambda calculus: its syntax and semantics. North-Holland, 1984.
Bruno Barras, Thierry Coquand, and Simon Huber. A generalization of the Takeuti–Gandy interpretation. Mathematical Structures in Computer Science, 25(5):1071–1099, 2015. URL: https://doi.org/10.1017/S0960129514000504.
https://doi.org/10.1017/S0960129514000504
U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed lambda-calculus. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, page 203–211, July 1991.
Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda - A Functional Language with Dependent Types. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 73-78, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
https://doi.org/10.1007/978-3-642-03359-9_6
Naim Çağman and J.Roger Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198(1):239-247, 1998.
Arthur Charguéraud. The Locally Nameless Representation. Journal of Automated Reasoning, 49(3):363-408, October 2012.
Thierry Coquand. Weak Type Theory (unpublished note). URL: http://www.cse.chalmers.se/~coquand/wmltt.pdf.
http://www.cse.chalmers.se/~coquand/wmltt.pdf
Thierry Coquand and Peter Dybjer. Intuitionistic Model Constructions and Normalization Proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen, 1993.
Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence Properties of Weak and Strong Calculi of Explicit Substitutions. J. ACM, 43(2):362-397, March 1996.
H. B. Curry and R. Feys. Combinatory Logic. Philosophische Rundschau, 6(3/4):294, 1958.
Nils Anders Danielsson. A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, pages 93-109, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.
N. G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381–392, January 1972.
Peter Dybjer and Denis Kuperberg. Formal Neighbourhoods, Combinatory Böhm Trees, and Untyped Normalization by Evaluation, 2008.
J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse de doctorat d'État, Univerité Paris 7, 1972.
Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012.
J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, 2 edition, 2008.
W.A. Howard. Assignment of Ordinals to Terms for Primitive Recursive Functionals of Finite Type. In Studies in Logic and the Foundations of Mathematics. Elsevier, 1970.
J.M.E. Hyland and C. h. L. Ong. Modified Realizability Toposes and Strong Normalization Proofs (Extended Abstract). In Typed Lambda Calculi and Applications, LNCS 664, pages 179-194. Springer-Verlag, 1993.
Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio, and Thomas Streicher. Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice. Archive for Mathematical Logic, January 2018.
Achim Jung and Jerzy Tiuryn. A New Characterization of Lambda Definability. Springer, 1993.
Delia Kesner. Reasoning About Call-by-need by Means of Types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, pages 424-441, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.
Delia Kesner, Alejandro Ríos, and Andrés Viso. Call-by-Need, Neededness and All That. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 241-257, Cham, 2018. Springer International Publishing.
Jean-Jacques Lévy and Luc Maranget. Explicit Substitutions and Programming Languages. In Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, page 181–200. Springer, Berlin, Heidelberg, December 1999.
M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009.
M.E. Maietti and G. Sambin. Toward a Minimalist Foundation for Constructive Mathematics. From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, 48, 2005.
Per Martin-Löf. About Models for Intuitionistic Type Theories and the Notion of Definitional Equality. Studies in Logic and the Foundations of Mathematics, 82, December 1975.
Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part, volume 80 of Logic Colloquium ’73, page 73–118. Elsevier, January 1975.
C.-H. Luke Ong. Fully Abstract Models of the Lazy Lambda Calculus. In FOCS, 1988.
Filippo Sestini. Normalization by Evaluation for Typed Lambda-Calculi with Weak Conversions (MSc’s Thesis, unpublished), 2018. URL: http://www.cs.nott.ac.uk/~psxfs5/msc-thesis.pdf.
http://www.cs.nott.ac.uk/~psxfs5/msc-thesis.pdf
Vincent Siles and Hugo Herbelin. Pure Type System conversion is always typable. Journal of Functional Programming, 22(2):153–180, 2012.
W. W. Tait. Intensional interpretations of functionals of finite type. Journal of Symbolic Logic, 32(2):198–212, 1967.
A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, Volume 2. Studia Logica, 50(2):355-356, 1991.
Filippo Sestini
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode