×

Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. (English) Zbl 1434.03025

Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 11, 18 p. (2017).
Summary: 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).
For the entire collection see [Zbl 1372.68017].

MSC:

03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
03F15 Recursive ordinals and ordinal notations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Alan Robinson and Andrei Voronkov, editors, {\it Handbook of Automated Reasoning}, volume I, pages 19-99. Elsevier, 2001. · Zbl 0993.03008
[2] Jean-Pierre Banâtre, Pascal Fradet, and Yann Radenac. Generalised multisets for chemical programming. {\it Math. Struct. Comput. Sci.}, 16(4):557-580, 2006. · Zbl 1122.68057
[3] Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. {\it J. Funct.} {\it Program.}, 13(2):261-293, 2003. · Zbl 1060.03030
[4] Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Formaliza tion of Knuth-Bendix orders for lambda-free higher-order terms. {\it Archive of Formal Proofs}, 2016. URL: https://devel.isa-afp.org/entries/Lambda_Free_KBOs.shtml. · Zbl 1496.03037
[5] Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A transfi nite Knuth-Bendix order for lambda-free higher-order terms. In Leonardo de Moura, editor, {\it CADE-26}, LNCS. Springer, 2017. · Zbl 1496.03037
[6] Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Formalization of nested multisets, hereditary multisets, and syntactic ordinals. {\it Archive of Formal Proofs}, 2016. URL: https://devel.isa-afp.org/entries/Nested_Multisets_Ordinals.shtml. · Zbl 1434.03025
[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, {\it IJCAR 2016}, volume 9706 of {\it LNCS}, pages 25-44. Springer, 2016. · Zbl 1475.68432
[8] Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Ger win Klein and Ruben Gamboa, editors, {\it ITP 2014}, volume 8558 of {\it LNCS}, pages 93-110. Springer, 2014. · Zbl 1416.68151
[9] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/ HOL. In Gerwin Klein and Ruben Gamboa, editors, {\it ITP 2014}, volume 8558 of {\it LNCS}, pages 111-127. Springer, 2014. · Zbl 1416.68152
[10] Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A lambda-free higher order recursive path order. In Javier Esparza and Andrzej Murawski, editors, {\it FoSSaCS} {\it 2017}, volume 10203 of {\it LNCS}, pages 461-479. Springer, 2017. · Zbl 1486.68085
[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. {\it Math.} {\it Struct. Comput. Sci.}, 21(4):827-859, 2011. · Zbl 1223.68101
[12] :18
[13] :17
[14] Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow. Finding lexicographic orders for termination proofs in Isabelle/HOL. In Klaus Schneider and Jens Brandt, editors, {\it TPHOLs} {\it 2007}, volume 4732 of {\it LNCS}, pages 38-53. Springer, 2007. · Zbl 1144.68352
[15] Pierre Castéran and Évelyne Contejean. On ordinal notations. {\it Coq User Contributions}, 2006. URL: http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/Cantor.html.
[16] Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Cer tification of automated termination proofs. In Boris Konev and Frank Wolter, editors, {\it FroCoS 2007}, volume 4720 of {\it LNCS}, pages 148-162. Springer, 2007. · Zbl 1148.68465
[17] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. {\it Com-} {\it mun. ACM}, 22(8):465-476, 1979. · Zbl 0431.68016
[18] Nachum Dershowitz and Georg Moser. The Hydra Battle revisited. In Hubert Comon Lundh, Claude Kirchner, and Hélène Kirchner, editors, {\it Rewriting, Computation and Proof,} {\it Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday}, volume 4600 of {\it LNCS}, pages 1-27. Springer, 2007. · Zbl 1181.68161
[19] R. L. Goodstein. On the restricted ordinal theorem. {\it J. Symb. Logic}, 9(2):33-41, 1944. · Zbl 0060.02306
[20] José Grimm. Implementation of three types of ordinals in Coq. Technical Report RR-8407, Inria, 2013. URL: https://hal.inria.fr/hal-00911710/document.
[21] Gerard Huet and Derek C. Oppen. Equations and rewrite rules: A survey. In Ronald V. Book, editor, {\it Formal Language Theory: Perspectives and Open Problems}, pages 349-405. Academic Press, 1980.
[22] 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, {\it CPP 2013}, volume 8307 of {\it LNCS}, pages 131-146. Springer, 2013. · Zbl 1426.68284
[23] 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, {\it SAC 2011}, pages 1639-1644. ACM, 2011. · Zbl 1326.68265
[24] Laurie Kirby and Jeff Paris. Accessible independence results for Peano arithmetic. {\it Bull.} {\it London Math. Soc.}, 4:285-293, 1982. · Zbl 0501.03017
[25] Alexander Krauss. Partial recursive functions in higher-order logic. In Ulrich Furbach and Natarajan Shankar, editors, {\it IJCAR 2006}, volume 4130 of {\it LNCS}, pages 589-603. Springer, 2006. · Zbl 1222.68367
[26] Alexander Krauss. Certified size-change termination. In Frank Pfenning, editor, {\it CADE-21}, volume 4603 of {\it LNCS}, pages 460-475. Springer, 2007. · Zbl 1213.68571
[27] Ralph Loader. Unary PCF is decidable. {\it Theor. Comput. Sci.}, 206(1-2):317-329, 1998. · Zbl 0916.68017
[28] Michel Ludwig and Uwe Waldmann. An extension of the Knuth-Bendix ordering with LPO-like properties. In Nachum Dershowitz and Andrei Voronkov, editors, {\it LPAR 2007}, volume 4790 of {\it LNCS}, pages 348-362. Springer, 2007. · Zbl 1137.03306
[29] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. {\it Isabelle/HOL: A Proof Assistant} {\it for Higher-Order Logic}, volume 2283 of {\it LNCS}. Springer, 2002. · Zbl 0994.68131
[30] Michael Norrish and Brian Huffman. Ordinals in HOL: Transfinite arithmetic up to (and beyond) {\it ω}1. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, {\it ITP 2013}, volume 7998 of {\it LNCS}, pages 133-146. Springer, 2013. · Zbl 1317.68227
[31] 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, {\it IWIL-2010}, volume 2 of {\it EPiC}, pages 1-11. EasyChair, 2012.
[32] Gordon D. Plotkin. LCF considered as a programming language. {\it Theor. Comput. Sci.}, 5(3):223-255, 1977. · Zbl 0369.68006
[33] John C. Reynolds. Types, abstraction and parametric polymorphism. In {\it IFIP’83}, pages 513-523, 1983.
[34] Manfred Schmidt-Schauß. Decidability of behavioural equivalence in unary PCF. {\it Theor.} {\it Comput. Sci.}, 216(1-2):363-373, 1999. · Zbl 0914.68125
[35] Peter H. Schmitt. A first-order theory of ordinals. In Cláudia Nalon and Renate Schmidt, editors, {\it TABLEAUX 2017}, LNCS. Springer, 2017. · Zbl 1496.68371
[36] Wacław Sierpiński. {\it Cardinal and Ordinal Numbers}, volume 34 of {\it Polska Akademia Nauk} {\it Monografie Matematyczne}. Państwowe Wydawnictwo Naukowe, 1958. · Zbl 0083.26803
[37] Gaisi Takeuti. {\it Proof Theory}, volume 81 of {\it Studies in Logic and the Foundations of Mathe-} {\it matics}. North-Holland, 2nd edition, 1987. · Zbl 0681.03039
[38] René Thiemann, Guillaume Allais, and Julian Nagele. On the formalization of termination techniques based on multiset orderings. In Ashish Tiwari, editor, {\it RTA 2012}, volume 15 of {\it LIPIcs}, pages 339-354. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. · Zbl 1437.68088
[39] Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compo sitional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In {\it LICS 2012}, pages 596-605. IEEE Computer Society, 2012. · Zbl 1362.68251
[40] Martijn Vermaat. {\it Infinitary Rewriting in Coq}. M.Sc. thesis, Vrije Universiteit Amsterdam, 2010. URL: http://www.cs.vu.nl/ tcs/mt/vermaat.pdf.
[41] Makarius Wenzel. Isabelle/Isar - A generic framework for human-readable proof documents. In Roman Matuszewski and Anna Zalewska, editors, {\it From Insight to Proof: Festschrift in} {\it Honour of Andrzej Trybulec}, volume 10(23) of {\it Studies in Logic, Grammar, and Rhetoric}. Uniwersytet w Białymstoku, 2007. · Zbl 1144.68369
[42] Harald Zankl, Sarah Winkler, and Aart Middeldorp. Beyond polynomials and Peano arith metic - Automation of elementary and ordinal interpretations. {\it J. Symb. Comput.}, 69:129- 158, 2015. · Zbl 1315.68168
[43] Hans Zantema. Termination. In Marc Bezem, Jan Willem Klop, and Roel de Vrijer, editors, {\it Term Rewriting Systems}, volume 55 of {\it Cambridge Tracts in Theoretical Computer Science}, pages 181-259. Cambridge University Press, 2003. · Zbl 1030.68053
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.