Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1, 2, 3) , (2) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
paper.pdf (457.8 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01599176 , version 1 (01-10-2017)

Identifiers

Cite

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⟩
195 View
106 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More