Document Open Access Logo

Z; Syntax-Free Developments

Author Vincent van Oostrom

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.24.pdf
  • Filesize: 0.85 MB
  • 22 pages

Document Identifiers

Author Details

Vincent van Oostrom
  • Universität Innsbruck, Austria

Acknowledgements

Patrick Dehornoy introduced me to the main themes presented here, and indeed this paper was always intended to be a joint one. His work continues to be an inspiration. I want to thank Bertram Felgenhauer, Julian Nagele, and Christian Sternagel for discussions on their Isabelle formalisations of the Z-property.

Cite AsGet BibTex

Vincent van Oostrom. Z; Syntax-Free Developments. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.24

Abstract

We present the Z-property and instantiate it to various rewrite systems: associativity, positive braids, self-distributivity, the lambda-calculus, lambda-calculi with explicit substitutions, orthogonal TRSs, .... The Z-property is proven equivalent to Takahashi’s angle property by means of a syntax-free notion of development. We show that several classical consequences of having developments such as confluence, normalisation, and recurrence, can be regained in a syntax-free way, and investigate how the notion corresponds to the classical syntactic notion of development in term rewriting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • rewrite system
  • confluence
  • normalisation
  • recurrence

Metrics

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

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. In F.E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 31-46. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96712.
  2. P. Aczel. A general Church-Rosser theorem, 1978. corrections http://www.ens-lyon.fr/LIP/REWRITING/MISC/AGRT_corrections.pdf. URL: http://www.ens-lyon.fr/LIP/REWRITING/MISC/AGeneralChurch-RosserTheorem.pdf.
  3. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  4. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 2nd revised edition, 1984. Google Scholar
  5. A. Church and J.B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39:472-482, 1936. URL: https://doi.org/10.2307/1989762.
  6. P. Dehornoy. Braids and Self-Distributivity, volume 192 of Progress in Mathematics. Birkhäuser, 2000. Google Scholar
  7. P. Dehornoy and V. van Oostrom. Z; proving confluence by monotonic single-step upperbound functions. In Logical Models of Reasoning and Computation (LMRC-08), Moscow, 2008. URL: http://cl-informatik.uibk.ac.at/users/vincent/research/publication/talk/lmrc060508.pdf.
  8. J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, and V. van Oostrom. Infinitary term rewriting for weakly orthogonal systems: Properties and counterexamples. Logical Methods in Computer Science, 10(2), 2014. URL: https://doi.org/10.2168/LMCS-10(2:7)2014.
  9. B. Felgenhauer, J. Nagele, V. van Oostrom, and C. Sternagel. The Z property. Arch. Formal Proofs, 2016, 2016. URL: https://www.isa-afp.org/entries/Rewriting_Z.shtml.
  10. B. Felgenhaurer. Personal communication, 2017. Google Scholar
  11. Y. Honda, K. Nakazawa, and K. Fujita. Confluence proofs of lambda-mu-calculi by Z theorem. Studia Logica, 2021. URL: https://doi.org/10.1007/s11225-020-09931-0.
  12. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, 1980. URL: https://doi.org/10.1145/322217.322230.
  13. G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, Part I + II. In J.L. Lassez and G.D. Plotkin, editors, Computational Logic - Essays in Honor of Alan Robinson, pages 395-443, Cambridge MA, 1991. MIT Press. Update of: Call-by-need computations in non-ambiguous linear term rewriting systems, 1979. Google Scholar
  14. J. Ketema, J.W. Klop, and V. van Oostrom. Vicious circles in rewriting systems. Technical Report E0427, Centrum voor Wiskunde en Informatica, December 2004. URL: https://ir.cwi.nl/pub/11022/11022D.pdf.
  15. J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Reduction strategies and acyclicity. In H. Comon-Lundh, C. Kirchner, and H. Kirchner, editors, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of Lecture Notes in Computer Science, pages 89-112. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73147-4_5.
  16. Y. Komori, N. Matsuda, and F. Yamakawa. A simplified proof of the Church-Rosser theorem. Studia Logica: An International Journal for Symbolic Logic, 102(1):175-183, 2014. URL: https://doi.org/10.1007/s11225-013-9470-y.
  17. J.-J. Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse de doctorat d'état, Université Paris VII, 1978. URL: http://pauillac.inria.fr/~levy/pubs/78phd.pdf.
  18. R. Loader. Notes on simply typed lambda calculus. ECS-LFCS- 98-381, Laboratory for Foundations of Computer Science, The University of Edinburgh, 1998. URL: http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/.
  19. L. Maranget. La stratégie paresseuse. Thèse de doctorat, Université Paris 7, 1992. Google Scholar
  20. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theor. Comput. Sci., 19(1):3-29, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00143-6.
  21. P.-A. Melliès. Axiomatic rewriting theory VI residual theory revisited. In S. Tison, editor, Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, volume 2378 of Lecture Notes in Computer Science, pages 24-50. Springer, 2002. URL: https://doi.org/10.1007/3-540-45610-4_4.
  22. J. Nagele, V. van Oostrom, and C Sternagel. A short mechanized proof of the Church-Rosser theorem by the Z-property for the λβ-calculus in nominal Isabelle. In 5th International Workshop on Confluence, IWC 2016, Obergurgl, Austria, September 8-9, 2016, Online Proceedings, 1016. URL: http://www.csl.sri.com/users/tiwari/iwc2016/iwc2016.pdf.
  23. K. Nakazawa and K. Fujita. Compositional Z: Confluence proofs for permutative conversion. Studia Logica: An International Journal for Symbolic Logic, 104(6):1205-1224, 2016. URL: https://doi.org/10.1007/s11225-016-9673-0.
  24. R.P. Nederpelt. Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD thesis, Technische Hogeschool Eindhoven, June 1973. Google Scholar
  25. M.H.A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43:223-243, 1942. URL: https://doi.org/10.2307/2269299.
  26. T. Nipkow. Orthogonal higher-order rewrite systems are confluent. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 306-317. Springer, 1993. URL: https://doi.org/10.1007/BFb0037114.
  27. V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994. URL: https://research.vu.nl/files/62846778/complete%20dissertation.pdf.
  28. V. van Oostrom. Finite family developments. In H. Comon, editor, Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of Lecture Notes in Computer Science, pages 308-322. Springer, 1997. URL: https://doi.org/10.1007/3-540-62950-5_80.
  29. V. van Oostrom. Reduce to the max, 1999. Unpublished manuscript. URL: http://cl-informatik.uibk.ac.at/users/vincent/research/publication/pdf/max.pdf.
  30. V. van Oostrom. Random descent. In RTA, 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.
  31. V. van Oostrom. Abstract rewriting. In A. Middeldorp, editor, 3rd International School on Rewriting, ISR 2008, Obergurgl, Austria, July 21–26, 2008, 2008. Z-property in part 2 of the slides. URL: http://cl-informatik.uibk.ac.at/isr-2008/html/b.4.html.
  32. V. van Oostrom. Confluence by decreasing diagrams; converted. In A. Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, 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.
  33. V. van Oostrom and Y. Toyama. Normalisation by Random Descent. In FSCD, volume 52 of LIPIcs, pages 32:1-32:18. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.32.
  34. V. van Oostrom and Y. Venema. Term rewriting systems I and II. In 10th European Summer School in Logic, Language and Information, ESSLLI 98, Saarbrücken, Germany, August 17–-28, 1998, 2008. Course notes on braids in part I of the course. URL: http://cl-informatik.uibk.ac.at/users/vincent/research/publication/pdf/braids.pdf.
  35. F. van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1996. URL: https://research.vu.nl/files/62847150/complete%20dissertation.pdf.
  36. R. Statman. There is no hyperrecurrent s,k combinator. Research Report 91-1332, Department of Mathematics, Carnegie Mellon University, Pittsburg, PA 15213, June 1991. URL: http://shelf2.library.cmu.edu/Tech/53922203.pdf.
  37. M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120-127, 1995. URL: https://doi.org/10.1006/inco.1995.1057.
  38. Terese. Term Rewriting Systems. Cambridge University Press, 2003. 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