Skip to Main content Skip to Navigation
Conference papers

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

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 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 or-dinals with negative coefficients. We present applications of the library to formalizations of Goodstein's theorem and the decidability of unary PCF (programming computable functions). 1 Introduction In their seminal article on proving termination using multisets [15], Dershowitz and Manna introduced two orders of increasing strength. The multiset order lifts a base partial order on a set A to finite multisets over A. It forms the basis of the multiset path order, which has many applications in term rewriting [41] and automatic theorem proving [1]. The nested multiset order is a generalization of the multiset order that operates on multisets that can be nested in arbitrary ways. Nesting can increase the order's strength: If (A, <) has ordinal type α < 0 , the associated multiset order has ordinal type ω α , whereas the nested order has ordinal type 0 = ω ω ω. .. . In this paper, we present formal proofs of the main properties of the nested multiset order that are useful in applications: preservation of well-foundedness and preservation of totality (linearity). The proofs are developed in the Isabelle/HOL proof assistant [27]. To our knowledge, this is the first development of its kind in any proof assistant. Our starting point is the following inductive datatype of nested finite multisets over a type a (Section 4): datatype a nmultiset = Elem a | MSet ((a nmultiset) multiset) The above Isabelle/HOL command introduces a (unary postfix) type constructor, nmultiset, equipped with two constructors, Elem : a → a nmultiset and MSet : (a nmultiset)multiset → a nmultiset, where a is a type variable and multiset is the type constructor of (finite) multisets.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Sunday, October 1, 2017 - 6:56:29 PM
Last modification on : Wednesday, November 3, 2021 - 7:08:56 AM


Files produced by the author(s)




Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD 2017: 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. pp.1 - 11, ⟨10.4230/LIPIcs.FSCD.2017.11⟩. ⟨hal-01599176⟩



Les métriques sont temporairement indisponibles