Jasmin Christian Blanchette

Mathias Fleury

Dmitriy Traytel

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

Keywords: 1998 ACM Subject Classification F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs, F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic, I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving Multisets, ordinals, proof assistants Digital Object Identifier 10.4230/LIPIcs.FSCD.2017.11 Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

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 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).

Introduction

In their seminal article on proving termination using multisets [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF], 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 [START_REF] Zantema | Termination[END_REF] 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 [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF]. 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.

Throughout the paper, we will write "multiset" meaning "finite multiset," following Isabelle conventions. The datatype command also introduces a recursor that can be used to define primitive recursive functions. In addition, the command provides an induction principle, which allows us to assume, in the MSet NM case, that the desired property holds for all nested multisets belonging to NM .

The definition of nmultiset exhibits recursion through a non-datatype (multiset). In recent versions of Isabelle/HOL, recursion is allowed under arbitrary type constructors that are bounded natural functors [START_REF] Christian Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF][START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF], a semantic criterion that is met by bounded sets, multisets, and other functors. This flexibility is absent in other proof assistants. The HOL systems and Lean support quotient types, which can be used to build multisets from lists; in Agda and Coq, setoids can be employed instead [START_REF] Barthe | Setoids in type theory[END_REF]. However, we argue that datatypes lead to simpler definitions and proofs than any of the alternatives.

If we omit the Elem constructor, we obtain the hereditary multisets (Section 5):

datatype hmultiset = HMSet (hmultiset multiset)
This type is similar to hereditarily finite sets, a model of set theory without the axiom of infinity, but with multisets instead of finite sets. It is easy to embed hmultiset in a nmultiset, and using Isabelle's Lifting and Transfer tools [START_REF] Huffman | Lifting and Transfer: A modular design for quotients in Isabelle/HOL[END_REF], we can lift definitions and results from the larger type to the smaller type, such as the definition of the nested multiset order. Hereditary multisets offer a convenient representation for ordinals below 0 (Section 6). These are the ordinals that can be expressed syntactically in Cantor normal form:

α ::= ω α1 • c 1 + • • • + ω αn • c n where c i ∈ N >0 and α 1 > • • • > α n
The correspondence with hereditary multisets is straightforward:

}

The coefficients c i are represented by multiset multiplicities, and the ω exponents are the multiset's members. Thus:

{} = 0 {0} = {{}} = ω 0 = 1 {0, 0, 0} = {{}, {}, {}} = ω 0 • 3 = 3 {1} = {{{}}} = ω ω 0 = ω 1 = ω {ω} = {{{{}}}} = ω ω
The standard addition and multiplication operations on ordinals are not commutative-e.g., 1 + ω = ω = ω + 1. Instead, we formalized the Hessenberg (or natural) operations [START_REF] Sierpiński | Cardinal and Ordinal Numbers[END_REF]. These are more convenient in many applications, and because they share many properties with natural numbers, they are easier to automate in Isabelle.

When carrying out proofs, we sometimes find ourselves wishing that it would be possible to subtract an ordinal from another. To support this, we define a type of signed multisets, or hybrid multisets [START_REF] Banâtre | Generalised multisets for chemical programming[END_REF], and use it to represent signed ordinals (Section 7).

We employ our library to formalize two examples that require ordinals or the nested multiset order: Goodstein's theorem (Section 8) and the decidability of unary PCF ( Section 9). Together with colleagues, Blanchette also used the library to formalize a variant of the transfinite Knuth-Bendix order [START_REF] Becker | Formalization of Knuth-Bendix orders for lambda-free higher-order terms[END_REF][START_REF] Becker | A transfinite Knuth-Bendix order for lambda-free higher-order terms[END_REF]. We gave some thought to proof automation, generalizing existing simplification procedures and exploiting Isabelle's arithmetic type classes. Our work also demonstrates the usefulness of bounded natural functors. The Isabelle theory files are available as part of the Archive of Formal Proofs [START_REF] Christian Blanchette | Formalization of nested multisets, hereditary multisets, and syntactic ordinals[END_REF]. Isabelle/HOL Isabelle is a generic proof assistant whose metalogic is an intuitionistic fragment of polymorphic higher-order logic (simple type theory). Types are built from type variables a, b, . . . and type constructors, written infix or postfix (e.g., →, multiset). All types are inhabited. Terms t, u are built from variables x, constants c, abstractions λx. t, and applications t u. Constants may be higher-order, i.e., they may be of function type. A formula is a term of type prop. The metalogical operators are , = ⇒, and ≡, for universal quantification, implication, and equality. The notation x. t is syntactic sugar for (λx. t).

Isabelle/HOL is the instantiation of Isabelle with classical higher-order logic (HOL) extended with type classes as its object logic, complete with a Boolean type bool, an equality predicate =, the usual connectives (¬, ∧, ∨, -→, ← →) and quantifiers (∀, ∃), and Hilbert's choice. HOL formulas, of type bool, are embedded in the metalogic. The distinction between prop and bool is important operationally, but it is not essential to understand this paper.

Isabelle/HOL offers two primitive definitional mechanisms: The typedef command introduces a type that is isomorphic to a nonempty subset of an existing type, and the definition command introduces a constant as equal to an existing term. On top of these, Isabelle/HOL provides a rich specification language that includes inductive datatypes and predicates, recursive functions, and their coinductive counterparts, as well as quotient types.

Proofs are expressed either as a sequence of low-level proof methods, called tactics, which manipulate the proof state directly, or in a declarative format called Isar [START_REF] Wenzel | Isabelle/Isar-A generic framework for human-readable proof documents[END_REF], which allows tactics only as terminal procedures. We generally prefer the more readable Isar style. The main proof methods are the simplifier, which rewrites terms using conditional oriented equations; the classical reasoner, which applies introduction and elimination rules; decision procedures for linear arithmetic; and metis, a complete first-order prover based on superposition. In addition, the Sledgehammer tool [START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF] integrates third-party automatic theorem provers. It can be applied to any proof goal. In case of success, it provides a short Isar proof, often using metis.

Multisets

Multisets over a are defined in Isabelle's standard library as isomorphic to the set of multiplicity functions f that are 0 at all but finitely many points x:

typedef a multiset = f : a → nat | finite {x | f x > 0}
Values are constructed from the empty multiset {} and the add x A operation. For concrete multisets, we use standard set notation. The singleton multiset {x} is easy to define in terms of add and {}. Multiset union , which adds the multiplicities of its arguments, is an instance of the polymorphic + : a → a → a operator. The relevant + type classes provide a wealth of lemmas and some proof automation. Other operations include -, ∪, ∩, ⊂, ⊆, <, and ≤.

Given a type a equipped with a partial order <, the < operator on multisets corresponds to the Dershowitz-Manna extension [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]. The extension operator is also available as a function mult : ( a × a) set → ( a multiset × a multiset) set. It is defined as the transitive closure of the one-step Dershowitz-Manna extension defined by Nested Multisets, Hereditary Multisets, and Syntactic Ordinals multiset. It is defined using an iterator on finite sets, adding each mapped element f x with the multiplicity of x in the initial multiset A (given by count A x):

mult1 R = {(A, B). ∃y B 0 X. B = B 0 + {y} ∧ A = B 0 + X ∧ ∀x ∈ X. (x, y) ∈ R}
definition image : ( a → b) → a multiset → b multiset where image f A = Finite_Set.fold (λx. (add (f x)) count A x ) {} (set A)
The structure (multiset, image, set, ℵ 0 ) forms a bounded natural functor [START_REF] Christian Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF][START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF]: image is the functorial action, set is the natural transformation, and ℵ 0 is an upper bound on the cardinality of the sets returned by set. Induction and recursion through a multiset are expressed in terms of set and image. The cardinality bound is needed to construct the datatype as the least fixed point of an isomorphism equation. Isabelle's datatypes do not allow genuinely negative occurrences in recursion, since this cannot be done consistently in HOL. However, some type constructors support both negative and positive views: a multiset can be viewed negatively as a fragment of a → nat or positively as a quotient of a list (with respect to the relation "contains the same elements with the same multiplicities as"). It is this latter view that is fruitful for recursion. It is easy to see that image then corresponds to the functorial action map on lists.

Isabelle's multiset theory is not as developed as other areas, such as lists and sets. Our first contribution has been to introduce some missing concepts and lemmas, which we added either directly to the Isabelle distribution or collected in a theory file in the Archive of Formal Proofs [START_REF] Christian Blanchette | Formalization of nested multisets, hereditary multisets, and syntactic ordinals[END_REF]. These include a replicate n x operator, which constructs the multiset consisting of n copies of x, and the cartesian product ×. We also showed that the Huet-Oppen extension [START_REF] Huet | Equations and rewrite rules: A survey[END_REF] of a partial order coincides with the Dershowitz-Manna extension as well as with the transitive closure of the one-step Dershowitz-Manna extension, allowing users to switch between the three characterizations. Remarkably, the characterizations do not coincide for arbitrary orders. Each characterization has its advantages. For example, the Huet-Oppen extension is unsuitable for defining the recursive path order [10, Section 2], whereas the Dershowitz-Manna extension is unsuitable for defining the Knuth-Bendix order [5, Section 2]. [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF] apply the multiset order to prove the termination of a tail-recursive reformulation of McCarthy's 91 function. Using Isabelle's definitional mechanism for recursive functions [23], the 91 function is specified as

Example 1 (McCarthy's 91 Function). Dershowitz and Manna

function g : nat → int → int where g n z = (if n = 0 then z else if z > 100 then g (n -1) (z -10) else g (n + 1) (z + 11))
To perform this definition, the command needs a well-founded relation R that includes g's call graph; otherwise, we could define a function f such that f n = f n + 1 and use this to derive 0 = 1, a contradiction. The default automation [START_REF] Bulwahn | Finding lexicographic orders for termination proofs in Isabelle/HOL[END_REF][START_REF] Krauss | Certified size-change termination[END_REF] is not powerful enough to synthesize the relation, so we provide R ourselves. Following Dershowitz and Manna (but correcting '< 111' to '≤ 111'), we define the relation as

R = ((n, z), (n , z )). (τ n z, τ n z ) ∈ mult {(a, b). b < a ∧ a ≤ 111}
where τ is defined as follows, together with an auxiliary function f:

definition f : int → int where f x = (if x > 100 then x -10 else 91) definition τ : nat → int → int multiset where τ n z = mset (map (λi. f i z) [0 . . n -1])
The mset function in τ 's definition converts a list to a multiset of its elements.

The main proof obligation is to show that g's call graph is included in R-i.e., that the arguments (n, z) become smaller with each recursive call according to the measure τ n z and the multiset order. We followed the original proof, relying on existing lemmas about mult.

11:5

The verified SAT solver framework [START_REF] Christian Blanchette | A verified SAT solver framework with learn, forget, restart, and incrementality[END_REF] developed mainly by Fleury as part of the IsaFoL (Isabelle Formalization of Logic) effort represents clauses as multisets of literals and problems as multisets of clauses. To improve automation, we developed simplifier plugins, or "simprocs," that cancel terms that appear on both sides of a subtraction, equality, or inequality, rewriting the expression A + {x} + B = add x A to B = {} and A + {x} + B -add x A to B. Since multiset multiplicities are natural numbers, we started with the cancellation simprocs for nat, due to Lawrence Paulson, and generalized them to arbitrary members of the type class of cancellative commutative monoids-including nat, a multiset, and the hereditary and signed multiset types introduced in Sections 5 and 7. The properties required by the type class are 0 + a = a, (a + b)

+ c = a + (b + c), a + b = b + a, (a + b) -a = b, and a -b -c = a -(b + c).
The simprocs for nat depend on a 'k ×' operation. We first needed to define its multiset counterpart, repeat : nat → a multiset → a multiset, and to prove lemmas about it. The multiset instances of our simprocs collectively perform the following steps:

1. Normalize the goal by rewriting add a X to {a} + X and replicate n a to repeat n {a}.

Extract A and B from any occurrence of the pattern A ∼ B in the goal to normalize,

where ∼ is among -, =, <, ≤, ⊂, and ⊆.

Extract the summands in

A = A 1 + • • • + A m and B = B 1 + • • • + B n to form two lists of multiplicity-term pairs.
4. Find common terms on both sides, subtract the coefficients, and remove the element in the goal using an explicit lemma instantiation.

5.

Recombine the simplified terms with ∼.

6.

Normalize {a} back to add a {} and simplify add (e.g., replacing M + add a {} + N with add a (M + N )).

In general, the normalization steps are parameterized by rewrite rules, which must be provided for each type instance.

Nested Multisets

The type of nested multisets defined in Section 1 is freely generated by the constructors Elem : a → a nmultiset and MSet : ( a nmultiset) multiset → a nmultiset. The characteristic theorems derived by the datatype command [START_REF] Christian Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF] include the induction rule

( x. P (Elem x)) = ⇒ ( M. ( N ∈ NM . P N ) = ⇒ P (MSet NM )) = ⇒ P N
In the MSet NM case, the induction hypothesis applies to all elements N of the multiset NM . Strictly speaking, the condition is N ∈ set NM , where set is the natural transformation associated with the functor multiset, but we overload the symbol ∈ for multisets. The command also defines a recursor rec : Using the recursor, we can specify primitive recursive functions on nested multisets. A useful example is the depth of a nested multiset, depth : a nmultiset → nat, defined by

( a → b) → (( a nmultiset × b) multiset → b) → a nmultiset
depth = rec (λx. 0) (λM. let X = set (image snd M ) in if X = {} then 0 else Max X + 1)
where snd : a × b → b is the second pair projection and Max returns the maximum element of a nonempty finite set equipped with a linear order. Even for a simple example like this, F S C D 2 0 1 7

11:6

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals the recursor-based definition is cryptic. Isabelle's primrec command allows users to specify primitive recursive functions by their equations, such as

depth (Elem x) = 0 depth (MSet M ) = (let X = set (image depth M ) in if X = {} then 0 else Max X + 1)
Internally, primrec defines depth in terms of rec and derives the user's equations from rec's characteristic equations.

The next function we consider is Dershowitz and Manna's nested multiset order [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]. We reproduce their definition below (partly adapting the notations):

For two nested multisets M, N over A, we say that M < < * N if 1. M, N ∈ A and M < N (two elements of the base set are compared using <); or else

M /

∈ A and N ∈ A (any multiset is greater than any element of the base set); or else

M, N /

∈ A, and for some nested multisets X, Y , where

{} = Y ⊆ N , M = (N -Y ) X and ∀x ∈ X. ∃y ∈ Y. x < < * y
The corresponding Isabelle definition is as follows (with < overloaded to also mean < < * ):

function < : a nmultiset → a nmultiset → bool where Elem a < Elem b ← → a < b | Elem a < MSet M ← → True | MSet M < Elem a ← → False | MSet M < MSet N ← → ext DM (<) M N
There are several things to note here. First, we use function instead of primrec because we are recursing on two nested multisets simultaneously. Second, ext DM R A B is the Dershowitz-Manna multiset order extension of R applied to multisets A, B. It is defined by

ext DM R A B ← → ∃X Y. Y = {} ∧ Y ⊆ B ∧ A = (B -Y ) + X ∧ ∀x ∈ X. ∃y ∈ Y. R x y
Third, the function command expects a termination proof in the form of a well-founded relation. We provide the well-founded lexicographic product sub × lex sub of the immediate subterm relations sub : (nmultiset × nmultiset) set defined as {(N, MSet NM ) | N ∈ NM }. The termination proof crucially relies on the fact that ext DM applies the relation passed as its first argument only to nested multisets contained in its second and third arguments. This is easy to prove for arbitrary relations for ext DM but would be harder for mult. And since we have not established the transitivity of the function we are defining yet, we cannot use the equivalence of mult and ext DM on partial orders. This explains the use ext DM in the definition. Fourth, after obtaining the termination proof, function generates an induction principle that matches the recursion schema used in the definition.

Next, we prove several closure properties of the nested multiset order. If < : a → a → bool is a (nonstrict) preorder, then < : a nmultiset → a nmultiset → bool yields a preorder. The same closure property holds for partial orders, total orders, and wellorders (i.e., well-founded total orders). Each closure property corresponds to a type class instantiation, and each type class instantiation gives us a wealth of lemmas and helpful reasoning infrastructure about the nested multiset order.

Only the proofs of transitivity and well-foundedness of the nested multiset order are challenging. For transitivity, we rely on ext DM 's equivalence to mult on transitive relations. We prove transitivity by induction, and the induction hypothesis establishes that ext DM is only applied to a transitive relation. To prove well-foundedness, we start with an auxiliary lemma: < is well-founded on the set of nested multisets of a fixed depth i. Formally:

wf {(M, N ) | depth M = i ∧ depth N = i ∧ M < N }.
The proof proceeds by induction on i and uses the equivalence of ext DM and mult (on transitive relations) as well as the proof of preservation of well-foundedness by mult. Finally, we obtain the well-foundedness of the entire relation by observing that depth M < depth N implies M < N and hence M < N can be rewritten to depth M < depth N ∨ depth M = depth N ∧ M < N . In other words, we lexicographically compare the depths and resort to the nested multiset order to break ties. The claim follows, since with the above lemma both components of the lexicographic comparison are well founded.

Hereditary Multisets

Many authors rely on nested multisets and the order on them in one way or another. However, most of them do not use the Elem constructor, or use it in an easily avoidable way. In this section, we consider nested multisets with no Elem constructor. In set theory, we could simply let a be the empty set to model this. Since this is not possible in HOL, we define Elem-freedom as an inductive predicate:

inductive no_elem : a nmultiset → bool where ( N ∈ NM . no_elem N ) = ⇒ no_elem (MSet NM )
In principle, we could now use typedef to carve out a new type consisting of nested multisets satisfying no_elem. However, the resulting type would be isomorphic to the datatype of hereditary multisets as introduced in Section 1, with its single injective constructor HMSet : hmultiset multiset → hmultiset. We prefer the datatype definition, since it offers convenient recursion and induction schemas. Nonetheless, the subtype view on hereditary multisets is also useful, as it allows us to lift the infrastructure from nested to hereditary multisets.

Formally, we establish this view by providing an isomorphism, as two mutually inverse injections Abs : The Lifting tool [START_REF] Huffman | Lifting and Transfer: A modular design for quotients in Isabelle/HOL[END_REF] exploits these properties to lift constants on nested multisets to hereditary multisets. Here is our definition of the hereditary multiset order:

lift_definition < : hmultiset → hmultiset → bool is < : unit nmultiset → unit nmultiset → bool
The lift_definition command produces the definition M < N ← → Rep M < Rep N, which hides the isomorphism. Moreover, the command also provides a setup for the companion Transfer tool [START_REF] Huffman | Lifting and Transfer: A modular design for quotients in Isabelle/HOL[END_REF], which reduces proof goals about the abstract type (hmultiset) to goals about the raw type (unit nmultiset). Nevertheless, the proof of the expected property HMSet M < HMSet N ← → ext DM (<) M N is not trivial, because we must ensure that the witnesses for the existential quantifiers in the definition of ext DM contain no Elem. With this property in place, it is easy to lift the instantiations of the various order type classes (up to and including wellorders) from nested to hereditary multisets. Finally, we prove that hmultiset is a cancellative commutative monoid by lifting the corresponding structure from the multiset type-i.e., by defining 0 = HMSet {}, HMSet A + HMSet B = HMSet (A + B), and HMSet A -HMSet B = HMSet (A -B). This enables natural-number-like reasoning with multisets, including our generalized cancellation simprocs.

Syntactic Ordinals

Hereditary multisets are isomorphic to the ordinals below 0 , which we call the syntactic ordinals. Instead of defining a new type, we use hmultiset whenever we need such ordinals and provide the main ordinal operations on this type. Our notion of syntactic ordinal is similar to Dershowitz and Moser's "ordinal terms" [START_REF] Dershowitz | The Hydra Battle revisited[END_REF], which they attribute to Takeuti [START_REF] Takeuti | Proof Theory[END_REF]Section 2.11], but unlike them we do not need to consider the ordinal 0 specially. The empty hereditary multiset 0 corresponds to the ordinal 0. Union + corresponds to Hessenberg addition, which is traditionally denoted by ⊕; we write + to exploit the Isabelle type classes for addition. The multiset order < conveniently coincides with its ordinal counterpart. Multiset subtraction also makes sense as a truncating subtraction on ordinals; for example, 1 -3 = 0, ω -3 = ω, and ω 2 + 3 -ω = ω 2 + 3. Notice that if α < β, then it is not necessarily the case that α -β = 0. To provide more complete support for ordinals, we define some additional constants and abbreviations on hmultiset, starting with the following basic concepts: ω α = HMSet {α}; 1 = ω 0 ; ω = ω 1 . Given 1 and +, Isabelle lets us enter arbitrary numerals and interprets them as

1 + • • • + 1.
The Hessenberg product is defined by taking the cartesian product of the operands' multisets and applying addition on the resulting pairs to obtain a multiset of ordinals, i.e., an ordinal: α • β = HMSet (image (+) (hmsetmset α × hmsetmset β)), where hmsetmset is HMSet's inverse. The expected properties are easy to prove: Multiplication is associative, commutative, and distributive over addition; 0 is absorbent; 1 is neutral; 0 = 1; etc.

It is interesting to compare our definition of the Hessenberg product with the literature. The following definition, by Ludwig and Waldmann [START_REF] Ludwig | An extension of the Knuth-Bendix ordering with LPO-like properties[END_REF], illustrates how suboptimal abstractions can lead to convoluted formulations:

For α ∈ O \ {0} we define: 0 0 = 0 0 α = 0 α 0 = 0 Let for m, m ∈ N >0 , n 1 , . . . , n m , n 1 , . . . , n m ∈ N >0 , b 1 , . . . , b m , b 1 , . . . , b m ∈ O such that b 1 > b 2 > • • • > b m and b 1 > b 2 > • • • > b m , a = m i=1 (ω bi • n i ), b = m i=1 (ω b i • n i ) We define then α β = m i=1 m j=1 ω bi⊕b j • coeff(α, b i ) + coeff(β, b j )
Subtraction is so ill behaved that multiplication does not distribute over it: For α = ω 2 +ω, β = 1, and γ = ω, we have α

• (β -γ) = ω 2 + ω = ω = α • β -α • γ.
As a result, some Isabelle type classes for subtraction cannot be instantiated for ordinals.

Given an ordinal n i=1 (ω αi • c i ) in Cantor normal form, its degree corresponds to the largest exponent, α 1 . Unfortunately, this definition does not gracefully handle the case where n = 0. We could extend the ordinal type with a special value (e.g., -∞), but this would require a different type and operations on that type. Instead, we introduce the concept of a head ω-factor. For 0, the head ω-factor is 0; for nonzero ordinals of degree α, it is ω α , which is always nonzero. The degree is the maximum element in the multiset that corresponds to the ordinal. Formally: head ω α = if α = 0 then 0 else ω Max (set (hmsetmset α)) .

The following decomposition lemma, which was brought to our attention by Uwe Waldmann, is useful when comparing ordinals. Given two ordinals α 1 , α 2 such that α 1 < α 2 , we can always express them as sums of the form α i = γ + β i , where the head ω-factor of β 1 is smaller than that of β 2 : lemma hmset_pair_decompose_less:

α 1 < α 2 = ⇒ ∃γ β 1 β 2 . α 1 = γ + β 1 ∧ α 2 = γ + β 2 ∧ head ω β 1 < head ω β 2
Example 2 (Hydra Battle). The hydra battle [START_REF] Kirby | Accessible independence results for Peano arithmetic[END_REF] is a classic process whose termination cannot be proved by induction on the natural numbers. Following Dershowitz and Moser's reformulation [START_REF] Dershowitz | The Hydra Battle revisited[END_REF], we use Lisp-style lists (unlabeled binary trees) to represent hydras: datatype lisp = Nil | Cons lisp lisp. The functions car and cdr are defined to extract the first and second arguments of Cons, respectively; they return Nil when invoked on a Nil node.

A hydra consists of a list of heads. In a departure from standard Greek mythology, each head is recursively a list of heads. The battle also involves a hero, Hercules, who gets to chop off one of the hydra's "leaf" heads at each round. If the head has no grandparent node, the head is lost and there is no regrowth; otherwise, the branch issuing from the grandparent node is copied n times, where n starts at 1 and is increased by 1 in each round. We refer to the literature for more details (and some nice drawings of polycephalic monsters).

Formally, the battle is captured by the h function below, which depends on an auxiliary function d:

function d nat → lisp → lisp where d n x = (if car x = Nil then cdr x else if car (car x) = Nil then (Cons (cdr (car x))) n (cdr x) else Cons (d n (car x)) (cdr x)) function h : nat → lisp → lisp where h n x = (if x = Nil then Nil else h (n + 1) (d n x))
For d, termination is easy: The left subtree of x becomes smaller with each iteration, so we can take {((n , x ), (n, x)). |x | < |x|} as the relation, where |x| returns the number of nodes of a list x. For h, instead of |x|, we use encode x as the measure, where encode is defined by the primitive recursive equations encode Nil = 0 and encode (Cons l r) = ω encode l + encode r. Thanks to well-foundedness of <, it suffices to show that the ordinal decreases in each recursive call to h-i.e., if x = Nil, then encode (d n x) < encode x. The proof is by structural induction on x. The Nil case is trivial. In the Cons l r case, if l = Nil, we have 0 < ω 0 + encode r. Otherwise, we distinguish two subcases. If car l = Nil, we must prove encode (f n (cdr l) r) < ω encode l + encode r, which amounts to n • ω encode (cdr l) + encode r < ω ω encode (car l) + encode (cdr l) + encode r. The right-hand side is greater because the exponent to ω has an additional nonzero term, ω encode (car l) , which dwarfs the n factor on the left. In the remaining case, we have car l = Nil. The proof obligation amounts to encode (d n l) < encode l, corresponding to the induction hypothesis for the left subtree.

The termination proof is about 30 lines long in Isabelle. As is often the case, the formalization revealed some inaccuracies in the informal argument. Although this is not mentioned by Dershowitz and Moser, the termination proof depends on car Nil = Nil. They also claim that Cons Nil Nil represents a "leaf of a hydra," but the car x = Nil test in d's definition can only mean that a simple Nil node is used for leaves.

Example 3 (Ludwig and Waldmann).

The following Isar proof outline closely follows the pen-and-paper proof of a property Ludwig and Waldmann needed to reason about their transfinite Knuth-Bendix order [START_REF] Ludwig | An extension of the Knuth-Bendix ordering with LPO-like properties[END_REF]. The informal proof was communicated to us privately by Waldmann. A more restrictive formulation is claimed as Lemma 10 in their paper. The steps are justified by short proofs, omitted below, most of which were generated by Sledgehammer. Using Isabelle's built-in automation and the cancellation simprocs, it would be possible to eliminate some of the intermediate steps.

lemma assumes α 2 + β 2 • γ < α 1 + β 1 • γ and β 2 ≤ β 1 and γ < δ shows α 2 + β 2 • δ < α 1 + β 1 • δ F S C
β 2 = β 0 + β 2 and head ω β 2 < head ω β 1 ∨ β 2 = 0 ∧ β 1 = 0 {by hmset_pair_decompose_less} have α 2 + β 0 • γ + β 2 • γ = α 2 + β 2 • γ {by β 2 = β 0 + β 2 } also have < α 1 + β 1 • γ {by α 2 + β 2 • γ < α 1 + β 1 • γ} also have = α 1 + β 0 • γ + β 1 • γ {by β 1 = β 0 + β 1 } finally have α + β 2 • γ < α 1 + β 1 • γ {by cancellation} have α 2 + β 2 • δ = α 2 + β 0 • δ + β 2 • δ {by β 2 = β 0 + β 2 } also have = α 2 + β 0 • δ + β 2 • η + β 2 • δ {by δ = η + δ } also have ≤ α 2 + β 0 • δ + β 2 • η + β 2 • δ + β 2 • γ {by monotonicity} also have = α 2 + β 2 • γ + β 0 • δ + β 2 • δ {by γ = η + γ } also have < α 1 + β 1 • γ + β 0 • δ + β 2 • δ {by α 2 + β 2 • γ < α 1 + β 1 • γ} also have = α 1 + β 1 • η + β 1 • γ + β 0 • η + β 0 • δ + β 2 • δ {by γ = η + γ , δ = η + δ } also have ≤ α 1 + β 1 • η + β 0 • η + β 0 • δ + β 1 • δ {by head ω (β 1 • γ + β 2 • δ ) < head ω (β 1 • δ ) ∨ β 1 • γ = β 2 • δ = β 1 • δ = 0} finally show α 2 + β 2 • δ < α 1 + β 1 • δ {by β 1 = β 0 + β 1 , δ = η + δ } qed 7

Signed Variants of Multisets and Hereditary Multisets

Syntactic ordinals do not enjoy the property that Ludwig and Waldmann refer to as "continuity" [START_REF] Ludwig | An extension of the Knuth-Bendix ordering with LPO-like properties[END_REF]: Given syntactic ordinals α, β such that α < β, there does not necessarily exist an ordinal γ such that α + γ = β. Yet, syntactic ordinals correspond formally to polynomials over the indeterminate ω. Why not allow negative coefficients (e.g., ω 2 -2ω + 1) and take γ = β -α? The practical motivation arose in the context of the formalization of a transfinite Knuth-Bendix order [START_REF] Becker | Formalization of Knuth-Bendix orders for lambda-free higher-order terms[END_REF][START_REF] Becker | A transfinite Knuth-Bendix order for lambda-free higher-order terms[END_REF]. Although it is a simple idea, we could not find it in the literature. We start by defining the signed multisets, also called the hybrid multisets [START_REF] Banâtre | Generalised multisets for chemical programming[END_REF]. In principle, we could define them in a similar way as the plain multisets (Section 3), by substituting int for nat in the typedef command. However, we prefer to perform a quotient construction, so as to be able to lift operations and lemmas about plain multisets:

quotient_type a zmultiset = a multiset × a multiset / R
where R = λ(P 1 , N 1 ) (P 2 , N 2 ). P 1 + N 2 = P 2 + N 1 . The quotient_type command [START_REF] Kaliszyk | Quotients revisited for Isabelle/HOL[END_REF] introduces a type that is isomorphic to the set of R-equivalence classes. In the same way as a pair (m, n) of natural numbers can represent the integer m -n, we use a pair (P, N ) of plain multisets to capture the signed multiset P -N, whose multiplicities can be negative. For example, both ({}, {7}) and ({3}, {3, 7}) correspond to the signed multiset that contains 7 with multiplicity -1 and no other element. Notice that R ({}, {7}) ({3}, {3, 7}), since {} + {3, 7} = {7} + {3}. The pos and neg functions, of type a zmultiset → a multiset, return normalized P and N components, with P ∩ N = {}.

The main signed multiset operations are defined by specifying them on the raw level of multiset pairs and lifting them to the abstract level of equivalence classes. The Lifting tool emits a proof obligation stating that equivalence classes are respected. For example, for unary functions f on multisets, this means that when f is invoked on R-equivalent arguments x and y, the results f x and f y are R-equivalent. A few definitions are given below:

lift_definition 0 : a zmultiset is ({}, {}) lift_definition -: a zmultiset → a zmultiset → a zmultiset is λ(P 1 , N 1 ) (P 2 , N 2 ). (P 1 + N 2 , N 1 + P 2 ) lift_definition zcount : a zmultiset → a → int is λ(P, N ) x. int (count P x) -int (count N x)
Many lemmas about such definitions can be lifted from the raw types using the Transfer tool, which exploits relational parametricity [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] to transfer results across types. Most HOL functions arising in practice are parametric. The type zhmultiset of signed hereditary multisets is defined using the typedef command as isomorphic to hmultiset zmultiset. Notice that the multisets contained in such a signed multiset are not signed. It is unclear to us whether "hereditarily signed" multisets, and "ordinals" in which the exponents of ω can recursively contain negative coefficients, would be worth studying.

The ι function embeds hmultiset into zhmultiset. Operations such as +, -, and < are lifted from the underlying multisets. Ordinal multiplication is by far the most problematic operation. It can be defined in terms of the cartesian product on signed multisets:

lift_definition • : zhmultiset → zhmultiset → zhmultiset is λM N : hmultiset zmultiset. ι (hmsetmset (HMSet (pos M ) • HMSet (pos N ))) -ι (hmsetmset (HMSet (pos M ) • HMSet (neg N ))) + ι (hmsetmset (HMSet (neg M ) • HMSet (neg N ))) -ι (hmsetmset (HMSet (neg M ) • HMSet (pos N )))
It is difficult to prove the associativity of this multiplication operator. Using the Transfer tool, we can quickly reduce the proof obligation to the following property of unsigned ordinals:

α 2 • (β 2 • γ 2 + β 1 • γ 1 -(β 2 • γ 1 + γ 2 • β 1 )) + γ 2 • (α 2 • β 1 + β 2 • α 1 -(α 2 • β 2 + α 1 • β 1 )) + α 1 • (β 2 • γ 1 + γ 2 • β 1 -(β 2 • γ 2 + β 1 • γ 1 )) + γ 1 • (α 2 • β 2 + α 1 • β 1 -(α 2 • β 1 + β 2 • α 1 )) = α 2 • (β 2 • γ 1 + γ 2 • β 1 -(β 2 • γ 2 + β 1 • γ 1 )) + γ 2 • (α 2 • β 2 + α 1 • β 1 -(α 2 • β 1 + β 2 • α 1 )) + α 1 • (β 2 • γ 2 + β 1 • γ 1 -(β 2 • γ 1 + γ 2 • β 1 )) + γ 1 • (α 2 • β 1 + β 2 • α 1 -(α 2 • β 2 + α 1 • β 1 ))
After staring at this goal for a few hours, we speculated that the property α

• (γ -β) + α • β = α • (β -γ) + α
• γ holds about truncating subtraction. We proved it and applied it four times to make the left-hand side of the proof obligation above syntactically identical to the right-hand side.

Here is a selection of the properties we proved using Isabelle, with α, β, γ ranging over signed ordinals:

1. α + β = β + α; 2. (α + β) + γ = α + (β + γ); 3. α • β = β • α; 4. (α • β) • γ = α • (β • γ); 5. (α + β) • γ = α • γ + β • γ; 6. α < β ← → α + γ < β + γ; 7. 0 + α = α; 8. 0 • α = 0; 9. 1 • α = α; 10. α ≤ β ← → α < β + 1; 11. α • β = 0 ← → α = 0 ∨ β = 0; 12. α < β ∧ 0 < γ = ⇒ γ • α < γ • β; 13. α -β + β = α; 14. α -β + γ = α + γ -β; 15. α + β -γ = α + (β -γ); 16. α -β -γ = α -(β + γ).
Finally, we instantiated our generalized cancellation simprocs for zmultiset and zhmultiset. As preprocessing steps, we normalize unary minuses, rewriting -α + β + α to (β + α) -α; the subtraction simproc then cancels the two α's, yielding β.

have ι α 2 + ι β 2 • ι δ = ι α 2 + ι β 2 • ι γ + ι β 2 • (ι δ -ι γ)
{by algebraic manipulations} also have

< ι α 1 + ι β 1 • ι γ + ι β 2 • (ι δ -ι γ) {by α 2 + β 2 • γ < α 1 + β 1 • γ} also have ≤ ι α 1 + ι β 1 • ι γ + ι β 1 • (ι δ -ι γ) {by β 2 ≤ β 1 , γ < δ} also have = ι α 1 + ι β 1 • ι δ {by algebraic manipulations} finally show α 2 + β 2 • δ < α 1 + β 1 • δ {by algebraic manipulations}
The next-to-last step eliminates the subtraction ι δ -ι γ, paving the way for the final step, which removes the ι casts. Waldmann privately confirmed that he was aware of this shortcut but did not dare take it without a solid theoretical foundation for signed ordinals.

Application to Goodstein's Theorem

Goodstein's theorem [START_REF] Goodstein | On the restricted ordinal theorem[END_REF] states that every Goodstein sequence eventually terminates at 0. Before we can define these sequences, we must first introduce an auxiliary notion. A natural number is in hereditary base n if it is expressed as a product

c 1 n k + c 2 n k-1 + • • • + c k-1 n + c k ,
where 0 ≤ c i < n for each i, c 1 = 0, and the exponents k, k -1, . . . , 1 are recursively expressed in hereditary base n. For example, 500 is written as 2 • 3 3+2 + 3 2 + 3 + 2 in hereditary base 3. The Goodstein sequence G s of natural numbers is defined as follows. The starting value is given by s: G s (0) = s. The remaining values G s (i + 1) are obtained by expressing G s (i) in base i + 2, replacing all occurrences of i + 2 by i + 3, and subtracting 1. For example, we have

G 4 (0) = 4 = 2 2 , G 4 (1) = 3 3 -1 = 26 = 2 • 3 2 + 2 • 3 + 2, and G 4 (2) = 2 • 4 2 + 2 • 4 + 2 -1 = 41.
Somewhat counterintuitively, the sequence eventually converges to 0: G 4 (3•2 402 653 211 -1) = 0.

Our formal proof relies on two functions encode and decode that convert between natural numbers and hereditary base n. The adjective 'hereditary' suggests that hereditary multisets, or syntactic ordinals, are a suitable data structure. Following this idea, 2 • ω 2 + 2 • ω + 2 represents 2 • 3 2 + 2 • 3 + 2 in hereditary base 3, or 2 • 5 2 + 2 • 5 + 2 in hereditary base 5.

The encode and decode functions are defined in a local context that fixes a constant base ≥ 2. Beyond the end of the local context, we must supply the base explicitly as additional argument to encode and decode, which we will indicate as a subscript. The argument e gives the exponent of the current base, starting from 0. The recursion scheme for encode is nonprimitive. Termination is established using the measure λ(e, n). n•(base e +1). The Goodstein sequence is defined as follows, where start is fixed: primrec goodstein : nat → nat where goodstein 0 = start | goodstein (i + 1) = decode i+3 0 (encode i+2 0 (goodstein i)) -1

If goodstein i > 0, then the ordinal associated with goodstein (i + 1) is smaller than the one for goodstein i. Let E i = encode i+2 0 (goodstein i). The proof sketch is as follows: lemma goodstein_step:

assumes goodstein i > 0 shows E i > E i+1 proof have decode i+3 0 E i > 0 {by decode_0_iff } have E i = encode i+3 0 (decode i+3 0 E i ) {by encode_decode_exp_0 } also have > encode i+3 0 (decode i+3 0 E i -1) {by less_imp_encode_less, decode i+3 0 E i > 0} finally show E i > E i+1 {by definition of E i+1 } qed
The main lemmas that are directly or indirectly needed are listed below: The first and second properties are the most difficult ones. The first one is proved by well-founded induction, following the recursion structure of encode. This induction principle is derived automatically by the function command. The second property is proved by strong induction on α. The assumptions ensure that the coefficients stored in α are smaller than the base (well_base) and that the last e digits are all 0s (aligned).

The entire formalization is about 580 lines long. The main difficulty was to come up with the right lemmas and inductions. Reasoning about ordinals was fairly comfortable. Nevertheless, we are very impressed by Zankl, Winkler, and Middeldorp's automatic proof of the termination of a term rewriting system that computes Goodstein's sequence [START_REF] Zankl | Beyond polynomials and Peano arithmetic-Automation of elementary and ordinal interpretations[END_REF]. Possibly the key to their success is that they avoid converting back and forth between the natural numbers and hereditary base notation.

9

Application to Decidability of Unary PCF Plotkin's PCF language of "programming computable functions" [START_REF] Plotkin | LCF considered as a programming language[END_REF] is a simply typed λ-calculus that has natural numbers N as a base type and permits recursion on them. Types are interpreted as Scott domains, i.e., N = N ∪ {⊥}. For unary PCF, a fragment of PCF which has only the base type o with the single value (in addition to the domain's ⊥), behavioral equivalence is decidable [START_REF] Loader | Unary PCF is decidable[END_REF][START_REF] Schmidt-Schauß | Decidability of behavioural equivalence in unary PCF[END_REF]. Schmidt-Schauß's elegant proof [START_REF] Schmidt-Schauß | Decidability of behavioural equivalence in unary PCF[END_REF] is based on an inductive enumeration of representative terms. The termination of the enumeration is ensured by abstracting types into hereditary multisets. In our ongoing formalization effort of this decidability result (which poses many challenges unrelated to multisets), we proved Schmidt-Schauß's key Lemma 11 about hereditary multisets.

Types of unary PCF are defined as datatype type = o | type ⇒ type, where ⇒ is a rightassociative infix datatype constructor. Given a type T , we define its argument types T i and its arity ar T such that T Nested Multisets, Hereditary Multisets, and Syntactic Ordinals equivalence classes. The construction is recursive and relies on a decrease in the involved types' measures for termination. More precisely, given T , the construction recursively computes sets of representative terms for types π j i T for all i < ar T and j ≤ ar T i , where the operator π is defined recursively as follows: The key step to help automation is to define X, Y, and Z (all of type hmultiset multiset) such that after unfolding the Dershowitz-Manna definition of the multiset order, the inequality is easily fulfilled (given the induction hypotheses).

= T 0 ⇒ • • • ⇒ T ar T -1 ⇒ o.
fun π : nat → nat → type → type where π 0 i T = (if i < ar T then T 0 ⇒ • • • ⇒ T i-1 ⇒ T i+1 ⇒ • • • ⇒ T ar T -1 ⇒ o else o) | π j+1 i T = (if i < ar T ∧ j < ar T i then π 0 j T i ⇒ • • • ⇒ π ar (Ti)j j T i ⇒ π 0 i T else o) Finally,
: δ (π 0 j T i ) < δ T i and IH 2 : ∀k < ar (T i ) j . δ (π k+1 j T i ) < δ T i define X = {δ (π 0 j T i )} + image (λk. δ (π k+1 j T i )) {0
Our formal proof is very close to Schmidt-Schauß's informal argument. It is rare to be able to formalize a technical proof so closely. This can be due to the care taken by the informal proof writer, due to good formal library support, or due to a combination of both.

Related Work

The nonnested multiset order has been formalized in several proof assistants, including Coq [START_REF] Blanqui | CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF][START_REF] Contejean | Certification of automated termination proofs[END_REF], HOL4, and Isabelle/HOL [START_REF] Thiemann | On the formalization of termination techniques based on multiset orderings[END_REF]. The Isabelle version is generalized to take two parameters: a strict and a nonstrict order. The resulting order is strictly more powerful for termination proving than the standard version. Another aspect where the related work goes further than our work is executability. In principle, little stands in the way of a decent code generation setup for our multiset variants, following the lines of the existing multiset setup. Norrish and Huffman [START_REF] Norrish | Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω[END_REF] present two formalizations of ordinals, in HOL4 and Isabelle/ HOL. The HOL4 formalization models ordinals as quotients of wellorders with respect to wellorder isomorphism. The Isabelle/HOL development also relies on a quotient construction, but from a more syntactic notion of raw ordinals, defined as datatype preordinal = Zero | StrictLim (nat → preordinal). Independently, Blanchette, Popescu, and Traytel [START_REF] Christian Blanchette | Cardinals in Isabelle/ HOL[END_REF] formalized ordinals and cardinals in Isabelle/HOL, representing ordinals by well-ordered relations dispersed over arbitrary types. Thereby they avoided fixing an a priori bound on the ordinals that can be constructed. All these formalizations go beyond 0 but are ultimately limited by the expressiveness of HOL, which is strictly weaker than set theory. Another difference with our current work is that they provide the standard addition and product and not Hessenberg's.

In Coq, Castéran and Contejean [START_REF] Castéran | On ordinal notations[END_REF] formalized ordinal notations up to Γ 0 . As case studies, they considered the hydra battle and Goodstein's theorem. Grimm [START_REF] Grimm | Implementation of three types of ordinals in Coq[END_REF] ported and extended this work, covering three alternative notions of ordinals. Also in Coq, Vermaat [START_REF] Vermaat | Infinitary Rewriting in Coq[END_REF] formalized tree ordinals, a syntactic representation similar to Norrish and Huffman's. Recently, Schmitt [START_REF] Peter | A first-order theory of ordinals[END_REF] axiomatized ordinals in KeY and proved Goodstein's theorem.

Conclusion

We presented a formalization in Isabelle/HOL of nested multisets, hereditary multisets, and ordinals below 0 . Their datatype definitions emphasize the close connections between the three notions. The signed generalizations of these types, with potentially negative multiplicities, offer a subtraction operator that enjoys nice algebraic properties. The signed syntactic ordinals do not appear to have been studied before.

The Lifting and Transfer tools were invaluable for carrying definitions across different multiset types. We relied heavily on Sledgehammer; it sometimes generated complex Isar proofs, which we occasionally inserted in our development. The cancellation simprocs also played a role, after we had adapted them so that they work on multisets. Well-founded recursion using function was vital, as it often is. But perhaps the most noteworthy aspect of our work is that all the necessary types could be introduced easily, either as inductive datatypes, as subsets of existing types, or as quotients. The support for recursion through bounded natural functors, a distinguishing feature of Isabelle/HOL, was crucial to define nested and hereditary multisets in a simple way, with convenient induction and recursion schemas.

α

  ::= {α 1 , . . . , α 1 c1 occurrences , . . . , α n , . . . , α n cn occurrences

For both RF

  and mult1 R, the smaller value is on the left. The operation set : a multiset → a set returns the set of elements in a multiset. The operation image : ( a → b) → a multiset → b multiset applies a function elementwise to a

  → b and derives its characteristic equations: rec e ms (Elem x) = e x rec e ms (MSet NM ) = ms (image (λN. (N , rec e ms N )) NM )

  unit nmultiset → hmultiset and Rep : hmultiset → unit nmultiset defined by Abs (MSet M ) = HMSet (image Abs M ) and Rep (HMSet M ) = MSet (image Rep M ). The isomorphism follows by easy inductions (on hmultiset or on the definition of no_elem): lemma M : hmultiset. no_elem (Rep M ) M : hmultiset. Abs (Rep M ) = M N : unit nmultiset. no_elem N = ⇒ Rep (Abs N ) = N

F

D 2 0 1 7 11: 10 Nested

 710 Multisets, Hereditary Multisets, and Syntactic Ordinals proof obtain η γ δ where γ = η + γ and δ = η + δ and head ω γ < head ω δ obtain β 0 β 1 β 2 where β 1 = β 0 + β 1 and

FExample 4 (

 4 Ludwig and Waldmann, Continued). By exploiting signed ordinals, we obtain a much simpler proof of Ludwig and Waldmann's property from Example 3:

context fixes base : nat assumes base ≥ 2

 2 begin function encode : nat → nat → hmultiset where encode e n = (if n = 0 then 0 else (n mod base) • ω encode 0 e + encode (e + 1) (n/base)) primrec decode : nat → hmultiset → nat where decode e (HMSet M ) = α∈M base decode 0 α base e end

  lemma less_imp_encode_less: n < p = ⇒ encode e n < encode e p lemma less_imp_decode_less: well_base α = ⇒ aligned e α = ⇒ aligned e β = ⇒ α < β = ⇒ decode e α < decode e β lemma decode_0 _iff : well_base α = ⇒ aligned e α = ⇒ (decode e α = 0 ← → α = 0) lemma decode_encode: decode e (encode e n) = n lemma encode_decode_exp_0 : well_base α = ⇒ encode 0 (decode 0 α) = α

F

  We measure a type using a primitive recursive function δ : type → hmultiset defined by δ o = 0 and δ (T ⇒ U ) = ω δ T + δ U . For a type T , Schmidt-Schauß constructs a set of representative closed terms of behavioral

  , . . . , ar (T i ) j -1} andY = {δ T i } and Z = image δ {T 0 , . . . , T i-1 , T i+1 , . . . , T ar T -1 } have δ (π j+1 i T ) = HMSet (X + Z){by definitions of δ and π} also haveX + Z < Y + Z {by Dershowitz-Manna characterization of <, IH 1 , IH 2 } also have HMSet (Y + Z) = δ T{by definition of δ} finally show δ (π j+1 i T ) < δ T {by above calculation} qed

  we prove that π indeed decreases the measure of types using the induction principle that follows the structure of π's definition and is provided by Isabelle's fun command[23].

	lemma δ_π:
	assumes i < ar T and j ≤ ar T i
	shows δ (π j i T ) < δ T
	proof (induct rule: π.induct)
	fix T i
	assume i < ar T
	show δ (π 0

i T ) < δ T {by definition of δ and π and simple multiset reasoning} next fix T i j assume i < ar T and j < ar T i and IH 1

Acknowledgment

Lawrence Paulson gave us the idea to formalize the nested multiset order. Aart Middeldorp pointed us to related work. Uwe Waldmann shared his insights about syntactic ordinals with us, including the lemma and the proof of Example 3. Robert Lewis, Mark Summerfield, Sophie Tourret, and the (extremely thorough) anonymous reviewers suggested dozens of textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).


Keywords:

Theoretical spectroscopic parameters for the low-lying states of isotopic variants of HCO+ and HOC+

Mirjana Mladenović

The theoretical spectroscopic parameters are derived for all isotopologues of HCO + and HOC + involving H, D, 16

  O, 17 O, 18 O, 12 C, and 13 C by means of a two-step procedure. Full-dimensional rovibrational calculations are first carried out to obtain numerically exact rovibrational energies for J=0-15 in both parities. Effective spectroscopic constants for the vibrational ground state, the calculated rovibrational energies to appropriate spectroscopic Hamiltonians. Combining our vibrationrotation corrections with the available experimental ground-state rotational constants, we also derive the new estimate for the equilibrium structure of HCO + , r e (CH)=1.091981(7Regarding the spectroscopic parameters, our estimates are in exelent agreement with available experimental results for both HCO + and HOC + : the agreement for the rotational constants B v is within 3 MHz, for the quartic centrifugal distortion constants D v within 1 kHz, and for the effective ℓ ℓ ℓ ℓ-doubling constants q v within 2 MHz. We thus expect that our results can provide useful assistance in analyzing expected observations of the rare forms of HCO + and HOC + that are not yet experimentally known. Theoretical spectroscopic parameters for the low-lying states of isotopic variants of HCO + and HOC +


R Abiri

X Zhao
email: xzhao9@utk.edu

Y Jiang

Controlling Gestures of a Social Robot in a Brain Machine Interface Platform

Introduction: Neural-based robotic platforms have become increasingly attractive option as a mean of direct communication between the brain and environment without any further physical contact. The information extracted from the brain signals will determine the degree and level of control in robot control tasks. Brain-robot interaction capability has shown great promise in development of forward control compatible with a patient's intentions and in cognitive training or rehabilitation using neurofeedback approach. Here, we propose a novel Brain Machine Interface (BMI) robotic platform using a personalized social robot in order to assist human participants during mind training. Brainwaves of a human participant were collected in a noninvasive-based BCI system during tasks of imaginary movements. The imagined body kinematics parameters were decoded to control a cursor on a computer screen during a fast training protocol (~ 10 minutes) and then the trained subject was allowed to interact with a social robot in our real-time BMI robotic platform. This wireless interaction not only can be useful for mind control of social robot's movements, but also could set foundations for the next stage application in rehabilitation of the cognitive abilities such as enhancing attention and memory of individuals with brain injury by providing real-time neurofeedback from social robot. Material, Methods and Results: During a fast training protocol, EEG signals were acquired by using an Emotiv EPOC device with 14 channels and through BCI2000 software (with high pass filter at 0.1Hz and low pass filter at 30Hz). By engaging the subject in our three-phase protocol including training, calibration, and test, the subject could achieve satisfactory control of a computer cursor after a short-time of training and based on imagined body kinematics paradigm. Then, the trained subject was allowed to make interaction with our BMI robotic platform to control the various gestures of a social robot in real-time course. As robotic interface, an affordable social robot called "Rapiro" was employed to provide neurofeedback to the subject. Simulink program was applied as interface software and was responsible to map the control signals (from BCI2000) to the correct pre-defined gesture in Rapiro. Figure 1 shows one example of real-time reactions of robot during mind-control of cursor in 2D space by a human subject. Discussion: As it is shown in Figure 1, a human subject was able to activate the correct gesture in social robot and achieved satisfactory performance. As the result of guiding cursor in wrong direction by the subject in some moments of inter-trial times, some discontinuities were observed in activating of robot neurofeedback. Significance: Several BMI platforms have been developed for patients with motor disorders during recover of the cortical plasticity underlying movements. However, limited research has applied robot as neurofeedback back to the human. Hence we offered a novel BCI robotic platform with possible future application for neurorehabilitation in patients with cognitive or mental disorders such as attention deficits. The presented BMI system using human-robot interaction can be further developed as a portable, wireless, and affordable platform to be used by patients.

Figure 1 .

 1 Figure 1. Mind controlled robot gestures (Right hand movement/left hand movement/both hands movement/head shaking) in real time. The figure illustrates cursor control task performance in 2D space during 12 trialsof a trained human subject. The mirrored robot movements served as simultaneous neurofeedback to the subject. It was programmed as such that the right target control activated the right hand movement; the left target control activated the left hand movement; the top target control lead to both hands movements and the bottom target control caused head shaking neurofeedback from the robot.

Acknowledgements: This work was in part supported by a NeuroNET seed grant to XZ; Supported by DoD D10-I-AR-J6-828, USUHS Grant HU0001-11-1-0007 to YJ