Document Open Access Logo

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

Authors Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.11.pdf
  • Filesize: 492 kB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • Multisets
  • ordinals
  • proof assistants

Metrics

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

Abstract

We present a collection of formalized results about finite nested multisets, developed using the Isabelle/HOL proof assistant. The nested multiset order is a generalization of the multiset order that can be used to prove termination of processes. Hereditary multisets, a variant of nested multisets, offer a convenient representation of ordinals below epsilon-0. In Isabelle/HOL, both nested and hereditary multisets can be comfortably defined as inductive datatypes. Our formal library also provides, somewhat nonstandardly, multisets with negative multiplicities and syntactic ordinals with negative coefficients. We present applications of the library to formalizations of Goodstein's theorem and the decidability of unary PCF (programming computable functions).

Cite As Get BibTex

Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.11

Author Details

Jasmin Christian Blanchette
Mathias Fleury
Dmitriy Traytel

References

  1. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 19-99. Elsevier, 2001. Google Scholar
  2. Jean-Pierre Banâtre, Pascal Fradet, and Yann Radenac. Generalised multisets for chemical programming. Math. Struct. Comput. Sci., 16(4):557-580, 2006. Google Scholar
  3. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. J. Funct. Program., 13(2):261-293, 2003. Google Scholar
  4. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Formalization of Knuth-Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs, 2016. URL: https://devel.isa-afp.org/entries/Lambda_Free_KBOs.shtml.
  5. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A transfinite Knuth-Bendix order for lambda-free higher-order terms. In Leonardo de Moura, editor, CADE-26, LNCS. Springer, 2017. Google Scholar
  6. Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs, 2016. URL: https://devel.isa-afp.org/entries/Nested_Multisets_Ordinals.shtml.
  7. Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. In Nicola Olivetti and Ashish Tiwari, editors, IJCAR 2016, volume 9706 of LNCS, pages 25-44. Springer, 2016. Google Scholar
  8. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. Google Scholar
  9. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 111-127. Springer, 2014. Google Scholar
  10. Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A lambda-free higher-order recursive path order. In Javier Esparza and Andrzej Murawski, editors, FoSSaCS 2017, volume 10203 of LNCS, pages 461-479. Springer, 2017. Google Scholar
  11. Frédéric Blanqui and Adam Koprowski. CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci., 21(4):827-859, 2011. Google Scholar
  12. Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow. Finding lexicographic orders for termination proofs in Isabelle/HOL. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, volume 4732 of LNCS, pages 38-53. Springer, 2007. Google Scholar
  13. Pierre Castéran and Évelyne Contejean. On ordinal notations. Coq User Contributions, 2006. URL: http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/Cantor.html.
  14. Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, FroCoS 2007, volume 4720 of LNCS, pages 148-162. Springer, 2007. Google Scholar
  15. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Commun. ACM, 22(8):465-476, 1979. Google Scholar
  16. Nachum Dershowitz and Georg Moser. The Hydra Battle revisited. In Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of LNCS, pages 1-27. Springer, 2007. Google Scholar
  17. R. L. Goodstein. On the restricted ordinal theorem. J. Symb. Logic, 9(2):33-41, 1944. Google Scholar
  18. José Grimm. Implementation of three types of ordinals in Coq. Technical Report RR-8407, Inria, 2013. URL: https://hal.inria.fr/hal-00911710/document.
  19. Gerard Huet and Derek C. Oppen. Equations and rewrite rules: A survey. In Ronald V. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349-405. Academic Press, 1980. Google Scholar
  20. Brian Huffman and Ondřej Kunčar. Lifting and Transfer: A modular design for quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, CPP 2013, volume 8307 of LNCS, pages 131-146. Springer, 2013. Google Scholar
  21. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. In William C. Chu, W. Eric Wong, Mathew J. Palakal, and Chih-Cheng Hung, editors, SAC 2011, pages 1639-1644. ACM, 2011. Google Scholar
  22. Laurie Kirby and Jeff Paris. Accessible independence results for Peano arithmetic. Bull. London Math. Soc., 4:285-293, 1982. Google Scholar
  23. Alexander Krauss. Partial recursive functions in higher-order logic. In Ulrich Furbach and Natarajan Shankar, editors, IJCAR 2006, volume 4130 of LNCS, pages 589-603. Springer, 2006. Google Scholar
  24. Alexander Krauss. Certified size-change termination. In Frank Pfenning, editor, CADE-21, volume 4603 of LNCS, pages 460-475. Springer, 2007. Google Scholar
  25. Ralph Loader. Unary PCF is decidable. Theor. Comput. Sci., 206(1-2):317-329, 1998. Google Scholar
  26. Michel Ludwig and Uwe Waldmann. An extension of the Knuth-Bendix ordering with LPO-like properties. In Nachum Dershowitz and Andrei Voronkov, editors, LPAR 2007, volume 4790 of LNCS, pages 348-362. Springer, 2007. Google Scholar
  27. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  28. Michael Norrish and Brian Huffman. Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP 2013, volume 7998 of LNCS, pages 133-146. Springer, 2013. Google Scholar
  29. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, IWIL-2010, volume 2 of EPiC, pages 1-11. EasyChair, 2012. Google Scholar
  30. Gordon D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223-255, 1977. Google Scholar
  31. John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP'83, pages 513-523, 1983. Google Scholar
  32. Manfred Schmidt-Schauß. Decidability of behavioural equivalence in unary PCF. Theor. Comput. Sci., 216(1-2):363-373, 1999. Google Scholar
  33. Peter H. Schmitt. A first-order theory of ordinals. In Cláudia Nalon and Renate Schmidt, editors, TABLEAUX 2017, LNCS. Springer, 2017. Google Scholar
  34. Wacław Sierpiński. Cardinal and Ordinal Numbers, volume 34 of Polska Akademia Nauk Monografie Matematyczne. Państwowe Wydawnictwo Naukowe, 1958. Google Scholar
  35. Gaisi Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2nd edition, 1987. Google Scholar
  36. René Thiemann, Guillaume Allais, and Julian Nagele. On the formalization of termination techniques based on multiset orderings. In Ashish Tiwari, editor, RTA 2012, volume 15 of LIPIcs, pages 339-354. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. Google Scholar
  37. Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In LICS 2012, pages 596-605. IEEE Computer Society, 2012. Google Scholar
  38. Martijn Vermaat. Infinitary Rewriting in Coq. M.Sc. thesis, Vrije Universiteit Amsterdam, 2010. URL: http://www.cs.vu.nl/~tcs/mt/vermaat.pdf.
  39. Makarius Wenzel. Isabelle/Isar - A generic framework for human-readable proof documents. In Roman Matuszewski and Anna Zalewska, editors, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar, and Rhetoric. Uniwersytet w Białymstoku, 2007. Google Scholar
  40. Harald Zankl, Sarah Winkler, and Aart Middeldorp. Beyond polynomials and Peano arithmetic - Automation of elementary and ordinal interpretations. J. Symb. Comput., 69:129-158, 2015. Google Scholar
  41. Hans Zantema. Termination. In Marc Bezem, Jan Willem Klop, and Roel de Vrijer, editors, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, pages 181-259. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact