Document Open Access Logo

Normalization by Evaluation for Typed Weak lambda-Reduction

Author Filippo Sestini

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.6.pdf
  • Filesize: 475 kB
  • 17 pages

Document Identifiers

Author Details

Filippo Sestini
  • Functional Programming Laboratory, University of Nottingham, United Kingdom

Acknowledgements

We thank Maria Emilia Maietti, Claudio Sacerdoti Coen, Thorsten Altenkirch, Andreas Abel, and Delia Kesner for helpful discussions and feedback on this work.

Cite AsGet BibTex

Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.6

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • normalization
  • lambda-calculus
  • reduction
  • term-rewriting
  • Agda

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, October 1991. Google Scholar
  2. A. Abel. Normalization by Evaluation, Dependent Types and Impredicativity. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 2013. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. Klaus Aehlig and Felix Joachimski. Operational aspects of untyped Normalisation by Evaluation. Mathematical Structures in Computer Science, 14(4):587–611, 2004. Google Scholar
  6. 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. Google Scholar
  7. Thorsten Altenkirch and James Chapman. Big-step Normalisation. J. Funct. Program., 19(3–4):311–333, July 2009. Google Scholar
  8. 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.
  9. Hendrik Pieter Barendregt. The lambda calculus: its syntax and semantics. North-Holland, 1984. Google Scholar
  10. 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.
  11. 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. Google Scholar
  12. 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.
  13. Naim Çağman and J.Roger Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198(1):239-247, 1998. Google Scholar
  14. Arthur Charguéraud. The Locally Nameless Representation. Journal of Automated Reasoning, 49(3):363-408, October 2012. Google Scholar
  15. Thierry Coquand. Weak Type Theory (unpublished note). URL: http://www.cse.chalmers.se/~coquand/wmltt.pdf.
  16. Thierry Coquand and Peter Dybjer. Intuitionistic Model Constructions and Normalization Proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen, 1993. Google Scholar
  17. 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. Google Scholar
  18. H. B. Curry and R. Feys. Combinatory Logic. Philosophische Rundschau, 6(3/4):294, 1958. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. Peter Dybjer and Denis Kuperberg. Formal Neighbourhoods, Combinatory Böhm Trees, and Untyped Normalization by Evaluation, 2008. Google Scholar
  22. 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. Google Scholar
  23. Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012. Google Scholar
  24. J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, 2 edition, 2008. Google Scholar
  25. 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. Google Scholar
  26. 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. Google Scholar
  27. 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. Google Scholar
  28. Achim Jung and Jerzy Tiuryn. A New Characterization of Lambda Definability. Springer, 1993. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. 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. Google Scholar
  32. M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009. Google Scholar
  33. 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. Google Scholar
  34. 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. Google Scholar
  35. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part, volume 80 of Logic Colloquium ’73, page 73–118. Elsevier, January 1975. Google Scholar
  36. C.-H. Luke Ong. Fully Abstract Models of the Lazy Lambda Calculus. In FOCS, 1988. Google Scholar
  37. 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.
  38. Vincent Siles and Hugo Herbelin. Pure Type System conversion is always typable. Journal of Functional Programming, 22(2):153–180, 2012. Google Scholar
  39. W. W. Tait. Intensional interpretations of functionals of finite type. Journal of Symbolic Logic, 32(2):198–212, 1967. Google Scholar
  40. A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, Volume 2. Studia Logica, 50(2):355-356, 1991. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact