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.
Type de document :
Communication dans un congrès
FSCD 2017: 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. 11, pp.1 - 11, 〈10.4230/LIPIcs.FSCD.2017.11〉
Liste complète des métadonnées

Littérature citée [44 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01599176
Contributeur : Jasmin Christian Blanchette <>
Soumis le : dimanche 1 octobre 2017 - 18:56:29
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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. 11, pp.1 - 11, 〈10.4230/LIPIcs.FSCD.2017.11〉. 〈hal-01599176〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

7