Document Open Access Logo

Generalized Newman’s Lemma for Discrete and Continuous Systems

Author Ievgen Ivanov

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.9.pdf
  • Filesize: 0.91 MB
  • 17 pages

Document Identifiers

Author Details

Ievgen Ivanov
  • Taras Shevchenko National University of Kyiv, Ukraine

Cite As Get BibTex

Ievgen Ivanov. Generalized Newman’s Lemma for Discrete and Continuous Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.9

Abstract

We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a corollary of this criterion. We describe a formalization of the proposed generalized Newman’s lemma in Isabelle proof assistant using HOL logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
  • Theory of computation → Timed and hybrid models
Keywords
  • abstract rewriting system
  • confluence
  • discrete-continuous systems
  • proof assistant
  • formal proof

Metrics

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

Supplementary Materials

References

  1. An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions. URL: http://cl-informatik.uibk.ac.at/isafor/.
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1999. Google Scholar
  3. Radhakisan Baheti and Helen Gill. Cyber-physical systems. The impact of control technology, 12(1):161-166, 2011. Google Scholar
  4. Pete L. Clark. The instructor’s guide to real induction. Mathematics Magazine, 92(2):136-150, 2019. Google Scholar
  5. Patrick Dehornoy and Vincent van Oostrom. Z, proving confluence by monotonic single-step upperbound functions. Logical Models of Reasoning and Computation (LMRC-08), page 85, 2008. Google Scholar
  6. Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing diagrams with two labels are complete for confluence of countable systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  7. Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Decreasing diagrams for confluence and commutation. Logical Methods in Computer Science, 16, 2020. Google Scholar
  8. Rafal Goebel, Ricardo G Sanfelice, and Andrew R Teel. Hybrid dynamical systems. IEEE control systems magazine, 29(2):28-93, 2009. Google Scholar
  9. Jean Goubault-Larrecq. Non-Hausdorff topology and domain theory: Selected topics in point-set topology, volume 22. Cambridge University Press, 2013. Google Scholar
  10. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, 1980. Google Scholar
  11. Isabelle proof assistant. http://isabelle.in.tum.de. [Online].
  12. Ievgen Ivanov. On representations of abstract systems with partial inputs and outputs. In T.V. Gopal, M. Agrawal, A. Li, and S.B. Cooper, editors, Theory and Applications of Models of Computation, volume 8402 of Lecture Notes in Computer Science, pages 104-123. Springer, 2014. Google Scholar
  13. Ievgen Ivanov. On induction for diamond-free directed complete partial orders. In CEUR-WS.org, volume 2732, pages 70-73, 2020. Google Scholar
  14. Ievgen Ivanov. Formalization of Generalized Newman’s Lemma (supplementary material for this paper). https://doi.org/10.5281/zenodo.7855691, 2023. [Online].
  15. Jan Willem Klop. Term rewriting systems. Centrum voor Wiskunde en Informatica, 1990. Google Scholar
  16. Edward A. Lee. Fundamental limits of cyber-physical systems modeling. ACM Transactions on Cyber-Physical Systems, 1(1), 2016. Google Scholar
  17. Philippe Malbos. Lectures on algebraic rewriting. http://hal.archives-ouvertes.fr/hal-02461874, 2019.
  18. George Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6(1):53-68, 1976. Google Scholar
  19. F. Mattern. On the relativistic structure of logical time in distributed systems. Parallel and Distributed Algorithms, 1992. Google Scholar
  20. Maxwell Herman Alexander Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, pages 223-243, 1942. Google Scholar
  21. Newman’s lemma - Wikipedia, the free encyclopedia. http://en.wikipedia.org/Newman_lemma. [Online].
  22. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. Google Scholar
  23. André Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 819-828, 2018. Google Scholar
  24. Jean-Claude Raoult. Proving open properties by induction. Information processing letters, 29(1):19-23, 1988. Google Scholar
  25. Christian Sternagel and Rene Thiemann. Abstract rewriting. Archive of Formal Proofs, June 2010. Google Scholar
  26. Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical computer science, 126(2):259-280, 1994. Google Scholar
  27. Freek Wiedijk. The seventeen provers of the world: Foreword by Dana S. Scott, volume 3600. Springer, 2006. Google Scholar
  28. J. C. Willems. Paradigms and puzzles in the theory of dynamical systems. IEEE Transactions on Automatic Control, 36(3):259-294, 1991. Google Scholar
  29. Harald Zankl. Decreasing diagrams. Archive of Formal Proofs, 2013. 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 About DROPS Imprint Privacy Contact