Document Open Access Logo

Factorize Factorization

Authors Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2021.6.pdf
  • Filesize: 0.66 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Lambda calculus
  • Theory of computation → Logic
Keywords
  • Lambda Calculus
  • Rewriting
  • Reduction Strategies
  • Factorization

Metrics

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

Abstract

We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi.
The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus.
Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.

Cite As Get BibTex

Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize Factorization. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.6

Author Details

Beniamino Accattoli
  • Inria & LIX, École Polytechnique, UMR 7161, Palaiseau, France
Claudia Faggian
  • Université de Paris, IRIF, CNRS, F-75013 Paris, France
Giulio Guerrieri
  • University of Bath, Department of Computer Science, Bath, UK

Funding

This work is partially supported by ANR JCJC grant "COCA HOLA" (ANR-16-CE40-004-01), ANR PRC project PPS ({ANR-19-CE48-0014}), and EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

References

  1. Samson Abramsky and Guy McCusker. Call-by-value games. In Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference, volume 1414 of Lecture Notes in Computer Science, pages 1-17. Springer, 1997. URL: https://doi.org/10.1007/BFb0028004.
  2. Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In 23rd International Conference on Rewriting Techniques and Applications, RTA 2012, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.6.
  3. 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.
  4. Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, volume 10017 of Lecture Notes in Computer Science, pages 206-226. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12.
  5. Yohji Akama. On Mints' reduction for ccc-calculus. In Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, volume 664 of Lecture Notes in Computer Science, pages 1-12. Springer, 1993. URL: https://doi.org/10.1007/BFb0037094.
  6. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In 22nd ACM Symposium on Principles of Programming Languages, POPL'95, pages 233-246. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199507.
  7. Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Log. Methods Comput. Sci., 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:8)2017.
  8. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. In Functional and Logic Programming - 14th International Symposium, FLOPS 2018, volume 10818 of Lecture Notes in Computer Science, pages 132-148. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90686-7_9.
  9. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  10. Leo Bachmair and Nachum Dershowitz. Commutation, transformation, and termination. In 8th International Conference on Automated Deduction, CADE 1986, volume 230 of Lecture Notes in Computer Science, pages 5-20. Springer, 1986. URL: https://doi.org/10.1007/3-540-16780-3_76.
  11. 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
  12. Frédéric Blanqui. Size-based termination of higher-order rewriting. J. Funct. Program., 28:e11, 2018. URL: https://doi.org/10.1017/S0956796818000072.
  13. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability = typability + inhabitation. CoRR, 2018. URL: http://arxiv.org/abs/1812.06009.
  14. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Foundations of Software Science and Computation Structures, 17th International Conference, FoSSaCS 2014, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  15. Haskell B. Curry and Robert Feys. Combinatory Logic, Volume 1. Studies in logic and the foundations of mathematics. North-Holland, 1958. Google Scholar
  16. 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.
  17. Nachum Dershowitz. On lazy commutation. In O. Grumberg, M. Kaminski, S. Katz, and S. Wintner, editors, Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday, pages 59-82. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01748-3_5.
  18. Henk Doornbos and Burghard von Karger. On the union of well-founded relations. Logic Journal of the IGPL, 6(2):195-201, 1998. URL: https://doi.org/10.1093/jigpal/6.2.195.
  19. 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 Computer Society, 2019. URL: https://doi.org/10.1109/LICS.2019.8785699.
  20. Alfons Geser. Relative Termination. PhD thesis, University of Passau, Germany, 1990. URL: http://vts.uni-ulm.de/docs/2012/8146/vts_8146_11884.pdf.
  21. Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pages 72-81. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/LICS.1992.185521.
  22. Bernhard Gramlich. Modularity in term rewriting revisited. Theor. Comput. Sci., 464:3-19, 2012. URL: https://doi.org/10.1016/j.tcs.2012.09.008.
  23. Giulio Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, volume 46 of OASICS, pages 3-17. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/OASIcs.WPTE.2015.3.
  24. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a call-by-value lambda-calculus. In 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, volume 38 of LIPIcs, pages 211-225. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.211.
  25. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science, 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:29)2017.
  26. J. Roger Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964. Google Scholar
  27. J. Roger Hindley. Reductions of residuals are finite. Transactions of the American Mathematical Society, 240:345-361, 1978. Google Scholar
  28. J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, New York, NY, USA, 2 edition, 2008. Google Scholar
  29. 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.
  30. Katsumasa Ishii. A proof of the leftmost reduction theorem for λβη-calculus. Theor. Comput. Sci., 747:26-32, 2018. URL: https://doi.org/10.1016/j.tcs.2018.06.003.
  31. Jan Willem Klop. Combinatory Reduction Systems. Phd thesis, Mathematisch Centrum, Amsterdam, 1980. Google Scholar
  32. Masahito Kurihara and Ikuo Kaji. Modular term rewriting systems and the termination. Inf. Process. Lett., 34(1):1-4, 1990. URL: https://doi.org/10.1016/0020-0190(90)90221-I.
  33. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/j.tcs.2008.01.044.
  34. 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.
  35. 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.
  36. Thomas Leventis. A deterministic rewrite system for the probabilistic λ-calculus. Math. Struct. Comput. Sci., 29(10):1479-1512, 2019. URL: https://doi.org/10.1017/S0960129519000045.
  37. Jean-Jacques Lévy. Réductions corrcectes et optimales dans le lambda calcul. PhD thesis, University of Paris 7, 1978. Google Scholar
  38. Paul-André Melliès. Typed lambda-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, volume 902 of Lecture Notes in Computer Science, pages 328-334. Springer, 1995. URL: https://doi.org/10.1007/BFb0014062.
  39. Paul-André Melliès. A factorisation theorem in rewriting theory. In Category Theory and Computer Science, 7th International Conference, CTCS '97, volume 1290 of Lecture Notes in Computer Science, pages 49-68. Springer, 1997. URL: https://doi.org/doi.org/10.1007/BFb0026981.
  40. Aart Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Rewriting Techniques and Applications, 3rd International Conference, RTA-89, volume 355 of Lecture Notes in Computer Science, pages 263-277. Springer, 1989. URL: https://doi.org/10.1007/3-540-51081-8_113.
  41. Aart Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), pages 396-401. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39194.
  42. Aart Middeldorp. Confluence of the disjoint union of conditional term rewriting systems. In Conditional and Typed Rewriting Systems, 2nd International Workshop, CTRS 1990, volume 516 of Lecture Notes in Computer Science, pages 295-306. Springer, 1990. URL: https://doi.org/10.1007/3-540-54317-1_99.
  43. Gerd Mitschke. The standardization theorem for λ-calculus. Mathematical Logic Quarterly, 25(1‐2):29-31, 1979. URL: https://doi.org/10.1002/malq.19790250104.
  44. Luca Paolini. Call-by-value separability and computability. In Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer, 2001. URL: https://doi.org/10.1007/3-540-45446-2_5.
  45. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theor. Informatics Appl., 33(6):507-534, 1999. URL: https://doi.org/10.1051/ita:1999130.
  46. 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.
  47. Laurent Regnier. Une équivalence sur les lambda-termes. Theor. Comput. Sci., 126(2):281-292, 1994. URL: https://doi.org/10.1016/0304-3975(94)90012-4.
  48. György E. Révész. A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem. Theor. Comput. Sci., 93(1):75-89, 1992. URL: https://doi.org/10.1016/0304-3975(92)90212-X.
  49. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-10394-4.
  50. J. Barkley Rosser. A mathematical logic without variables. Duke Mathematical Journal, 1(3):328-355, September 1935. URL: https://doi.org/10.1215/S0012-7094-35-00123-5.
  51. Michaël Rusinowitch. On termination of the direct sum of term-rewriting systems. Inf. Process. Lett., 26(2):65-70, 1987. URL: https://doi.org/10.1016/0020-0190(87)90039-1.
  52. Alexis Saurin. On the relations between the syntactic theories of lambda-mu-calculi. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference, volume 5213 of Lecture Notes in Computer Science, pages 154-168. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_13.
  53. Masako Takahashi. Parallel reductions in lambda-calculus. Inf. Comput., 118(1):120-127, 1995. URL: https://doi.org/10.1006/inco.1995.1057.
  54. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  55. Yoshihito Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett., 25(3):141-143, 1987. URL: https://doi.org/10.1016/0020-0190(87)90122-0.
  56. Yoshihito Toyama. On the church-rosser property for the direct sum of term rewriting systems. J. ACM, 34(1):128-143, 1987. URL: https://doi.org/10.1145/7531.7534.
  57. Yoshihito Toyama, Jan Willem Klop, and Hendrik Pieter Barendregt. Termination for the direct sum of left-linear term rewriting systems -preliminary draft-. In Rewriting Techniques and Applications, 3rd International Conference, RTA-89, volume 355 of Lecture Notes in Computer Science, pages 477-491. Springer, 1989. URL: https://doi.org/10.1007/3-540-51081-8_127.
  58. Vincent Van Oostrom. Some symmetries of commutation diamonds. Talk at the International Workshop on Confluence, 30 June 2020. Google Scholar
  59. Vincent van Oostrom. Confluence by decreasing diagrams. In Rewriting Techniques and Applications, 19th International Conference, RTA 2008,, volume 5117 of Lecture Notes in Computer Science, pages 306-320. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_21.
  60. 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.
  61. Vincent van Oostrom and Hans Zantema. Triangulation in rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, volume 15 of LIPIcs, pages 240-255. Schloss Dagstuhl, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.240.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact