Document Open Access Logo

Complete Non-Orders and Fixed Points

Authors Akihisa Yamada , Jérémy Dubut

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2019.30.pdf
  • Filesize: 463 kB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
Keywords
  • Order Theory
  • Lattice Theory
  • Fixed-Points
  • Isabelle/HOL

Metrics

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

Abstract

In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.

Cite As Get BibTex

Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.30

Author Details

Akihisa Yamada
  • National Institute of Informatics, Tokyo, Japan
Jérémy Dubut
  • National Institute of Informatics, Tokyo, Japan
  • Japanese-French Laboratory for Informatics, Tokyo, Japan

Funding

The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST; J. Dubut is also supported by Grant-in-aid No. 19K20215, JSPS.

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. Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In Jonathan M. Borwein and William M. Farmer, editors, Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM 2006), volume 4108 of LNCS, pages 31-43. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11812289_4.
  3. Stefan Berghofer and Tobias Nipkow. Random Testing in Isabelle/HOL. In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), pages 230-239. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/SEFM.2004.36.
  4. George M. Bergman. An Invitation to General Algebra and Universal Constructions. Springer International Publishing, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-11478-1.
  5. S. Parameshwara Bhatta. Weak chain-completeness and fixed point property for pseudo-ordered sets. Czechoslovak Mathematical Journal, 55(2):365-369, 2005. Google Scholar
  6. Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), volume 6172 of LNCS, pages 131-146. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_11.
  7. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), volume 6173 of LNCS, pages 107-121. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-14203-1_9.
  8. B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002. URL: https://doi.org/10.1017/CBO9780511809088.
  9. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott. Continuous Lattices and Domains. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511542725.
  10. Georges Gonthier. Formal proof - the four-color theorem. Notices of the AMS, 55(11):1382-1393, 2008. Google Scholar
  11. Florian Haftmann and Tobias Nipkow. A code generator framework for Isabelle/HOL. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics: Emerging Trends, pages 128-143. Department of Computer Science, University of Kaiserslautern, 2007. Google Scholar
  12. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5:e2, 2017. URL: https://doi.org/10.1017/fmp.2017.1.
  13. Florian Kammüller. Modular Reasoning in Isabelle. In David McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of LNCS, pages 99-114. Springer Berlin Heidelberg, 2000. URL: https://doi.org/10.1007/10721959_7.
  14. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Wiwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP 2009), pages 207-220. ACM, 2009. URL: https://doi.org/10.1145/1629575.1629596.
  15. K. Leutola and J. Nieminen. Posets and generalized lattices. Algebra Universalis, 16(1):344-354, 1983. Google Scholar
  16. J. D. Mashburn. The least fixed point property for omega-chain continuous functions. Houston Journal of Mathematics, 9(2):231-244, 1983. Google Scholar
  17. T. Nipkow, L.C. Paulson, and M. Wenzel. 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.
  18. S. Parameshwara Bhatta and Shiju George. Some fixed point theorems for pseudo ordered sets. Algebra and Discrete Mathematics, 11(1):17-22, 2011. Google Scholar
  19. H.L. Skala. Trellis theory. Algebra Univ., 1:218-233, 1971. URL: https://doi.org/10.1007/BF02944982.
  20. Abdelkader Stouti and Abdelhakim Maaden. Fixed points and common fixed points theorems in pseudo-ordered sets. Proyecciones, 32(4):409-418, 2013. URL: https://doi.org/10.4067/S0716-09172013000400008.
  21. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  22. Makarius Wenzel. Isabelle/jEdit - a prover IDE within the PIDE framework. In Proceedings of the 5th Conferences on Intelligent Computer Mathematics (CICM 2012), volume 7362 of LNCS, pages 468-471. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-31374-5_38.
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