Document Open Access Logo

Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)

Authors Akihisa Yamada , Jérémy Dubut

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.34.pdf
  • Filesize: 0.75 MB
  • 13 pages

Document Identifiers

Author Details

Akihisa Yamada
  • National Institute of Advanced Industrial Science and Technology, Tokyo, Japan
Jérémy Dubut
  • National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

Funding

This work was supported by JST, CREST Grant Number JPMJCR22M1, Japan.

Cite AsGet BibTex

Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.34

Abstract

Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL’s ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Denotational semantics
Keywords
  • Directed Sets
  • Completeness
  • Scott Continuous Functions
  • Ordinals
  • Isabelle/HOL

Metrics

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

References

  1. Samson Abramsky and Achim Jung. Domain Theory. Number III in Handbook of Logic in Computer Science. Oxford University Press, 1994. Google Scholar
  2. Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989. Google Scholar
  3. Grzegorz Bancerek and Piotr Rudnicki. A compendium of continuous lattices in MIZAR. J. Autom. Reason., 29(3-4):189-224, 2002. URL: https://doi.org/10.1023/A:1021966832558.
  4. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 111-127. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_8.
  5. Paul M. Cohn. Universal Algebra. Harper & Row, 1965. Google Scholar
  6. Jérémy Dubut and Akihisa Yamada. Fixed point theorems for non-transitive relations. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/lmcs-18(1:30)2022.
  7. Alain Finkel and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, volume 3 of Leibniz International Proceedings in Informatics (LIPIcs), pages 433-444, Dagstuhl, Germany, 2009. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1844.
  8. Jean Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology, volume 22 of New Mathematical Monographs. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139524438.
  9. Tsurane Iwamura. A lemma on directed sets. Zenkoku Shijo Sugaku Danwakai, 262:107-111, 1944. in Japanese. Google Scholar
  10. George Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6:53-68, 1976. Google Scholar
  11. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  12. Lawrence C. Paulson and Krzysztof Grabczewski. Mechanizing set theory. J. Autom. Reason., 17(3):291-323, 1996. URL: https://doi.org/10.1007/BF00283132.
  13. Dana Scott. Outline of a Mathematical Theory of Computation. Technical Report PRG02, OUCL, 1970. Google Scholar
  14. Lev Anatol'evich Skornyakov. Complemented modular lattices and regular rings. Oliver & Boyd, 1964. Google Scholar
  15. Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. The MIT Press, 1993. 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