# Quotient automaton

In computer science, in particular in formal language theory, a quotient automaton can be obtained from a given nondeterministic finite automaton by joining some of its states. The quotient recognizes a superset of the given automaton; in some cases, handled by the Myhill–Nerode theorem, both languages are equal.

## Formal definition

A (nondeterministic) finite automaton is a quintuple A = ⟨Σ, S, s$_0$, δ, S$_f$⟩, where:
* Σ is the input alphabet (a finite, non-empty set of symbols),
* S is a finite, non-empty set of states,
* s$_0$ is the initial state, an element of S,
* δ is the state-transition relation: δ ⊆ S × Σ × S, and
* S$_f$ is the set of final states, a (possibly empty) subset of S.
A string a$_1$...a$_n$ ∈ Σ is recognized by A if there exist states s$_1$, ..., s$_n$ ∈ S such that ⟨s$_{i-1}$,a$_i$,s$_i$⟩ ∈ δ for i=1,...,n, and s$_n$ ∈ S$_f$. The set of all strings recognized by A is called the language recognized by A; it is denoted as L(A).
For an equivalence relation ≈ on the set S of A’s states, the quotient automaton A/$_≈$ = ⟨Σ, S/$_≈$, [s$_0$], δ/$_≈$, S$_f$/$_≈$⟩ is defined by$^{:5}$
* the input alphabet Σ being the same as that of A,
* the state set S/$_≈$ being the set of all equivalence classes of states from S,
* the start state [s$_0$] being the equivalence class of A’s start state,
* the state-transition relation δ/$_≈$ being defined by δ/$_≈$([s],a,[t]) if δ(s,a,t) for some s ∈ [s] and t ∈ [t], and
* the set of final states S$_f$/$_≈$ being the set of all equivalence classes of final states from S$_f$.
The process of computing A/$_≈$ is also called factoring A by ≈.

## Example

Quotient examples :
| | Automaton diagram | Recognized language | Is the quotient of | Is the quotient of | Is the quotient of |
| | Automaton diagram | Recognized language | A by | B by | C by |
| A: | | 1+10+100 | | | |
| B: | | 1$^*$+1$^*$0+1$^*$00 | a≈b | | |
| C: | | 1$^*$0$^*$ | a≈b, c≈d | c≈d | |
| D: | | (0+1)$^*$ | a≈b≈c≈d | a≈c≈d | a≈c |
For example, the automaton A shown in the first row of the table is formally defined by
* Σ$^A$ = {0,1},
* S$^A$ = {a,b,c,d},
* s$^A$ $_0$ = a,
* δ$^A$ = { ⟨a,1,b⟩, ⟨b,0,c⟩, ⟨c,0,d⟩ }, and
* S$^A$ $_f$ = { b,c,d }.
It recognizes the finite set of strings { 1, 10, 100 }; this set can also be denoted by the regular expression "1+10+100".
The relation (≈) = { ⟨a,a⟩, ⟨a,b⟩, ⟨b,a⟩, ⟨b,b⟩, ⟨c,c⟩, ⟨c,d⟩, ⟨d,c⟩, ⟨d,d⟩ }, more briefly denoted as a≈b,c≈d, is an equivalence relation on the set {a,b,c,d} of automaton A’s states. Building the quotient of A by that relation results in automaton C in the third table row; it is formally defined by
* Σ$^C$ = {0,1},
* S$^C$ = {a,c},
* s$^C$ $_0$ = a,
* δ$^C$ = { ⟨a,1,a⟩, ⟨a,0,c⟩, ⟨c,0,c⟩ }, and
* S$^C$ $_f$ = { a,c }.
It recognizes the finite set of all strings composed of arbitrarily many 1s, followed by arbitrarily many 0s, i.e. { ε, 1, 10, 100, 1000, ..., 11, 110, 1100, 11000, ..., 111, ... }; this set can also be denoted by the regular expression "1$^*$0$^*$". Informally, C can be thought of resulting from A by glueing state a onto state b, and glueing state c onto state d.
The table shows some more quotient relations, such as B = A/$_{a≈b}$, and D = C/$_{a≈c}$.

## Properties

* For every automaton A and every equivalence relation ≈ on its states set, L(A/$_≈$) is a superset of (or equal to) L(A).$^{:6}$
* Given a finite automaton A over some alphabet Σ, an equivalence relation ≈ can be defined on Σ$^*$ by x ≈ y if ∀ z ∈ Σ$^*$: xz ∈ L(A) ↔ yz ∈ L(A). By the Myhill–Nerode theorem, A/$_≈$ is a deterministic automaton that recognizes the same language as A.$^{:65–66}$ As a consequence, the quotient of A by every refinement of ≈ also recognizes the same language as A.