Christian Doczkal
email: christian.doczkal@ens-lyon.fr

Gert Smolka
email: smolka@ps.uni-saarland.de

Regular Language Representations in the Constructive Type Theory of Coq

Keywords: Regular Languages, Two-Way Automata, WS1S, Constructive Type Theory, Interactive Theorem Proving, Coq, Ssreflect

We explore the theory of regular language representations in the constructive type theory of Coq. We cover various forms of automata (deterministic, nondeterministic, oneway, two-way), regular expressions, and the logic WS1S. We give translations between all representations, show decidability results, and provide operations for various closure properties. Our results include a constructive decidability proof for the logic WS1S, a constructive refinement of the Myhill-Nerode characterization of regularity, and translations from twoway automata to one-way automata with verified upper bounds for the increase in size. All results are verified with an accompanying Coq development of about 3000 lines.

Introduction

Regular languages and their representations [START_REF] Hopcroft | Introduction to automata theory, languages, and computation -international edition[END_REF][START_REF] Kozen | Automata and computability[END_REF][START_REF] Khoussainov | Automata Theory and its Applications[END_REF] are an important topic in Computer Science. The representations of regular languages range from various forms of automata (deterministic, nondeterministic, one-way, two-way) to regular expressions and formulas in monadic second-order logic. The core of the theory consists of algorithms that translate between different representations, decide language properties like membership and emptiness, and realize language operations such as union, complement, concatenation, iteration, word reversal, right-quotient, and image and preimage under word homomorphisms. The translation of formulas to automata yields a decision method for WS1S, a logic with nonelementary complexity interesting in its own right. Minimal DFAs provide a normal form for DFAs that is unique up to renaming. There is also an abstract characterization of regular languages based on finite partitions (Myhill-Nerode relations).

We present a formal development of the aforementioned results in the constructive type theory of Coq [START_REF]The Coq Proof Assistant[END_REF]. We observe that constructive type theory provides for an elegant presentation of the theory of regular languages, improving on the usual set-theoretic presentation by addressing computational issues explicitly and by providing an expressive facility for inductive definitions. One aspect where the constructive approach leads to new insight is the Myhill-Nerode theorem, which in the literature is formulated as a nonconstructive characterization of regular languages. We refine the theorem such that we obtain a constructive characterization of regular languages with a class of finite partitions we call classifiers. Classifiers provide a big-step representation of DFAs useful for establishing decidability results and as intermediate representation for the translation of 2NFAs to DFAs.

First-class finite types and dependent types are essential for our development. Languages are formalized as predicates on words, words are formalized as lists over alphabets, and alphabets are formalized as finite types of symbols. Automata are formalized as structures involving an alphabet and a finite type of states. Classifiers and finite partitions are formalized as functions mapping words to elements of a finite type. Given a two-way automaton and an input word, we represent the possible configurations as a finite type. Here, dependent types are used to represent the finitely many possible head positions on the input word. In order to be able to quantify over automata, (e.g., in the definition of regularity) it is essential that finite types are first-class objects, which is not the case in HOL-based provers [START_REF] Wu | A formalisation of the Myhill-Nerode theorem based on regular expressions[END_REF].

The results we prove are known in the literature. Our efforts concern constructive proofs and the formalization of the results and definitions in constructive type theory. Considerable refinement was needed for the constructive formulation of the Myhill-Nerode theorem. Two of our main results, the characterization of regular languages with WS1S formulas [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF][START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF][START_REF] Trakhtenbrot | Finite automata and the logic of monadic predicates[END_REF] and with two-way automata [START_REF] Rabin | Finite automata and their decision problems[END_REF][START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF][START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF], have not been formalized before, although their technical complexity certainly calls for machined-checked proofs. In the case of two-way automata, we adapt the proofs of Vardi [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] and Shepherdson [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF] to tapes with endmarkers and generalize Shepherdson's proof from 2DFAs to 2NFAs.

Our main goal is an elegant presentation of the results in constructive type theory with machine-checked proofs. Constructive type theory ensures that all constructed functions are computable. Our focus is on clarity and simplicity, concrete executability is not a concern.

The paper develops the theory and the proofs in an informal mathematical language based on constructive type theory and is accompanied by a Coq development [START_REF] Doczkal | Coq development accompanying this paper[END_REF]. The paper and the Coq development are aligned such that it is easy to go back and forth. All numbered theorems in the paper correspond to theorems in the Coq development, and the proofs in the paper outline the Coq proofs. When appropriate, we discuss issues concerning the Coq development in the paper, but we do not give Coq code in the paper.

The Coq development employs the Ssreflect extension and makes essential use of the basic modules of the Mathematical Components library [36]. The development consists of about 3000 lines of code. The two biggest parts are the results about WS1S (870 lines) and two-way automata (550 lines).

As it comes to related work, we distinguish between work concerned with the theory of regular languages and work concerned with the formalization of regular language theory using interactive theorem provers. Papers from the first group will be mentioned in the technical sections of the paper they relate to, while papers from the second group will be discussed in Section 14.

The present paper extends and revises the material of two previous conference papers [START_REF] Doczkal | A constructive theory of regular languages in Coq[END_REF][START_REF] Doczkal | Two-way automata in Coq[END_REF] of the authors.

The paper is organized as follows. We start with type-theoretic preliminaries (Section 2) and fix notations for languages (Section 3). We then define the notion of regularity using DFAs (Section 4). Afterwards, we consider classifiers (Section 5), NFAs (Section 6), and regular regular expressions (Section 7) and show that they yield representations of of regular languages. The remaining part of the paper studies DFA minimization (Section 8), two-way automata (Sections 9 to 11), and the logic WS1S (Sections 12 and 13).

Type Theory Preliminaries

We formalize our results in the constructive and intensional type theory of the proof assistant Coq. In this setting, decidability properties are of great importance. A decider for a predicate P : X → Prop is a boolean predicate p : X → B satisfying ∀x.P x ↔ (p x = true)

We call a predicate decidable if it has a decider. Similar to predicates, a decidable proposition is a proposition that is equivalent to some boolean expression. We will mostly use the same notation for decidable propositions and the associated boolean expressions. In particular, if a boolean b appears as a proposition, it is to be read as b = true.

In Coq, operations such as boolean equality tests and choice operators are not available for all types. Nevertheless, there are certain classes of types for which these operations are definable. For our purposes, three classes of types are of particular importance. These are discrete types, countable types, and finite types [START_REF] Gonthier | A modular formalisation of finite group theory[END_REF].

We call a type X discrete if equality on (elements of) X is decidable. The type of booleans B and the type of natural numbers N are both discrete.

We call a type X countable if there are functions f : X → N and g : N → X ⊥ (X ⊥ being the option type over X) such that g( f x) = Some x for all x : X. Since N is discrete, all countable types are also discrete. Moreover, every countable type X comes equipped with a choice operator xchoose X : ∀p : X → B. (∃x. p x) → X satisfying p(xchoose X p E) for all E : (∃x. p x). That is, xchoose X turns abstract1 existence proofs into concrete witnesses. If X is countable, the type X * of lists over X is also countable. We will repeatedly make use of the fact that surjective functions from countable types to discrete types have right inverses. Lemma 2.1 Let X be countable, let Y be discrete, and let f : X → Y be surjective. Then one can define a function f : Y → X such that f ( f y) = y for all y.

Proof By surjectivity, we have a proof E : (∀y∃x. f x = y). It is easy to verify that f y := xchoose X (E y) is a right inverse as required.

⊓ ⊔

A finite type is a discrete type X together with a duplicate free list enumerating all elements of X. If X is finite, we write |X| for the number of elements of X and rank x for the position of an element x : X in the list enumerating the type. For our purposes, the most important property of finite types is that quantification over finite types preserves decidability. Discrete, countable, and finite types are closed under forming product types X ×Y , sum types X +Y , and option types X ⊥ . Moreover, all three classes of types are closed under building subtypes with respect to decidable predicates. Let p : X → B. The Σ -type { x : X | p x }, whose elements are dependent pairs of elements x : X and proofs of p x = true, can be treated as a subtype of X. In particular, the first projection yields an injection from { x : X | p x } to X since p x = true is proof irrelevant, i.e., has at most one proof [START_REF] Hedberg | A coherence theorem for Martin-Löf's type theory[END_REF].

Finite types also come with a power operator. That is, if X and Y are finite types then there is a finite type Y X whose |Y | |X| elements represent the functions from X to Y up to extensionality. We write 2 X for the finite type of (extensional) finite sets with decidable membership represented as B X . If a finite type X appears as a set, it is to be read as the full set over X.

Languages in Constructive Type Theory

An alphabet is a finite type. A word over an alphabet is a list over the alphabet. We shall use the letters Σ and Γ for alphabets. Since we write X * for the type of lists over X, Σ * denotes the type of words over Σ . The elements of an alphabet are called symbols. We shall use the letters a and b for symbols and the letters x, y, and z for words. As usual, we write ε for the empty word (i.e., the empty list), xy or x • y for the concatenation of words, a for the singleton word [a], a n for the word consisting of n occurrences of the symbol a, and |x| for the length of words. We also write x[n, m] for the subword from position n (inclusive) to m (exclusive).

A language over Σ is a unary predicate on Σ * . We shall write x ∈ L for L x when convenient. Given that we work in an intensional type theory, languages containing the same words are not necessarily equal. We call two languages equivalent and write L 1 ≡ L 2 if they contain the same words. The absence of extensionality will not cause difficulties since all our constructions respect language equivalence. Note that in contrast to languages, which are predicates on the infinite type Σ * , sets over finite types (e.g., sets of states) are represented extensionally.

We employ the usual notations for languages. We write / 0 for the empty language, Σ * for the language of all words, L := Σ * \ L for complements of languages,

L 1 • L 2 := { xy | x ∈ L 1 , y ∈ L 2 }
for concatenations of languages, L 0 := {ε} and L n+1 := L • L n for powers of languages, and L * := n L n for Kleene stars of languages. Further, we write

L 1 /L 2 := { x | ∃y ∈ L 2 . xy ∈ L 1 } for right quotients and L 1 \L 2 := { y | ∃x ∈ L 1 . xy ∈ L 2 }
for left quotients of languages. Moreover, we write R L (x) := { y | xy ∈ L } for the residual language of L with respect to x. Note that residual languages are a special case of left quotients. That is, we have R L (x) ≡ {x}\L (but not R L (x) = {x}\L due to the absence of extensionality).

A function h :

Σ * → Γ * from words to words is a (word) homomorphism if h(x • y) = h(x) • h(y). We write h -1 (L) := { x | h x ∈ L } for the preimage of L under h and h(L) := { y | ∃x ∈ L.h x = y } for the image of L under h. Lemma 3.1 Let x ∈ Σ * ,
let L and L ′ be decidable languages, and let h be a homomorphism. Then the languages

Σ * , / 0, {x}, L, L ∪ L ′ , L ∩ L ′ , L • L ′ , L * , R L (x),

⊓ ⊔

Note that the language h(L) is generally not decidable even for decidable L. 2 The languages associated to the various representations of regular languages will always be decidable.

Deterministic Finite Automata

Deterministic finite automata (DFAs) can be seen as the most basic operational representation of regular languages. We take DFAs to be the representation defining the notion of regularity.

Definition 4.1 A deterministic finite automaton (DFA) is a structure (Q, s, F, δ ) where -Q is a finite type of states. -s : Q is the starting state. -F : 2 Q is the set of final states. -δ : Q → Σ → Q is the transition function.
In Coq, we represent DFAs using dependent records:

dfa := { state : finType start : state final : set state trans : state → Σ → state}
Here, state : finType restricts the type of states to be a finite type. The combination of dependent records and finite types provides for a formalization of finite automata that is very convenient to work with. In particular, there are no well-formedness conditions. Let A = (Q, s, F, δ ) be a DFA. We extend δ to a function δ : Q → Σ * → Q by recursion on words:3 δ q ε := q δ q(ax) := δ (δ q a) x If δ q x ∈ F for some state q and some word x, we say that q accepts x. The language of A is then defined as the language accepted by the starting state:

L (A) := { x ∈ Σ * | δ s x ∈ F } Note that L (A) is a decidable language. Definition 4.2 A DFA A accepts a language L if L ≡ L (A). Definition 4.3 A language is regular if it is accepted by some DFA.
Regular languages enjoy a number of closure properties. The closure under boolean operations (e.g., complement and intersection) and preimages of homomorphisms can easily be established using DFAs. For other closure properties we will use different representations.

x | x ∈ L (A 1 ) ⊙ x ∈ L (A 2 ) }.
Proof We show the case for the binary boolean operation "⊙". Let

A 1 = (Q 1 , s 1 , F 1 , δ 1 ) and A 2 = (Q 2 , s 2 , F 2 , δ 2 ).
It is easy to verify that the DFA (Q, s, F, δ ) where

Q := Q 1 × Q 2 F := { q | q ∈ F 1 ⊙ q ∈ F 2 } s := (s 1 , s 2 ) δ (p, q) a := (δ 1 p a, δ 2 q a) accepts { x | x ∈ L (A 1 ) ⊙ x ∈ L (A 2 ) }. ⊓ ⊔
Lemma 4.5 Let L ⊆ Γ * be regular and let h :

Σ * → Γ * be a homomorphism. Then h -1 (L) is regular. Proof Let A = (Q, s, F, δ ) be a DFA accepting L. Then the DFA (Q, s, F, δ ′ ) with δ ′ p a := δ p (h a) accepts h -1 (L). ⊓ ⊔
We now prove two criteria for nonregularity. The first criterion is based on residual languages. The reachable states of a DFA accept, up to equivalence, exactly the residual languages of its language. Consequently, a language with infinitely many nonequivalent residual languages cannot be regular. Theorem 4.6 (Residual Criterion) Let L be a language and let f :

N → Σ * such that n = m whenever R L ( f n) ≡ R L ( f m). Then L is not regular.
Proof Assume that L is regular and let A = (Q, s, F, δ ) be a DFA accepting L. We define a function g : N → Q as g n := δ s ( f n). Using the assumption on f , we obtain that g is injective. This is a contradiction since Q is finite. The contrapositive of Theorem 4.6 is referred to as "Continuation Lemma" in [START_REF] Rosenberg | State[END_REF].

Another criterion for nonregularity is the Pumping Lemma [START_REF] Rabin | Finite automata and their decision problems[END_REF]. The intuition is that for every DFA the runs on sufficiently long words must include cycles that may be repeated by repeating the corresponding part of the input word. Lemma 4.8 Let A be a DFA and let x, z, y : Σ * . If xyz ∈ L (A) and |A| < |y|, then there exist u, v, and w such that y = uvw, v = ε, and xuv i wz ∈ L (A) for all i : N.

Proof Let A = (Q, s, F, δ ) and xyz ∈ L (A) with |A| < |y|. Let f (n) := δ ( δ s x) (y[0, n]). Since |A| < |y|, we obtain j < k < |y| such that f ( j) = f (k).
It is easy to verify that u := y[0, j], v := y[ j, k] and w := y[k, |y|] satisfy the required properties.

⊓ ⊔

Note that the argument in the proof of Lemma 4.8 does not make use of the notion of "runs" employed in the informal argument. While the notion of a run provides useful intuitions about DFAs, the formalization of our results for DFAs would not profit from making the concept explicit.

Lemma 4.9 (Pumping) Let L ⊆ Σ * . Then L is nonregular if for all k ∈ N there exist words x, y, z : Σ * such that k ≤ |y|, xyz ∈ L, and for all u, v, w such that y = uvw and v = ε there exists some i such that xuv i wz / ∈ L.

We include the Pumping Lemma because of its ubiquity in the literature. For proofs of nonregularity, the Residual Criterion (Theorem 4.6) is usually easier to use. In particular, the Pumping Lemma is incomplete in the sense that there are examples of decidable nonregular languages (cf. [START_REF] Johnsonbaugh | Converses of pumping lemmas[END_REF]) that do not satisfy the precondition of Lemma 4.9.

Classifiers

We now introduce the notion of classifier. A classifier is a function that can be seen as representing a right-congruent partition of Σ * with finite index. Right-congruence provides for a cut-off property that is useful for establishing decidabiliy properties. Moreover, classifiers refining a given language correspond to Myhill-Nerode relations [START_REF] Hopcroft | Introduction to automata theory, languages, and computation -international edition[END_REF][START_REF] Kozen | Automata and computability[END_REF]. Based on classifiers, we will establish a constructive Myhill-Nerode characterization of regularity. Proof By Corollary 5.4, we have that ∃x. f x = q is decidable for all q. Hence, we can construct the subtype

{ q : Q | ∃x. f x = q }. ⊓ ⊔ If f : Σ * → Q is a classifier, we write f (Σ * )
for the subtype of Q corresponding to the image of f . We now extend the notion of classifier to classifiers for a given language and show that this provides another representation for regular languages. Definition 5.6 Let L be a language. A classifier for L is a classifier that refines L, i.e., a classifier such that (x ∈ L ↔ y ∈ L) whenever f x = f y. Fact 5.7 Let A = (Q, s, F, δ ) be a DFA. Then δ q is a classifier for the language accepted by q. In particular, δ s is a classifier for L (A).

Conversely, we can turn a classifier-decider pair for a language into a DFA. Lemma 5.8 Let L be decidable and let f : Σ * → Q be a classifier for L. Then one can construct a DFA accepting L that has at most |Q| states.

Proof By casting the results of f from Q to f (Σ * ), we obtain a surjective classifier g : Σ * → f (Σ * ) for L (Corollary 5.5). Since g is surjective, it has a right inverse g (Lemma 2.1). It is straightforward to verify that the DFA (Q ′ , s, F, δ ) where

Q ′ := f (Σ * ) s := g ε F := { q | g q ∈ L } δ q a := g((g q) • a)
accepts the language L and has at most |Q| states.

⊓ ⊔ Theorem 5.9 A language is regular if and only if it has both a decider and a classifier.

Remark 5.10 Classifiers can be seen as computational representations of Myhill-Nerode relations (i.e., right congruent relations of finite index that refine the language). Lemma 5.8 corresponds to the observation in [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF] that the construction of DFAs from Myhil-Nerode relations is "effective" (or computational) whenever language membership is decidable and the number of equivalence classes is bounded. In addition to the upper bound on the number of equivalence classes (i.e., the size of Q), Lemma 5.8 includes (via the decidable equality on the finite type Q) the redundant assumption that the Myhill-Nerode relation is decidable. This simplifies both the statement and the proof and is sufficient for our purposes.

The cut-off property for classifiers (Theorem 5.3) allows us to easily establish decidability of language emptiness for DFAs.

Theorem 5.11 1. Language (non-)emptiness for DFAs is decidable. 2. Language inclusion and equivalence for DFAs are decidable.

Proof For (1), let A = (Q, s, F, δ ) be a DFA. Then L (A) is nonempty iff ∃x. δ s x ∈ F which is decidable since δ s is a classifier (Corollary 5.4). Claim (2) follows with (1) and Lemma 4.4.

⊓ ⊔

Note that, constructively, decidability of non-emptiness (i.e., ∃x.x ∈ L) implies decidability of language emptiness (i.e., L ≡ / 0), but not the other way around. We remark that our proof of decidability of language emptiness is essentially the proof given in [START_REF] Rabin | Finite automata and their decision problems[END_REF] with the cut-off property made explicit.

With decidability of language emptiness in place, we can show the closure of regular languages under quotients. For DFAs A = (Q, s, F, δ ) and q : Q, we define A[q] := (Q, q, F, δ ). Lemma 5.12 Let L 1 and L 2 be regular. Then L 1 /L 2 is regular.

Proof Let A = (Q, s, F, δ ) be a DFA accepting L 1 . We want to define a DFA B = (Q, s, F ′ , δ ) where F ′ := { q | ∃y ∈ L 2 . δ q y ∈ F }.
For this to be well-defined we need to be able to decide which states are final states. We have ∃y ∈

L 2 . δ q y ∈ F iff L 2 ∩ L (A[q]
) is nonempty which is decidable (Lemma 4.4 and Theorem 5.11).

⊓ ⊔ Lemma 5.13 Let L 1 and L 2 be regular. Then L 1 \L 2 is regular.

Proof Let A = (Q, s, F, δ ) be a DFA accepting L 2 and let S := { q | ∃x ∈ L 1 . δ s x = q }.
Similar to the proof of Lemma 5.12, membership in S is decidable since ∃x ∈ L 1 . δ s x = q is equivalent to the non-emptiness of L 1 ∩ L (B) where

B := (Q, s, {q}, δ ). It is straightforward to verify that L 1 \L 2 ≡ q∈S L (A[q]
). Thus, L 1 \L 2 is regular since regular languages are closed under union (Lemma 4.4).

⊓ ⊔

We remark that there are languages that can be shown regular using excluded middle but cannot be shown regular constructively. To see this, consider the constant language L := { x | P } where P is some independent proposition (i.e., a proposition for which P ∨ ¬P is not provable constructively). Assuming ∀P.P ∨ ¬P, one can easily show the existence of a DFA accepting L. However, even without excluded middle, the existence of a DFA accepting L would allow us to prove ε ∈ L ∨ ε / ∈ L and therefore also P ∨ ¬P. Hence, we have: Since the constant function from Σ * to the unit type is a classifier for { x | P }, this also shows that the restriction to decidable languages in Lemma 5.8 is unavoidable in a constructive setting. For our use of Lemma 5.8 in the translation from 2NFAs to DFAs (cf. Section 11), the decidability condition is easily satisfied.

Similar to constant languages, one can show using excluded middle that L 1 /L 2 is regular whenever L 1 is regular (for any language L 2 ). However, without a proper computational representation of L 2 it is impossible to determine which of the finitely many possible sets of final states is the correct one (cf. proof of Lemma 5.12). In contrast to Lemma 5.8, assuming decidabiliy of L 2 is not sufficient. To see this, consider the regular language L 1 := Σ * and the class of decidable languages L 2 (m) := { a n | the m-th Turing machine holds within n steps on input ε }. Then L 1 /L 2 (m) is nonempty iff the m-th Turing machine halts on input ε. If we could constructively show the existence of automata for all languages L 1 /L 2 (m), this would give us, via the constructive interpretation of the logic, a method for deciding the halting problem. A sufficient requirement on the representation of L 2 is that non-emptiness of L 2 ∩ L (A q ) is decidable. We formalize the case where L 2 is given by a DFA and remark that that a context-free grammar for L 2 would suffice.

Nondeterministic Finite Automata

Nondeterministic finite automata (NFAs) are another prominent representation of regular languages. Nondeterminism often allows for constructions that are simpler than directly constructing DFAs. We give conversions between DFAs and NFAs and then use NFAs to establish the closure of regular languages under concatenation and Kleene star. We will also use NFAs as one possible target for the reduction from two-way automata to one-way automata (Section 10) and to show decidability of WS1S (Section 12).

Nondeterministic finite automata differ from DFAs in that the transition function is replaced with a relation. Moreover, we allow multiple starting states.

Definition 6.1 A nondeterministic finite automation (NFA) is a structure (Q, S, F, →) where: -Q is a finite type of states. -S : 2 Q is the set of starting states. -F : 2 Q is the set of final states. -→ : Q → Σ → Q → B is the transition relation.
We write p a → q for the application of → to p, a, and q.

Let A = (Q, S, F, →) be an NFA. Similar to DFAs, we define acceptance for every state of an NFA by structural recursion on the input word.

accept p ε := p ∈ F accept p (ax) := ∃q. p a → q ∧ accept q x
The language of an NFA is the union of the languages accepted by its starting states.

L (A) := { x ∈ Σ * | ∃s ∈ S. accept s x } Note that since Q is finite, L (A) is a decidable language.
As with DFAs, acceptance of languages is defined up to language equivalence. Since we allow multiple starting states, the disjoint union of two NFAs yields an NFA for the union of the respective languages. Lemma 6.2 Let N be an n-state NFA and let M be an m-state NFA. Then one can construct an NFA with n + m states that accepts L (N) ∪ L (M).

Proof Let N = (Q 1 , S 1 , F 1 , → 1 ) and M = (Q 2 , S 2 , F 2 , → 2 ). The NFA for L (N)∪L (M) uses the sum type Q 1 + Q 2 as
the type of states and { inl q | q ∈ S 1 } ∪ { inr q | q ∈ S 2 } as starting states. Final states and transition relation are defined analogously.

⊓ ⊔

We establish the equivalence between DFAs and NFAs using the powerset construction.

Lemma 6.3 For every n-state NFA A, one can construct a DFA with 2 n states that accepts L (A).

Proof Let A = (Q, S, F, →) be an NFA. Then the DFA (Q ′ , s ′ , F ′ , δ ′ )
where

Q ′ := 2 Q F ′ := { X | X ∩ F = / 0 } s ′ := S δ ′ X a := { q | ∃p ∈ X. p a → q } is a DFA accepting L (A). ⊓ ⊔
Since DFAs can easily be transformed to NFAs, we obtain: Theorem 6.4 A language is regular if and only if it is accepted by some NFA.

One can work directly with NFAs to show the closure of regular languages under concatenation and iteration. Indeed, this is what we did in [START_REF] Doczkal | A constructive theory of regular languages in Coq[END_REF]. However, the proofs become simpler if one first extends NFAs with ε-transitions.

We define εNFAs like NFAs with additional transitions of the form p ε → q, i.e., transitions that do not consume a symbol from the input word. In contrast to NFAs, acceptance for εNFAs cannot be defined using a simple recursion on the input word due to possible sequences of ε-transitions of arbitrary length. Thus, we define acceptance for εNFAs as an inductive predicate. Let N = (Q, S, F, →) be an εNFA. The acceptance relation for N is defined inductively as follows:

p ∈ F accept ε p ε p a → q accept ε q x accept ε p (a :: x) p ε → q accept ε q x accept ε p x
Note that, in contrast to NFAs, the language of an εNFA is -a priori -not a decidable language. However, decidability (and equivalence to NFAs) are easily established by removing ε-edges as shown below. Lemma 6.5 For every n-state εNFA N one can construct an n-state NFA accepting L (N).

Proof Let N = (Q, S, F, →) be some εNFA. We define an NFA N ′ = (Q, S ′ , F, ) where

S ′ := { q | ∃s ∈ S.s ε → * q } p a q := ∃q ′ . p a → q ′ ∧ q ′ ε → * q
The inclusion L (N ′ ) ⊆ L (N) follows by induction on words. The converse inclusion follows by induction on the acceptance relation. ⊓ ⊔ Lemma 6.6 Let N 1 and N 2 be NFAs. Then one can construct NFAs accepting L (N 1 ) * and

L (N 1 ) • L (N 2 ).
Proof We show the case for

L (N 1 )•L (N 2 ). Let N 1 = (Q 1 , S 1 , F 1 , → 1 ) and N 2 = (Q 2 , S 2 , F 2 , → 2 )
. By Lemma 6.5, it suffices to construct an εNFA. We define an εNFA M = (Q, S, F, →) where

Q := Q 1 + Q 2 inl p a → inl q := p a → 1 q S := { inl p | p ∈ S 1 } inr p a → inr q := p a → 2 q F := { inr p | p ∈ F 2 } inl p ε → inr q := p ∈ F 1 ∧ q ∈ S 2
and no other transitions are possible. To show that M accepts L (N 1 ) • L (N 2 ) it suffices to show the following three properties:

1. ∀p : Q 2 . accept p x → accept ε (inr p) x 2. ∀p : Q 1 . accept p x → y ∈ L (N 2 ) → accept ε (inl p) xy 3. ∀p : Q 1 + Q 2 .
accept ε p x → accept q x if p = inr q ∃y z. x = yz ∧ accept q y ∧ z ∈ L (N 2 ) if p = inl q Claims (1) and (2) follow by induction on x where (1) provides the base case for (2). Claim (3) follows by induction on accept ε p x.

⊓ ⊔

The proof the lemma above avoids the need for the notion of a run through a simple generalization of the statement. For the translations from 2NFAs to NFAs (Section 10) and MSO formulas to NFAs (Section 13) we were unable to find such generalizations. For this reason, we also formalize the notion of (accepting) runs on NFAs.

Let N = (Q, S, F, →) be an NFA. We define a relation run : Σ * → Q → Q * → Prop relating words and nonempty sequences of states inductively as follows:

q ∈ F run ε q [] p a → q
run x q l run (ax) p (q :: l) An accepting run for x is a sequence of states (s :: l) such that s ∈ S and run x s l. Note that accepting runs for x must have length |x| + 1. We write (r i ) i≤|x| for runs of length |x| + 1 and r i for the i-th element (counting from 0). Lemma 6.7 x ∈ L (N) iff there exists an accepting run for x.

Regular Expressions

In this section we establish the equivalence between finite automata and regular expressions, another prominent representation of regular languages. While finite automata can be seen as operational characterizations of regular languages, regular expressions provide a compositional (or algebraic) characterization of regular languages. We consider regular expressions with the following syntax:

e := / 0 | ε | a | e • e | e + e | e * (a : Σ )
As with words, we usually omit the "•" operator. We write |e| for the tree size of e. The language of a regular expression e, written L (e), is defined as follows: The main result of this section is that regular expressions describe exactly the regular languages. One direction is fairly straightforward. Proof By induction on e. The base cases are straightforward, the remaining cases follow with Lemma 6.2 and the constructions underlying Lemma 6.6.

L ( / 0) := / 0 L (e 1 e 2 ) := L (e 1 ) • L (e 2 ) L (

⊓ ⊔

We now translate DFAs to regular expressions. There are a number of algorithms for constructing regular expressions from automata, e.g., Brzozowski's algebraic method [START_REF] Brzozowski | Derivatives of regular expressions[END_REF] and Kleene's algorithm [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF][START_REF] Kozen | Automata and computability[END_REF]. We employ a variant of Kleene's algorithm for DFAs, because we deem it easiest to formalize.

For the rest of this section, we fix some DFA A = (Q, s, F, δ ). We define an indexed collection of transition languages between states p, q : Q as follows:

L X p,q := { x ∈ Σ * | δ p x = q, ∀0 < i < |x|. δ p(x[0, i]) ∈ X }
That is, x ∈ L X p,q if starting from state p and reading x the automaton A ends in state q and visits only states from X in between. Note that in the particular case where X is Q, the requirement on the intermediate states is trivially fulfilled. Consequently, the language of A can be expressed as the union of the transition languages between the starting state and the final states.

Lemma 7.4 L (A) ≡ q∈F L Q s,q
That is, to obtain a regular expression for L (A), it suffices to construct regular expressions for L Q s,q where q ∈ F. We recursively solve this problem for all languages L X p,q by successively removing states from X. For the case where X = / 0, one can directly give a regular expression. Let p, q : Q. We define:

R / 0 p,q := (if p = q then ε else / 0) + ∑ a∈Σ δ (p,a)=q a Lemma 7.5 L R / 0 p,q ≡ L / 0 p,q .
For nonempty sets of allowed intermediate states, consider some word x from L {r}∪X p,q . Reading x starting from p, the automaton will either not visit r at all, or reach r, go through a number of cycles starting and ending at r, and then continue to q without visiting r again. This motivates the following recursive equivalence:

Lemma 7.6 Let p, q, r : Q and X ⊆ Q, then L {r}∪X p,q ≡ L X p,r • L X r,r * • L X r,q ∪ L X p,q
Proof The inclusion from right to left is easy to show. For the other direction, we first show

∀x. x ∈ L {r}∪X p,q → x ∈ L X p,q ∨ ∃y z. x = yz ∧ y ∈ L X p,r ∧ z ∈ L {r}∪X r,q ∧ |z| < |x| (*)
We consider two cases: δ p (x[0, i]) = r for all i such that 0 < i < |x|. In this case, we have x ∈ L X p,q . δ p (x[0, i]) = r for some i with 0 < i < |x|. Let i be the minimal i satisfying the condition. It

is straightforward to verify that x[0, i] ∈ L X p,q and x[i, |x|] ∈ L {r}∪X r,q . Moreover, |x[i, |x|]| < |x| since 0 < i.
The inclusion from left to right then follows by complete induction on word length using (*).

⊓ ⊔

The construction of the regular expression accepting L (A) then follows the recursive structure given by Lemma 7.6. We define a function reg : Q * → Q → Q → regexp by recursion on the list of states:

reg [] p q := R / 0 p,q reg (r :: l) p q := (reg l p r)(reg l r r) * (reg l r q) + (reg l p q) Lemma 7.7 Let l : Q * and p, q : Q. Then L (reg

l p q) ≡ L { r | r ∈ l } p,q .
Theorem 7.8 A language is regular iff it is accepted by some regular expression.

Proof Let L be a regular language. Since A was chosen arbitrarily, we can assume that A accepts L. Hence, the claim follows with Lemmas 7.4 and 7.7 (taking l to be the list enumerating the finite type Q). The converse follows with Lemma 7.3 and Theorem 6.4. ⊓ ⊔

The equivalence between DFAs and regular expressions yields two closure properties of regular expressions that are difficult to prove without automata. 4Corollary 7.9 Let e 1 and e 2 be regular expressions. Then one can construct regular expressions accepting L (e 1 ) ∩ L (e 2 ) and L (e 1 ).

Remark 7.10 The constructions presented in this section allow the definition of a complementation operation for regular expressions that causes a doubly-exponential increase in the size of the expression. The DFA for the complement language of some expression e can have up to 2 [START_REF] Gelade | Succinctness of the complement and intersection of regular expressions[END_REF].

Using regular expressions, it is straightforward to show that regular languages are closed under images of homomorphisms and under word reversal. Lemma 7.11 Let L ⊆ Σ * be regular and let h : Σ * → Γ * be a homomorphism. Then h(L) is regular.

Proof Let e be a regular expression for L. Replacing all atoms a occurring in e with an expression accepting {h(a)} yields a regular expression for h(L).

⊓ ⊔ Lemma 7.12 Let L be regular. Then { x | rev x ∈ L } is regular.

Proof Let e such that L (e) ≡ L. It is straightforward to compute a regular expression for { x | rev x ∈ L } by reversing all sequential compositions e 1 e 2 in e. ⊓ ⊔ Remark 7.13 Closure under word reversal can also be shown using NFAs. However, both the direct structural acceptance criterion and the notion of accepting run (Section 6) are asymmetric in that they always need to reach final states. To show closure under word reversal using NFAs, we would have to generalize the notion of run to runs between any pair of states. The proof above requires no such generalization.

Together with the closure properties established in Sections 4 and 6, we obtain:

Theorem 7.14 (Closure Properties) Let L 1 and L 2 be regular.

Then L 1 , L * 1 ,L 1 ∪ L 2 , L 1 ∩ L 2 , L 1 • L 2 , h(L), h -1 (L), L 1 /L 2 , L 1 \L 2 and { x | rev x ∈ L } are regular.
Note that, all closure properties are established as operations on the underlying representations of the input languages.

DFA Minimization

In this section, we show that for every regular language there exists a unique minimal automaton (cf. [START_REF] Kozen | Automata and computability[END_REF]). The proof is based on a simple minimization function that prunes unreachable states and collapses states that accept the same language. Definition 8.1 Let A = (Q, s, F, δ ) be a DFA. We call A connected if every state is reachable, i.e. ∀q : Q ∃x : Σ * . δ s x = q.

collapsed if no distinct states p, q : Q are related by the collapsing relation p ≈ A q := ∀x. δ p x ∈ F ↔ δ q x ∈ F minimal if every DFA accepting L (A) has at least |Q| states.

The collapsing relation relates states that accept the same language and can therefore be merged. It turns out that an automaton is minimal iff if it is connected and collapsed. We first show that all connected and collapsed automata for a given language are isomorphic and therefore have the same size.

Definition 8.2 Let A 1 = (Q 1 , s 1 , F 1 , δ 1 ) and A 2 = (Q 2 , s 2 , F 2 , δ 2 )
be DFAs. We call A 1 and A 2 isomorphic, if there exists a a bijection i :

Q 1 → Q 2 satisfying ∀q : Q 1 . i(δ 1 q a) = δ 2 (i q) a ∀q : Q 1 . i q ∈ F 2 ↔ q ∈ F 1 i s 1 = s 2
Theorem 8.3 Let A 1 and A 2 be connected and collapsed DFAs accepting the same language. Then A 1 and A 2 are isomorphic.

Proof Let A 1 = (Q 1 , s 1 , F 1 , δ 1 ) and A 2 = (Q 2 , s 2 , F 2 , δ 2 ).
i := δ2 s • δ1 s j := δ1 s • δ2 s
Since A and B are also collapsed, we have i( j p) = p and j(i q) = q for all p and q. Thus, i : Proof Let B be some DFA accepting L (F A).

Q 1 → Q 2 is
Then |FA| = |FB| ≤ |B|. ⊓ ⊔
We now construct a minimization function by defining two operations on DFAs, called prune and collapse, that preserve the language and respectively establish connectedness and collapsedness.

For prune we construct the sub-automaton whose type of states is the subtype of reachable states. Recall that for every DFA (Q, s, F, δ ) the function δ s is a classifier. Consequently, the pruning function can be defined as follows (cf. Corollary 5.5).

prune (Q, s, F, δ ) := (Q ′ , s, F ′ , δ )
where

Q ′ := ( δ s)(Σ * ) F ′ := { q ∈ Q ′ | q ∈ F } Remark 8.5
For the definition in Coq we also need to cast s from Q to Q ′ and lift δ to a function of type Q ′ → Σ → Q ′ . This is straightforward since s is clearly reachable and transitions preserve reachability.

Lemma 8.6 prune A is connected, accepts L (A) and has at most |A| states.

To define the function collapse, we make use of quotient types. A quotient type for some type Q and an equivalence relation ≈ on Q is a type Q/≈ together with a surjective function π : Q → Q/≈ satisfying π p = πq ↔ p ≈ q. If Q is countable and ≈ is decidable, then Q/≈ can be constructed as a subtype of Q [START_REF] Cohen | Pragmatic quotient types in Coq[END_REF]. In this case π also has a right inverse π (Lemma 2.1).

To show decidability of the collapsing relation, we again make use of Corollary 5.4.

Lemma 8.7 Let A be a DFA. Then ≈ A is decidable.

Proof Let A = (Q, s, F, δ ) and let q, r : Q. Decidability of q ≈ A r follows with Corollary 5.4 by taking f x := ( δ q x, δ r x) and p := λ (q, r). q ∈ F ↔ r ∈ F.

⊓ ⊔

The function collapse takes as input some automaton A and returns the quotient automaton with respect to the collapsing relation.

collapse A := (Q ′ , s ′ , F ′ , δ )
where A = (Q, s, F, δ ) and

Q ′ := Q/≈ A s ′ := π s F ′ := { q | π q ∈ F } δ ′ q a := π(δ (π q) a)
Lemma 8.8 Let A be a connected DFA. Then collapse A accepts L (A), is collapsed and connected, and has at most |A| states.

We obtain a minimization function by defining minimize := collapse • prune. Theorem 8.9 Let A be a DFA, then minimize A accepts L (A) and is connected, collapsed, and minimal.

Proof Immediate with Lemmas 8.6, 8.8, and 8.4.

⊓ ⊔ Theorem 8.10 Let A be a DFA. Then A is minimal iff A is connected and collapsed.

Proof Assume A is is minimal. Then both prune and collapse preserve the number of states. Hence, all states must be reachable and ≈ A must be an identity relation. For the converse direction, assume A is connected and collapsed and fix some DFA B with L (A) = L (B).

Then |A| = |minimize B| ≤ |B| by Theorems 8.3 and 8.9 ⊓ ⊔ Corollary 8.11 All minimal automata accepting a given language are isomorphic.

Note that the premise |FA| ≤ |A| of Lemma 8.4 becomes redundant with Theorem 8.10. However, the relevant direction of the proof of Theorem 8.10 relies on the fact that the function minimize establishes connectedness and collapsedness without increasing the number of states.

We remark that the classifier obtained from a minimal DFA corresponds to the coarsest Myhill-Nerode relation [START_REF] Hopcroft | Introduction to automata theory, languages, and computation -international edition[END_REF][START_REF] Kozen | Automata and computability[END_REF] (cf. Remark 5.10). Fact 8.12 If A = (Q, s, F, δ ) is a minimal DFA for L, then δ s x = δ s y iff R L (x) ≡ R L (y).

Two-Way Finite Automata

A two-way finite automaton (2FA) is essentially a read-only Turing machine, i.e., a machine with a finite state control and a read head that may move back and forth on the input word. One of the fundamental results about 2FAs is that the ability to move back and forth does not increase expressiveness [START_REF] Rabin | Finite automata and their decision problems[END_REF]. That is, two-way automata are yet another representation of the class of regular languages. As for one-way automata, we consider both the deterministic and the nondeterministic variant.

In the literature, two-way automata appear in a number of variations. Modern accounts of two-way automata [START_REF] Pighizzini | Two-way finite automata: Old and recent results[END_REF] usually consider automata with end-markers. That is, on input x the automaton is run on the string ⊲x⊳, where ⊲ and ⊳ are marker symbols that do not occur in Σ and allow the automaton to detect the word boundaries. These marker symbols are not present in early work on two-way automata [START_REF] Rabin | Finite automata and their decision problems[END_REF][START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF][START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF]. The ability to detect word boundaries allows for the construction of more compact automata for some languages. In fact, the emptiness problem for nondeterministic two-way automata with only one endmarker over a singleton alphabet is polynomial while the corresponding problem for two-way automata with two endmarkers is NP-complete [START_REF] Vardi | Endmarkers can make a difference[END_REF]. Remarkably, the original proofs in [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF][START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] carry over to the setting with end-markers without conceptual changes.

Definition 9.1 A nondeterministic two-way automaton (2NFA) is a structure M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) where -Q is a finite type of states -s : Q is the starting state -F : 2 Q is the set of final states -δ : Q → Σ → 2 Q×{L,R} is the transition function for symbols -δ ⊲ : Q → 2 Q
is the transition function for the left marker δ ⊳ : Q → 2 Q is the transition function for the right marker Let M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) be a 2NFA. If (q, R) ∈ δ p a, this means that when reading the symbol a while in state p, the automaton may enter state q and move its read head one position to the right. For end-markers, we only allow the head to move back onto the word (or to the opposing marker if the input is ε), so no direction needs to be given. On an input word x : Σ * the configurations of M on x, written C x , are pairs (p, i) ∈ Q × {0, . . . , |x| + 1} where i is the position of the read head. We take i = 0 to mean that the head is on the left marker and i = |x| + 1 to mean that the head is on the right marker. Otherwise, the head is on the i-th symbol of x (counting from 1). In particular, we do not allow the head to move beyond the end-markers. In following, we write x[i] for the i-th symbol of x. The step relation → x : C x → C x → B updates state and head position according to the transition function for the current head position:

δ p i :=      (δ ⊲ p) × {R} i = 0 δ p (x[i]) 0 < i ≤ |x| (δ ⊳ p) × {L} i = |x| + 1 (p, i) - → x (q, j) :=(q, L) ∈ δ p i ∧ i = j + 1 ∨ (q, R) ∈ δ p i ∧ i + 1 = j
We write → * x for the reflexive transitive closure of → x . The language of M is then defined as follows:

L (M) := { x | ∃q ∈ F. (s, 1) - → x * (q, |x| + 1) }
That is, M accepts the word x if it can reach the right end-marker while being in a final state.

In Coq, we represent C x as the finite type Q×ord(|x|+2), where ord n := { m : N | m < n }. This allows us to represent → x as well as → *

x as decidable relations on C x . 5 Hence, L (M) is a decidable language. In the mathematical presentation, we treat ord n like N and handle the bound implicitly. In Coq, we use a conversion function inord : ∀n. N → ord(n + 1) which behaves like the 'identity' on numbers in the correct range and otherwise returns 0. This allows us to sidestep most of the issues arising from the dependency of the type of configurations on the input word. In particular, we recover the separation between stating facts about → x and proving that all mentioned indices stay within bounds.

Definition 9.2 A deterministic two-way automaton (2DFA) is a 2NFA (Q, s, F, δ , δ ⊲ , δ ⊳ )
where |δ ⊳ q| ≤ 1, |δ ⊲ q| ≤ 1, and |δ q a| ≤ 1 for all q : Q and a : Σ . Fact 9.3 For every n-state DFA one can construct an n-state 2DFA that accepts the same language and only moves its head to the right. Remark 9.4 While Fact 9.3 is obvious from the mathematical point of view, the formal proof is somewhat cumbersome due to the mismatch between the acceptance condition for DFAs, which is defined by recursion on the input word, and the acceptance condition for 2FAs, where the word remains constant throughout the computation.

The next two sections are devoted to the translation of two-way automata to one-way automata. There are several such translations in the literature. Vardi [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] gives a simple construction that takes as input some 2NFA M and yields an NFA accepting L (M). This establishes that deterministic and nondeterministic two-way automata accept exactly the regular languages. The size of the constructed NFA is exponential in the size of M. Consequently, if one wants to obtain an automaton for the input language, rather than its complement, the construction incurs a doubly exponential blowup in the number of states. Shepherdson [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF] gives a translation from 2DFAs to DFAs that incurs only an exponential blowup. Building on ideas from [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF], we adapt this construction to 2NFAs.

We first present the translation to NFAs since it is much simpler. We then give a direct translation from 2NFAs to DFAs. We also show that when applied to 2DFAs, the latter construction yields the bounds on the size of the constructed DFA established in [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF].

Vardi Construction

Let M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) be a 2NFA. We construct an NFA accepting L (M). Vardi [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] formulates the proof for 2NFAs without markers. We adapt the proof to 2NFAs with markers. The main idea is to define certificates for the non-acceptance of a string x by M. The proof then consists of two parts: 1. proving that these negative certificates are sound and complete 2. constructing an NFA whose accepting runs correspond to negative certificates Definition 10.1 A negative certificate for a word x is a set

C ⊆ C x satisfying: N1. (s, 1) ∈ C N2. If (p, i) ∈ C and (p, i) → x (q, j), then (q, j) ∈ C . N3. If q ∈ F then (q, |x| + 1) / ∈ C .
The first two conditions ensure that the negative certificates for x overapproximate the configurations M can reach on input x. The third condition ensures that no accepting configuration is reachable.

Lemma 10.2 Let x : Σ * . There exists a negative certificate for x iff x / ∈ L (M).

Proof Let R := { (q, j) | (s, 1) → * x (q, j) }. If there exists a negative certificate C for x, then R ⊆ C and, therefore, x / ∈ L (M). Conversely, if x / ∈ L (M), then R is a negative certificate for x.

⊓ ⊔ Let x be a word and let C be a negative certificate for x. The certificate C can be viewed as (|x|+2)-tuple over 2 Q where the i-th component, written

C i , is the set { q | (q, i) ∈ C }.
We define an NFA whose accepting runs correspond to this tuple view of negative certificates. For this, condition (N2) needs to be rephrased into a collection of local conditions, i.e., conditions that no longer mention the head position.

Definition 10.3 Let U,V,W : 2 Q and a : Σ . We say that -(U,V ) is ⊲-closed if q ∈ V whenever p ∈ U and q ∈ δ ⊲ p. -(U,V ) is ⊳-closed if q ∈ U whenever p ∈ V and q ∈ δ ⊳ p. -(U,V,W ) is a-closed if for all p ∈ V we have 1. q ∈ U whenever (q, L) ∈ δ p a 2. q ∈ W whenever (q, R) ∈ δ p a
We define an NFA N = (Q ′ , S ′ , F ′ , →) that incrementally checks the closure conditions defined above:

Q ′ := 2 Q × 2 Q S ′ := {(U,V ) | s ∈ V and (U,V ) is ⊲-closed} F ′ := {(U,V ) | F ∩V = / 0 and (U,V ) is ⊳-closed} (U,V ) a → (V ′ ,W ) := (V = V ′ ∧ (U,V,W ) is a-closed)
For q : Q ′ , we write q.1 for the first component of q and q.2 for the second component. Note that transition relation requires the two states to overlap. Hence, the runs of N on some word x, which consist of |x| transitions, define (|x|+2)-tuples. We will show that the accepting runs of N correspond exactly to negative certificates.

Lemma 10.4 x ∈ L (N) iff there exists a negative certificate for x.

Proof By Lemma 6.7, it suffices to show that there exists an accepting run iff there exists a negative certificate. "⇒" Let (r i ) i≤|x| be an accepting run of N on x. We define a negative certificate C for x where C 0 := (r 0 ).1 and C i+1 := (r i ).2. "⇐" If C is a negative certificate for x we can define a run (r i ) i≤|x| for x on M where r 0 := (C 0 , C 1 ) and r i+1 := (C i , C i+1 ). ⊓ ⊔ Remark 10.5 The formalization of the lemma above is straightforward but tedious due to the need to unfold the comparatively intricate definitions of N, C , and (r i ) i≤|x| . With about 60 lines, the proof of Lemma 10.4 is considerably longer than the proofs of most other lemmas.

Lemma 10.6 L (N) = L (M).

Proof Follows immediately with Lemmas 10.2 and 10.4. ⊓ ⊔ Theorem 10.7 For every n-state 2NFA M one can construct an NFA accepting L (M) and having at most 2 2n states.

If one wants to obtain a DFA for L (M) using this construction, one needs to determinize N before complementing it. Since N is already exponentially larger than M, the resulting DFA then has a size that is doubly exponential in |Q|.

We remark that, perhaps surprisingly, the translation from 2NFAs to NFAs for the complement language becomes simpler and more 'symmetric' in the presence of end-markers. The original construction [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] uses 2 Q + 2 Q × 2 Q as the type of states while the construction above gets along with the type 2 Q × 2 Q . States from the type 2 Q are required to check beginning and end of a negative certificate in the absence of end-markers.

Shepherdson Construction

We now give a second proof that the language accepted by a 2NFA is regular. The proof follows the original proof of Shepherdson [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF]. In [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF], the proof is given for 2DFAs without end-markers. Building on ideas form Vardi [START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF], we adapt the proof to 2NFAs with endmarkers.

We fix some 2NFA M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) for the rest of this section. In order to construct a DFA for L (M), it suffices to construct a classifier for L (M) (Lemma 5.8). For this, we need to come up with a finite type X and a function T : Σ * → X which is right-congruent and refines L (M).

The construction exploits that the input is read-only. Therefore, M can only save a finite amount of information in its finite state control. Consider the situation where M is running on a composite word xz. In order to accept xz, M must move its head all the way to the right. In particular, it must move the read-head beyond the end of x and there is a finite set S ⊆ Q of states that M can possibly be in when this happens for the first time. Once the read head is to the right of x, M may move its head back onto x. However, the only additional information that can be gathered about x is the set of states M may be in when returning to z. Since the possible states upon return may depend on the state M is in when entering x form the right, this defines a relation R ⊆ Q × Q. The set S and the relation R provide all the information required about x to determine whether xz ∈ L (M). For every word x, S and R (as defined above) define a finite table. We will define a function

T : Σ * → 2 Q × 2 Q×Q
returning the table for a given word. Note that 2 Q × 2 Q×Q is a finite type, i.e., there are only finitely many possible tables. We will show that L (M) is regular, by showing that T is a classifier for L (M), i.e., that T is right-congruent and refines L (M).

To formally define T , we need to be able to stop M once its head reaches a specified position. We define the k-stop relation on x:

(p, i) k - → x (q, j) := (p, i) - → x (q, j) ∧ i = k
Note that for k ≥ |x| + 2 the stop relation coincides with the step relation. The function T is then defined as follows:

T x := ({ q | (s, 1) |x|+1 ---→ x * (q, |x| + 1) }, { (p, q) | (p, |x|) |x|+1 ---→ x * (q, |x| + 1) })
Note that T returns a pair of a set and a relation. We write (T x).1 for the first component of T x and (T x).2 for the second component. Before we can show that T is a classifier for L (M), we need a number of properties of the stop relation. The first lemma captures the intuition, that for composite words xz, all the information M can gather about x is given by T x.

Lemma 11.1 Let p, q : Q and let x, z : Σ * . Then

1. q ∈ (T x).1 iff (s, 1) |x|+1 ---→ xz * (q, |x| + 1) 2. (p, q) ∈ (T x).2 iff (p, |x|) |x|+1 ---→ xz * (q, |x| + 1)
Since for composite words xz everything that can be gathered about x is provided by T x, M behaves the same on xz and yz whenever T x = T y. To show this, we need to exploit that M moves its head only one step at a time. This is captured by the lemma below. Lemma 11.2 Let i ≤ k ≤ j and let l be a k ′ -→ x -path from (p, i) to (q, j). Then there exists some state p ′ such that l can be split into a

k - → x -path from (p, i) to (p ′ , k) and a k ′ -→ x -path from (p ′ , k) to (q, j).
Proof By induction on the length of the k ′ -→ x -path from (p, i) to (q, j). Lemma 11.2 can be turned into an equivalence if k ′ ≥ k. We state this equivalence in terms of transitive closure since for most parts of the development the concrete path is irrelevant.

Lemma 11.3 Let i ≤ k ≤ j and let k ′ ≥ k. Then (p, i) k ′ -→ x * (q, j) iff there exists some p ′ such that (p, i) k - → x * (p ′ , k) k ′ -→ x * (q, j).
We now show that for runs of M that start and end on the right part of a composite word xz, x can be replaced with y whenever T x = T y.

Lemma 11.4 Let p, q : Q and let x, y, z : Σ * such that T x = T y. Then for all k > 1, i ≤ |z|+1, and 1 ≤ j ≤ |z| + 1, we have

(p, |x| + i) |x|+k ---→ xz * (q, |x| + j) iff (p, |y| + i) |y|+k ---→ yz * (q, |y| + j)
Proof By symmetry, it suffices to show the direction from left to right. We proceed by induction on the length of the path from (p, |x| + i) to (q, |x| + j). There are two cases to consider: i = 0. According to Lemma 11.2 the path can be split such that:

(p, |x|) |x|+1 ---→ xz * (p ′ , |x| + 1) |x|+k ---→ xz * (q, |x| + j)
Thus, (p, p ′ ) ∈ (T x).2 by Lemma 11.1. Applying Lemma 11.1 again, we obtain

(p, |y|) |y|+1 ---→ yz * (p ′ , |y| + 1)
The claim then follows by induction hypothesis since the path from (p, |x|) to (p ′ , |x|+1) must make at least one step.

i > 0. The path from (p, |x| + i) to (q, |x| + j) is either trivial and the claim follows immediately or or there exist p ′ and i ′ such that (p,

|x| + i) |x|+k ---→ xz (p ′ , |x| + i ′ ). But then (p, |y| + i) |y|+k ---→ yz (p ′ , |y| + i ′ )
and the claim follows by induction hypothesis.

⊓ ⊔

Now we have everything we need to show that T is a classifier for L (M).

Lemma 11.5 T refines L (M).

Proof Fix x, y : Σ * and assume T x = T y. By symmetry, it suffices to show y ∈ L (M) when-

ever x ∈ L (M). If x ∈ L (M), then (s, 1) |x|+2 ---→
x * (p, |x| + 1) for some p ∈ F. We show

y ∈ L (M) by showing (s, 1) |y|+2 ---→ y * (p, |y| + 1)
. By Lemma 11.3, there exists a state q such that:

(s, 1) |x|+1 ---→ x * (q, |x| + 1) |x|+2 ---→ x * (p, |x| + 1)
We can simulate the first part on y using Lemma 11.1 and the second part using Lemma 11.4. ⊓ ⊔ Lemma 11.6 T is right-congruent.

Proof Fix words x, y : Σ * and some symbol a : Σ and assume T x = T y. We need to show By Lemma 11.3, there exists a state p such that:

T xa = T ya. We first show (T xa).2 = (T ya).2. Let (p, q) ∈ Q × Q. We have to show that (p, |xa|) |xa|+1 ---→ xa * (q, |xa| + 1) implies (p, |ya|) |ya|+1 -
(s, 1) |x|+1 ---→ xa * (p, |x| + 1) |xa|+1 ---→ xa * (q, |xa| + 1)
Thus, we have p ∈ (T x).1 (and therefore also p ∈ (T y).1) and (p, q) ∈ (T xa).2. Since we have shown above that (T xa).2 = (T ya).2, the claim follows with Lemma 11.1.

⊓ ⊔

Note that Lemma 11.4 is used very differently in the proofs of Lemma 11.5 and Lemma 11.6.

In the first case we are interested in acceptance and set k to |x| + 2 so we never actually stop.

In the second case we set k to |xa| + 1 to stop on the right marker. Using Lemma 5.8 and the two lemmas above, we obtain:

Theorem 11.7 Let M be a 2NFA with n states. Then one can construct a DFA accepting L (M) having at most 2 n 2 +n states.

We now show that for deterministic two-way automata, the bound on the size of the constructed DFA can be improved from 2 n 2 +n to (n + 1) (n+1) . Fact 11.8 Let M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) be a 2DFA. Then k -→ x is functional for all k and x. Corollary 11.9 Let M be a 2DFA with n states. Then one can construct a DFA accepting L (M) having at most (n + 1) (n+1) states.

Proof Let M = (Q, s, F, δ , δ ⊲ , δ ⊳ ) be deterministic and let T : Σ * → 2 Q × 2 Q×Q be defined as above. Since T is right-congruent (Lemma 11.6) we can construct the type T (Σ * ) (Corollary 5.5). By Lemma 5.8, it suffices to show that T (Σ * ) has at most (|Q|+1) (|Q|+1) elements.

Let (S, R) : T (Σ * ). Then T x = (S, R) for some x : Σ * . We show that S has at most one element. Assume p, q ∈ S. By the definition of T , we have

(s, 1) |x|+1 ---→ x * (p, |x| + 1) and (s, 1) |x|+1 ---→ x * (q, |x| + 1) Since |x|+1 ---→
x is functional and both (p, |x| + 1) and (p, |x| + 1) are terminal, we have p = q. A similar argument yields that R is a functional relation. Consequently, we can construct an injection i :

T (Σ * ) → Q ⊥ × (Q ⊥ ) Q
Given some (S, R) : T (Σ * ), (i(S, R)).1 is defined to be the unique element of S or ⊥ if S = / 0. The definition of (i(S, R)).2 is analogous. The claim then follows since

Q ⊥ × (Q ⊥ ) Q has exactly (|Q| + 1) (|Q|+1) elements. ⊓ ⊔
12 Weak Monadic Second-Order Logic

We now consider weak monadic second order logic (WMSO), or more precisely the WMSO theory of one successor relation (WS1S). Our main results about WS1S are the decidability of satisfiability and model checking and a proof of the characterization theorem of Büchi [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF], Elgot [START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF], and Trakhtenbrot [START_REF] Trakhtenbrot | Finite automata and the logic of monadic predicates[END_REF] ([17, Theorem 12.26]), i.e., the fact that formulas can be assigned languages in such a way that the class of languages described by formulas is exactly the class of regular languages.

The aforementioned results are all closely related. The decidability results are obtained by translating formulas to NFAs. Together with the closure or regular languages under preimages of homomorphisms, this translation also yields an automaton for the language associated to a given formula. To show that formulas can express all regular languages, we give a formula describing the runs of a given automaton. Here, we rely on the fact that the the satisfaction relation is decidable as this ensures that the logic behaves classically even though we are working in a constructive setting.

We consider MSO formulas according to the following grammar:

φ , ψ := X ⊆ Y | X < Y | ⊥ | φ → ψ | ∃X.φ (X,Y : N)
We take variables to be natural numbers rather than objects of some abstract type of variables. Informally, a valuation is a function assigning finite sets of natural numbers to every variable. A valuation V satisfies X ⊆ Y if V X ⊆ V Y , and X < Y if every element of V X is smaller than every element of V Y . We write V |= φ if V satisfies φ . We will show that V |= φ is decidable. This establishes that the logic behaves classically (i.e., V |= ¬¬φ → φ with ¬ψ := ψ → ⊥ as usual). In particular, it allows us to use the classical definition of universal quantification (i.e., ∀X.φ := ¬∃X.¬φ ) and similarly for the remaining logical operations. 0 1 2 3 4 0 1 0 1 0 0 1 0 1 0 0 0 2 0 1 0 1 0

Then V v (0) = {0, 2}, V v (1) = {1}, V v (2) = {1, 3}, and V v (X) = / 0 for X ≥ 3. ⊓ ⊔
Lemma 12.5 For each V and n, there exists some v : B * n such that V agrees with V v on all variables smaller than n.

By assigning valuations to words over B n , we can assign to every formula the language of those words whose valuations satisfy the formula. Definition 12.6 (Vector Language) Let φ be a formula and let n : N. The language of nvectors of φ is defined as

L n (φ ) := { v ∈ B * n | V v |= φ } It order
to decide the satisfaction relation and satisfiability of formulas, it suffices to decide language membership and language emptiness for vector languages. For this purpose, we construct an NFA A n,φ accepting L n (φ ) for any given φ and n. The construction proceeds by recursion on the formula φ . The main reason for including the index n is the case for formulas of the form ∃φ . Removing the existential quantifier yields a formula with an additional free variable. Hence, the problem of constructing an NFA accepting L n (∃φ ) is reduced to the problem of constructing an NFA accepting L n+1 (φ ).

It is straightforward, albeit tedious, to construct automata for ⊆ and <.

Lemma 12.7 For each n, X, Y , one can construct automata A n,X⊆Y and A n,X<Y such that L (A n,X⊆Y ) ≡ L n (X ⊆ Y ) and L (A n,X<Y ) ≡ L n (X < Y ).

For additional detail on these constructions we refer to the Coq development. In the following, we describe the construction for A n,∃φ , which is the most technical of the required constructions.

Intuitively, A n,∃φ is obtained from A n+1,φ by guessing the content of the first "row" of the input word (cf. Example 12.4). The construction is complicated by the fact that one has to allow for this guessed row to be longer than the input word. This is necessary since the numbers occurring in the witness of the the quantified variable may need to be larger than the length of the input word. Definition 12.8 Let A n+1,φ = (Q, S, F, →) be an NFA with alphabet B n+1 . We define an NFA A n,∃φ := (Q, S, F ′ , ) with alphabet B n where

p v q := p ( 1v → ∪ 0v →) q F ′ := p ∃q ∈ F. p 10 n → ∪ 00 n → * q
In order to express the correctness properties of the construction above, we define an extension operation and a projection operation on words. Definition 12.9 For b : B * and v : B * n , we write b v for the word over B n+1 where the first components are given by b and the remaining components are given by v (filling with zeros or 0 n in case |b| = |v|). For v : B * n+1 , we write pr v : B * n for the result of removing the first component of every tuple.

The formalization of the results described in this section employs dependent types in a particularly pleasing manner. The type B n is represented using n-tuples (i.e., length-indexed lists) as provided by Ssreflect. The only type-changing operations employed in the proof are extension and projection (cf. Definition 12.9). The types : ∀n.B * → B * n → B * n+1 pr : ∀n.B * n+1 → B * n can be inferred automatically from the underlying list operations. This simplicity is, at least in part, due to the De Bruijn representation. Since quantifiers in De Bruijn representation always quantify over the variable 0, we never have to insert rows in the middle or remove any row but the first.

WS1S as a Representation for Regular Languages

We now prove the characterization theorem of Büchi [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF], Elgot [START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF], and Trakhtenbrot [START_REF] Trakhtenbrot | Finite automata and the logic of monadic predicates[END_REF] which establishes WS1S formulas as representations of regular languages. By assigning valuations to words over Σ , one can associate to the formula φ the language L Σ (φ ) of those words whose valuations satisfy the formula. Let n be the size of the alphabet Σ and assume bound φ ≤ n. The valuation corresponding to a word x : Σ * maps the variable X to the list of occurrences of the X-th symbol of Σ in the word x (or to the empty list if X ≥ n). Note that the valuation for x interprets the free variables of φ as a partition since there is exactly one symbol at every position. We formalize L Σ (φ ) by bijectively mapping the symbols of Σ to the unit vectors of length n, i.e., the elements of B n having exactly one occurrence of 1.

Definition 13.1 (Σ -language) Let n := |Σ | and for a : Σ let u a : B n be the unit vector with a single 1 at position rank a and 0 at all other positions. We write h Σ : Σ * → B * n for the homomorphism mapping each symbol a : Σ to u a . The Σ -language of a formula φ is then defined as

L Σ (φ ) := { x ∈ Σ * | V h Σ (x) |= φ } Lemma 13.2 L Σ (φ ) is regular. Proof Since L Σ (φ ) ≡ h -1 (L n (φ ))
, regularity follows with Theorems 7.14 and 12.15.

We now show that formulas can describe all regular languages by giving a language preserving translation from NFAs to formulas. To simplify the presentation, we describe the construction using named formulas. If a : Σ , we write P a for the free variable containing the positions of a in the input word. Further, we use lower-case letters for first-order variables represented using singleton, e.g., ∃x. x ∈ Y is just notation for ∃X. singleton(X) ∧ X ⊆ Y . The formalization in Coq is carried out using the De Bruijn representation used in the previous sections.

We fix some NFA A = (Q, S, F, →) (with alphabet Σ ) for the rest of this section. Further we set n := |Q| and refer to the individual states of A as q 0 , . . . , q n-1 . We now construct a formula φ A such that L Σ (φ A ) ≡ L (A).

The idea is to construct a formula of the form where φ max ensures that the witness for m is the length of the input word and φ run ensures that the witnesses for X n-1 . . . X 0 encode an accepting run of A. More precisely, k ∈ X i is to mean that after reading k symbols of the input word, the automaton is in state q i . We start by defining

φ A := ∃m.(φ max ∧ ∃X n-1 . . . X 0 . φ run ) φ part := ∀k.k ≤ m. q i ∈Q   k ∈ X i ∧ q j ∈Q∧q i =q j k / ∈ X j   φ init := ∀x.zero(x) → q i ∈S x ∈ X i φ fin := q j ∈F m ∈ X j φ trans := ∀k k ′ . succ(k, k ′ ) → k < m → q i a →q j k ∈ X i ∧ k ∈ P a ∧ k ′ ∈ X j φ run := φ part ∧ φ init ∧ φ fin ∧ φ trans
φ max := ∀k. k < m ↔ a∈Σ k ∈ P a
For φ run , we need to ensure that the X i form a partition of the set {0, . . . , m} in such way that 0 ∈ X i for some stating state q i , m ∈ X j for some final state q j , and if k ∈ X i and k + 1 ∈ X j then q i w[k] → q j . This leads to the definition of φ run given in Figure 1, where zero(x) ensures that x is (the singleton containing) 0 and succ(x, y) ensures that (the unique element of) y is the successor of (the unique element of) x. The formula employed here is a simplified version of the formula employed in [START_REF] Hofmann | Automatentheorie und Logik[END_REF] that more closely matches the notion of run defined in Section 6.

Lemma 13.3

Let A be an NFA over Σ . Then L Σ (φ A ) ≡ L (A).

Proof Let x ∈ Σ * . We show V h Σ (x) |= φ A iff x ∈ L (A). If x ∈ L (A) then there exists an accepting run (r i ) i≤|x| of A on x. We set the existential witness for m to |x| and for each X i to { k | ∃ j. r j = q i }. It is straightforward to verify that V h Σ (x) |= φ A with these instantiations.

Conversely, if V h Σ (x) |= φ A , we need to construct a run from the witnesses used for m and the X i . Since φ part is satisfied, the X j form a partition of {0, . . . , |x|}. We set r i to be the unique state q j such that i ∈ X j . Again, it is straightforward to verify that this constitutes an accepting run of A on x.

⊓ ⊔ Theorem 13.4 Let L ⊆ Σ * . Then L is regular iff L ≡ L Σ (φ ) for some φ .

Proof Immediate with Lemma 13.2 and Lemma 13.3. ⊓ ⊔ Remark 13.5 The proof of Lemma 13.3 relies on the fact that h(L Σ (φ )) is comprised of unit vectors only. In particular, there is no translation t from NFAs with alphabet B n to formulas satisfying L n (tA) ≡ L (A) for all A since L n (φ ) is always closed under adding or removing trailing 0 n vectors (Lemma 12.13).

While the simple structure of formulas in De Bruijn representation is nice when analyzing formulas recursively (as in the translation from formulas to NFAs), one has to be careful when manually writing down larger formulas. We decompose the formula describing NFA runs into parts of manageable size as shown in Figure 1 that each come with their own correctness lemmas that fully characterize the formula. The most complex monolithic formula is φ trans whose formalization spans 6 lines. The correctness proofs for various parts employ contexts of the form X 0 :: . . . :: X n-1 :: m :: I. That is, for the state q j the term rank q j (shifted to respect local quantifiers) refers to X j . Consequently, the X j can be accessed using readable names even in De Bruijn representation. For context lookups, the shifts required for local quantifiers can usually be eliminated though simplification (i.e., Coq's internal notion of computation). Consequently, wrong indices usually did not simplify as expected and where therefore easy to spot and correct.

Related Work

Given the theoretical and practical importance of regular language representations and their associated algorithms, there are a number of developments formalizing various aspects of the theory. This includes verified practical decision procedures as well as more mathematically minded developments like the one described in this paper.

Constable et al. [START_REF] Constable | Constructively formalizing automata theory[END_REF] constructively formalize automata theory, including the Myhill-Nerode theorem, in Nuprl. They use a notion of finite type to represent state sets. However, Nuprl allows the construction of (finite) quotient types with respect to undecidable relations. This allows proving the Myhill-Nerode theorem and the existence of a minimization function for DFAs assuming only decidability of the language. However, the minimization function obtained this way is computationally trivial, i.e., does not actually perform minimization [START_REF] Constable | Constructively formalizing automata theory[END_REF]Sect. 7.2].

On the Coq side, one of the earliest works is a verified translation from regular expressions to finite automata by Filliâtre [START_REF] Filliâtre | Finite automata theory in Coq: A constructive proof of kleene's theorem[END_REF]. Here, states are represented using finite sets of numbers leading to a representation that is considerably more difficult to work with than finite types. Further, there are a number of verified and executable decision procedures. Coquand and Siles [START_REF] Coquand | A decision procedure for regular expression equivalence in type theory[END_REF] build a reflective decision procedure for regular expression equivalence based on Brzozowski's algebraic method. The main technical difficulty in their work is in formalizing the termination argument, i.e., the fact that up to a certain decidable equivalence, regular expressions have only finitely many derivatives. In a substantial development, Braibant and Pous [START_REF] Braibant | Deciding Kleene algebras in Coq[END_REF] verify a more efficient decision procedure for regular expression equivalence based on finite automata and prove it sound and complete for all Kleene algebras (KA). For efficiency reasons, they represent state sets as bounded natural numbers. In [START_REF] Pous | Kleene algebra with tests and coq tools for while programs[END_REF], Pous describes a complete redesign of [START_REF] Braibant | Deciding Kleene algebras in Coq[END_REF] based on partial derivatives. As corollary of the completeness proof for an axiomatization of KA, he obtains a proof of Kleene's theorem. The completeness proof uses generalized automata represented as matrices over regular expressions. Moreira et.al. [START_REF] Moreira | Deciding kleene algebra terms equivalence in Coq[END_REF] develop a similar decision procedure for KA also based on partial derivatives.

On the HOL-side (i.e., Isabelle/HOL) the situation is more complex. Since quantification over types is not available in these systems, using types to represent state spaces is not feasible. One alternative representation is to use numbered states or bit lists [START_REF] Nipkow | Verified lexical analysis[END_REF]. However, this requires the explicit renaming of states when combining automata and weakens the type checking for automata. Due to this difficulty, much of the work on regular languages in Isabelle/HOL focuses on regular expressions rather than finite automata. This includes verified (partial correctness) decision procedures for regular expression and relation algebra equivalences [START_REF] Krauss | Proof pearl: Regular expression equivalence and relation algebra[END_REF], a decision procedure for WS1S and M2L(Str) based on regular expres- sions with projection [START_REF] Traytel | Verified decision procedures for MSO on words based on derivatives of regular expressions[END_REF], and a proof of the Myhill-Nerode theorem only using regular expressions [START_REF] Wu | A formalisation of the Myhill-Nerode theorem based on regular expressions[END_REF]. The last paper also includes a detailed discussion of the problem of defining a type of finite automata in Isabelle/HOL. In a substantial development, Berghofer [START_REF] Berghofer | Formalizing the logic-automaton connection[END_REF] develops a verified decision procedure for Presburger arithmetic based on finite automata over bit-strings.

More recently, and partly in response to [START_REF] Wu | A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)[END_REF] and [START_REF] Doczkal | A constructive theory of regular languages in Coq[END_REF], Paulson [START_REF] Paulson | A formalisation of finite automata using hereditarily finite sets[END_REF] formalized automata theory, including the Myhill-Nerode theorem and Brzozowski's minimization algorithm, in Isabelle/HOL based on hereditarily finite sets. Like finite types, HF sets have all the closure properties required for the usual constructions on finite automata. However, there are a number of differences. Due to the absence of dependent types, the definition of DFAs in [START_REF] Paulson | A formalisation of finite automata using hereditarily finite sets[END_REF] is split into a type that overapproximates DFAs and a predicate that checks wellformedness conditions (e.g., that the starting state is a state of the automaton). Finite types, being types, benefit from type checking and thus avoid the need for explicit well-formedness conditions. Moreover, many finite types are inductively defined data types (e.g., product and sum types) and thus allow pattern matching leading to more natural definitions.

Conclusion

We have shown that many results about regular languages can be obtained constructively and formally with reasonable effort. We have shown the equivalence of seven representations of regular languages (DFAs, NFAs, regular expressions, classifiers, 2DFAs, 2NFAs, and MSO formulas) and a number of closure properties of these representations. Equivalence of the various representations is obtained trough language-preserving translations as summarized in Figure 2. As part of the equivalence proof between formulas and NFAs, we establish decidability of satisfaction and satisfiability for WS1S. The part of this work where constructive logic forced us to deviate most from the presentation in the literature is the Myhill Nerode theorem. This led to the new notion of a classifier and a constructive reformulation of the theorem providing for the construction of DFAs from classifiers (cf. Remark 5.10). This construction is used to obtain redundant translations from 2FAs to DFAs providing better size bounds.

Obtaining an elegant formalization in Coq first requires rethinking the original proofs, which are mostly phrased in terms of classical set theory, in terms of the constructive type theory underlying Coq. Finite automata are a typical example of a finite dependently-typed mathematical structure. Consequently, finite types and dependent types are used pervasively throughout the whole development. Our representation of finite automata relies on dependent record types and finite types being first-class objects. Dependent types are also used to represent the possible configurations of a two-way automaton as a word-indexed collection of finite types and to obtain the vector languages for formulas.

In addition to the mathematical redesign, we implement all concepts in a manner that is both faithful to the mathematical development and easy to work with. The Coq development accompanying this paper [START_REF] Doczkal | Coq development accompanying this paper[END_REF] matches the paper proofs closely and provides the details elided in the paper. Altogether the Coq development consists of about 3000 lines of code (1300 lines of specification / 1700 lines of proof). The two biggest parts of the development are the results about WS1S (870 lines) and the results about two-way automata (550 lines). The conciseness of the Coq development is, at least in part, due to our use of the Mathematical Components Libraries (Math-Comp) [36], which provide the necessary infrastructure for our development. With the exception of modular arithmetic and binomial coefficients, our Coq development uses just about every concept provided by the Ssreflect component of Math-Comp (boolean reflection, finite and countable types, finite sets, graph reachability, length-indexed lists, etc.).

The present work shows that current interactive theorem proving tools (Coq and Ssreflect in our case) allow for a mathematically rewarding and reusable formalization of nontrivial results about regular languages with reasonable effort.

As mentioned above, the two most technical parts of our development are the translations from two-way automata to one-way automata and the the translations between NFAs and MSO formulas. We comment on each of these in turn.

The original translations from two-way automata to one-way automata [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF][START_REF] Vardi | A note on the reduction of two-way automata to one-way automata[END_REF] are described at a fairly informal level. When spelling out the details, the constructions and proofs become delicate and call for formalization, in particular if one does not have the robust intuitions of experts in automata theory. We adapt the proof of Shepherdson [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF] from deterministic two-way automata without end-markers to nondeterministic two-way automata with end-markers. This does not require conceptual changes. We had formalized the construction for 2DFAs (with end-markers) before realizing that the construction applies, with minimal changes, also to 2NFAs. That this is the case appears to be known to the experts [START_REF] Pighizzini | Two-way finite automata: Old and recent results[END_REF]. However, to the best of our knowledge, the construction was never published. We not only adapt Shepherdson's construction to 2NFAs, we also show that when applied to 2DFAs, the construction yields the bounds established in [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF]. One of the advantages of having formal proofs is that one can modify definitions and lemma statements and have the theorem prover point out the places in the proof that needed to be adapted. The process of adapting the construction from 2DFAs to 2NFAs profited greatly from this.

Similar to the translations from two-way automata to one-way automata, the translations between MSO formulas and NFAs are fairly technical. For the direction from formulas to NFAs, the main tool for factoring the proof into small lemmas is the introduction of extension and projection operations on words over bit-vectors. Here, we profit from the De Bruijn representation for formulas, which ensures that we never have to insert a row into the middle or remove a row other than the first. The translation from formulas to automata also establishes decidability of the satisfaction relation and satisfiability. The former establishes that the logic behaves classically, thus allowing us to show that the logical operations defined in terms of our minimal syntax behave correctly. These operations are then used in the translation from NFAs to formulas. As a consequence, and unlike in a classical setting, the correctness proofs for the two translations are not entirely independent.

  and h -1 (L) are decidable. Proof Let x : Σ * . Then x ∈ L•L ′ is decidable since there are only finitely many ways to split x. Decidability of x ∈ L * then follows by complete induction on |x| using the equivalence ax ∈ L * ↔ x ∈ R L (a) • L * . All other claims are trivial.

Lemma 4 . 4

 44 Let A 1 and A 2 be DFAs, and let ⊙ : B → B → B. Then one can construct DFAs accepting L (A 1 ) and {

⊓ ⊔ Example 4 . 7

 47 Let L = { a n b n | n ∈ N }. Then f n := a n satisfies the residual criterion.

Fact 5 .

 5 14 (∀P : Prop. P ∨ ¬P) ↔ ∀P : Prop. ∃A : dfa.L (A) ≡ { w | P }.

Remark 7 . 2

 72 ε) := {ε} L (e 1 + e 2 ) := L (e 1 ) ∪ L (e 2 ) L (a) := {a} L (e * ) := L (e) * Lemma 7.1 L (e) is a decidable language for every regular expression e.Proof Immediate with Lemma 3.1. ⊓ ⊔ In the Coq development, we directly assign decidable languages to regular expressions using the constructions underlying the proof of Lemma 3.1.

Lemma 7 . 3

 73 For every regular expression e one can construct an NFA accepting L (e) that has at most 2 • |e| states.

Lemma 8 . 4

 84 a bijection. The remaining properties are easy to verify.⊓ ⊔A straightforward consequence of Theorem 8.3 is the fact that every function that establishes connectedness and collapsedness without increasing the number of states is a correct minimization function. Let F : dfa → dfa such that for all A we have L (FA) ≡ L (A), |FA| ≤ |A|, and FA is connected and collapsed. Then for all A, FA is minimal (and accepts L (A)).

  --→ ya * (q, |ya| + 1) Since |xa| + 1 = |x| + 2 this follows immediately with Lemma 11.4. It remains to show (T xa).1 = (T ya).1. By symmetry, it suffices to show that (s, 1) |xa|+1 ---→ xa * (q, |xa| + 1) implies (s, 1) |ya|+1 ---→ ya * (q, |ya| + 1)

Fig. 1

 1 Fig.1Encoding of the runs of A

Fig. 2

 2 Fig. 2 Summary of translations between representations. The translation from 2NFAs to NFAs yields an automaton for the complement language.

  Let f : Σ * → Q be a classifier and let x be a word such that |Q| < |x|. Then there exists some word y such that |y| < |x| and f x = f y.

	Definition 5.1 We call a function f : Σ * → Q classifier if Q is a finite type and f is right-
	congruent, i.e., f (xa) = f (ya) whenever f x = f y.
	Lemma 5.2 Proof Since |Q| < |x|, there exist i, j such that i < j < |x| and f (x[0, i]) = f (x[0, j]). The
	claim then follows with right-congruence by setting y := x[0, i] • x[ j, |x|].	⊓ ⊔
	Theorem 5.3 (Cut-Off) Let f : Σ * → Q be a classifier and let P : Q → Prop. Then
	(∃x. P( f x)) ↔ ∃x. |x| ≤ |Q| ∧ P( f x)
	Proof By complete induction on |x| using Lemma 5.2.	⊓ ⊔
	Corollary 5.4 Let f : Σ * → Q be a classifier. Then ∃x. p( f x) and ∀x. p( f x) are decidable
	for all decidable predicates p : Q → B.
	Proof Decidability of ∃x. p( f x) follows with Theorem 5.3, since there are only finitely
	many words of length at most |Q|. Decidability of ∀x. p( f x) then follows from decidability
	of ∃x. ¬p( f x).	⊓ ⊔
	Corollary 5.5 Let f : Σ * → Q be a classifier. Then the image of f can be constructed as a
	subtype of Q.

  2•|e| states and the construction underlying Theorem 7.8 yields expressions of size O(|Σ | • |Q| • 4 2•|Q| ) (see the Coq development for a precise bound). While this may seem expensive, it matches the doubly exponential lower bound for the complementation of regular expressions

Here, abstract means that no witness can be extracted from the existence proof. The function xchoose X computes a witness by enumerating elements of X. The proof argument is only used to guarantee termination.

The language L := { a n b m | The n-th Turing machine holds within m steps on input ε } is decidable, but the image of L under the homomorphism mapping a to a and b to ε is undecidable.

In[START_REF] Kozen | Automata and computability[END_REF], δ is defined recursively starting from the right end of the word. In Coq, structural recursion is more natural and the impact on the proofs appears to be minimal.

Wu et al. [42] derive the closure of regular expressions under complement by proving the Myhill-Nerode theorem using regular expressions. The proof is significantly more complex than the automata constructions.

That the transitive closure of a decidable relation is decidable is established in the Ssreflect libraries using depth-first search.

Acknowledgements We thank Jan-Oliver Kaiser, who was involved in our previous work on one-way automata and also in some of the early experiments with two-way automata. We also thank Damien Pous and the anonymous reviewers for helpful comments.

† This author has been funded by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157). This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

The use of < for second-order variables allows us to employ a syntax without firstorder variables. First-order variables can be emulated using second-order variables that are required to be singletons. That is, we define predicates empty X := ∀Y.X ⊆ Y singleton X := ¬empty X ∧ ∀Y.¬emptyY → Y ⊆ X → X ⊆ Y and emulate the first-order quantifier ∃n.φ using ∃n.singleton n ∧ φ . If n and m are singletons, n < m corresponds to the usual less-than relation on the respective unique members. We remark that our MSO formulas are technically first-order formulas.

We begin by giving a formal definition of the satisfaction relation. Recall that variables are natural numbers. The formalization employs formulas in De Bruijn representation [START_REF] Abadi | Explicit substitutions[END_REF]. That is, the named binder ∃X.φ is replaced by the nameless binder ∃φ that always binds the variable 0 and lowers all free variables by one. The named formula ∃Y. X ⊆ Y is then represented as ∃(X + 1 ⊆ 0) as usual.

The satisfaction relation between valuations V : N → N * (finite sets being represented as lists) and formulas φ , written V |= φ , is defined by recursion on formulas:

Here, N :: V := λ n.if n = 0 then N else V (n -1) is the 'stream cons' operation on valuations and handles the shifting of free variables underneath of quantifiers. While valuations assign lists of natural numbers to the free variables, we will treat these these lists like finite sets and use standard set notations.

The first step in deciding V |= φ is to capture the fact that only the values that V assigns to the free variables of φ are relevant. We write bound φ for the least number n such that all free variables of φ are smaller than n. Lemma 12.1 If V and V ′ agree on all variables up to bound φ , then

For every n : N, the class of valuations that assign the empty lists to all variables X ≥ n can be represented using words over bit-vectors of length n. Definition 12.2 We write B n for the alphabet of bit-vectors of length n (i.e., n-tuples over B) and B * n for the type of words over B n . When talking about bit-vectors, we write 1 for true and 0 for false. We write 0 n for the bit-vector with n zeroes and 1v for extending the bit-vector v with a 1 on the left.

The valuation for v, written V v , is defined as

Example 12.4 Words over B n can be thought of as matrices where the characters are columns.

Then the X-th row of the matrix for a word v encodes V v (X). Consider the 5-letter word v over B 3 depicted by the following matrix.

Proof Claims (1) and ( 2) are easy to prove. Claims (3) and ( 4) follow with Lemma 12.1. ⊓ ⊔

Proof It suffices to show that every state q of A n+1,φ that accepts b v accepts v when seen as a state of A n,∃φ . We proceed by induction on b. The base case follows by induction on v. For the step case either v is nonempty and we can justify a transition in A n,∃φ or v is empty and A n+1,φ makes a transition from one final state of A n,∃φ to another.

⊓ ⊔ Lemma 12.12 Let v ∈ L (A n,∃φ ). Then b v ∈ L (A n+1,φ ) for some b : B * Proof Similar to the proof of the previous lemma. ⊓ ⊔ Lemma 12.13 Let v :

Lemma 12.14 Let A n+1,φ be an NFA accepting L n+1 (φ ). Then A n,∃φ accepts L n (∃φ ).

. By Lemma 12.12, there exists some b : Lemma 12.10(3). By Lemma 12.10(2) The construction outlined above yields a decision procedure of nonelementary complexity (Negation requires complementation, and thus determinization, while existential quantification introduces nondeterminism). This is essentially optimal [START_REF] Reinhardt | The complexity of translating logic to finite automata[END_REF].

This is a post-peer-review, pre-copyedit version of an article published in the Journal of Automated Reasoning. The final authenticated version is available online at: https://doi.org/10.1007/s10817-018-9460-x