Document Open Access Logo

Strategies for Asymptotic Normalization

Authors Claudia Faggian, Giulio Guerrieri

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.17.pdf
  • Filesize: 1.01 MB
  • 24 pages

Document Identifiers

Author Details

Claudia Faggian
  • IRIF, CNRS, Université de Paris Cité, F-75013 Paris, France
Giulio Guerrieri
  • Huawei Research, Edinburgh Research Centre, UK

Funding

Work supported by the ANR project PPS: ANR-19-CE48-0014.

Cite AsGet BibTex

Claudia Faggian and Giulio Guerrieri. Strategies for Asymptotic Normalization. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 17:1-17:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.17

Abstract

We present an abstract technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation - where the limits are distributions over the possible outputs - or infinitary lambda-calculi - where the limits are infinitary terms such as Böhm trees. As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and - in a uniform way - for Call-by-Name) probabilistic lambda-calculus.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Lambda calculus
Keywords
  • rewriting
  • strategies
  • normalization
  • lambda calculus
  • probabilistic rewriting

Metrics

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

Related Versions

References

  1. Samson Abramsky and C.-H. Luke Ong. Full Abstraction in the Lazy Lambda Calculus. Inf. Comput., 105(2):159-267, 1993. URL: https://doi.org/10.1006/inco.1993.1044.
  2. Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and Normalization, Essentially. In Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, volume 11893 of Lecture Notes in Computer Science, pages 159-180. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_9.
  3. Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9780511983504.
  4. Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic, 117(1):95-168, 2002. URL: https://doi.org/10.1016/S0168-0072(01)00104-X.
  5. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Sci. Comput. Program., 185, 2020. URL: https://doi.org/10.1016/j.scico.2019.102338.
  6. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  7. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  8. Henk Barendregt and Jan Willem Klop. Applications of infinitary lambda calculus. Inf. Comput., 207(5):559-582, 2009. URL: https://doi.org/10.1016/j.ic.2008.09.003.
  9. Alessandro Berarducci and Benedetto Intrigila. Church-Rosser λ-theories, infinite λ-calculus and consistency problems. In W. Hodges, M. Hyland, and et. al., editors, Logic: From Foundations to Applications (European Logic Colloquium), pages 33-58. Oxford Sci. Publ., 1996. Google Scholar
  10. Gianluca Curzi and Michele Pagani. The Benefit of Being Non-Lazy in Probabilistic λ-calculus: Applicative Bisimulation is Fully Abstract for Non-Lazy Probabilistic Call-by-Name. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 327-340. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394806.
  11. Roel C. de Vrijer. Conditional linearization. Indagationes Mathematicae, 10(1):145-159, 1999. URL: https://doi.org/10.1016/S0019-3577(99)80012-3.
  12. Ugo de'Liguoro and Adolfo Piperno. Non Deterministic Extensions of Untyped Lambda-Calculus. Inf. Comput., 122(2):149-177, 1995. URL: https://doi.org/10.1006/inco.1995.1145.
  13. Claudia Faggian. Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131 of LIPIcs, pages 19:1-19:25. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.19.
  14. Claudia Faggian. Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms. Log. Methods Comput. Sci., vol. 18, issue 2, 2022. Google Scholar
  15. Claudia Faggian and Giulio Guerrieri. Strategies for Asymptotic Normalization (long version). CoRR, 2022. URL: http://arxiv.org/abs/2204.08772.
  16. Claudia Faggian and Simona Ronchi Della Rocca. Lambda Calculus and Probabilistic Computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785699.
  17. Francesco Gavazzo. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. PhD thesis, Università di Bologna, Italy, 2019. URL: https://tel.archives-ouvertes.fr/tel-02386201.
  18. Francesco Gavazzo and Claudia Faggian. A Relational Theory of Monadic Rewriting Systems, Part I. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470633.
  19. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  20. J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda-Calculus. Cambridge University Press, 1986. Google Scholar
  21. Nao Hirokawa, Aart Middeldorp, and Georg Moser. Leftmost Outermost Revisited. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015, volume 36 of LIPIcs, pages 209-222. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.209.
  22. J. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Transfinite Reductions in Orthogonal Term Rewriting Systems. Inf. Comput., 119(1):18-38, 1995. URL: https://doi.org/10.1006/inco.1995.1075.
  23. J. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93-125, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00171-5.
  24. Ugo Dal Lago and Francesco Gavazzo. Effectful Normal Form Bisimulation. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 263-292. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_10.
  25. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl., 46(3):413-450, 2012. URL: https://doi.org/10.1051/ita/2012012.
  26. Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. URL: http://gallium.inria.fr/~xleroy/publi/ZINC.pdf.
  27. Thomas Leventis. A deterministic rewrite system for the probabilistic λ-calculus. Mathematical Structures in Computer Science, 29(10):1479-1512, 2019. URL: https://doi.org/10.1017/S0960129519000045.
  28. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda calcul. PhD thesis, Université Paris 7, 1978. URL: http://pauillac.inria.fr/~levy/pubs/74phd-cycle3.pdf.
  29. Maxwell H. A. Newman. On Theories with a Combinatorial Definition of Equivalence. Annals of Mathematics, 43(2), 1942. Google Scholar
  30. Gordon D. Plotkin. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  31. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  32. Vincent van Oostrom. Random Descent. In Term Rewriting and Applications, 18th International Conference, RTA 2007, volume 4533 of Lecture Notes in Computer Science, pages 314-328. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_24.
  33. Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, volume 52 of LIPIcs, pages 32:1-32:18. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.32.
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