State machines

Peter Hancock

Preliminary version: 23 Nov 2000

We want to arrange and relate the following notions connected with state machines and their specifications.

So far the points of interest are that Mealy machines and Moore machines are complementary; that we can with benefit generalise them to dependent types; and that a Moore machine is a “localised” transition system.

1 Machines

Let (C, R) be a pair of sets.

A Mealy machine with input C and output R consists of a set S whose elements are called states, a function m : S → (R × S)^{C}, and an initial state s_{0} : S.

A Mealey machine is often called simply a state machine, or deterministic automaton. Commonly the state set S is required to be finite, but here we don’t need to impose this cardinality restriction as part of the definition.

A Moore machine with input R and output C consists of a set S whose elements are called states, a function m : S → C × S^{R}, and an initial state s_{0} : S.

We write Me(C, R) for the class of Mealy machines with input C and output R, and Mo(C, R) for the class of Moore machines with input R and output C.

Observe that Mealy machines are passive, in the sense that they wait for an input, and respond with an output; conversely Moore machines are active, in the sense that they (spontaneously) send an output (in C) and wait for an input. We can say that Moore machines are clients and Mealy machines are servers.

Another way to describe these machines is that they are pointed coalgebras for the following endofunctors on the category of sets. (We leave the action on morphisms implicit.)

\begin{aligned}F_{Me}(S) & = & (R × S)^{C} \\ F_{Mo}(S) & = & C × S^{R} \end{aligned}

To say that they are pointed coalgebras means that they can be represented as elements of the final coalgebras for the respective functors. That is to say, • A Mealy machine is an element of νF_{Me}, which can be thought of as a

C-branching tree in which every node other than the root is labelled with an element of R. (Perhaps it would be better to say that it is a C-indexed forest of C-branching R-labelled trees.)

• A Moore machine is an element of νF_{Mo}, which can be thought of as a R-branching tree in which every node is labelled with an element of C.

Examples. One important example of a Mealey machine is the finite automaton part of a Turing machine. In this case, the input set C consists of the symbols which may appear in the tape cells, while (according to a common convention) the output set R = 2 + C represents the actions of moving the head left, moving the head right, or rewriting the cell currently under the head so that it holds a certain symbol.

One important example of a Moore machine is the tape (and transport part – it does not matter whether it moves the tape, or moves the machine) part of a Turing machine. In this case, the input set is the set R above, while the output set is the sset C above. The set of states can be represented in various ways; one may use the pair of the stream of characters to the left of the head, and the stream of characters under or the right of the head.

(There is some Haskell code which could go here.)

Dependent versions Here we start from a family {R(c) | c : C} of sets rather than a mere pair of sets. It is allowed that for certain commands c : C the set of responses R(c) can be empty. This sheds some light on the termination of machines. (Termination is sometimes represented by adjoining a special halt state, or a predicate of halting states.) In this case, the functors are as follows:

\begin{aligned}F_{Me}(S) & = & Πc : C.(R(c) × S) \\ F_{Mo}(S) & = & Σc : C.S^{R(c)} \end{aligned}

We call elements of the final coalgebras for these functors generalised machines.

An example of a generalised Moore machine. Recall that Martin-Löf’s W-type W (C, R) is the least solution W of the equation W = F_{Mo}(W), with typical element ⊔_{c}f where c : C and f : R(c) → W. Then the map ϕ : ⊔_{c}f ↦ ⟨c, f⟩ provides us with a coalgebra (W, ϕ) for F_{Mo}, and so any element t : W is the initial state of a generalised Moore machine. (As W is the least fixed point of F_{Mo}, such a machine eventually terminates, in the sense that it eventually issues a command for which no response is possible.)

2 Transition systems

A transition system is a triple (A, B, .[.]) where A is a set of states, B is a function which assigns a set B(a) to each element a : A, and .[.] is a binary function which to a : A and b : B(a) assigns a[b] : A.

\begin{aligned}A & : & Set \\ B & : & A → Set \\ .[.] & : & Πa : A.B(a) → A \end{aligned}

Note that a transition system is a coalgebra in the (super-large) category of types (large sets) for the (covariant) functor Fam, where Fam(X) = ΣI : Set.X^{I}. This is because a typical element of the type A → Fam(A) has the form

λ a.⟨B(a), λ b.a[b]⟩

Given such a structure, we can define two predicate transformers.

\begin{aligned}P^{□} & = & \{a | Πb : B(a).P (a[b])\} \\ P^{◇} & = & \{a | Σb : B(a).P (a[b])\} \end{aligned}

The accessible elements of A are those in the least prefixed point of .^{□} .

Acc = μP.P^{□} ⊆ P

The infinite elements of A are those in the greatest postfixed point of .^{◇} .

Inf = νP.P ⊆ P^{◇}

Observe that an element of Acc(a) for some a : A has the form ⊔f, where f : B(a) → Acc(a[b]).

Localisation to a universe. Let (U, T) be a universe (i.e. a set-indexed family of sets). Then we can define for each set X a set fam_{⟨U,T ⟩}(X).

fam_{⟨U,T ⟩}(X) = Σu : U.X^{T (u)}

Now we can define a localised version of a transition system to be a coalgebra for fam_{⟨U,T ⟩}. In other words, a ⟨U, T ⟩-localised transition system is a generalised Moore machine (forgetting about the initial state) with command set U, and response family {T (u) | u : U}. It issues as a command a code for a set, and then moves to a new state on receipt of an element of the set so coded.

It is natural now to look at coalgebras for the functor

S ↦ Πu : U.T (u) × S

that is, at generalised Mealy machines. Also, look at algebras as well as coalgebras.

3 Interaction systems

A interaction system is a quadruple (A, B, C, .[./.]) where A is a set of states, B is a function which assigns a set B(a) to each element a : A, C is a function which to a : A and b : B(a) assigns a set C(a, b), and .[./.] is a ternary function which to a : A and b : B(a) assigns a[b/c] : A.

A  : Set
B  : A → Set
C  : Πa : A.B(a) → Set
.[./.] : Πa : A, b : B(a).C(a, b) → A

Note that a interaction system is a coalgebra in the category of types (large sets) for the functor Fam^{2}. This is because a typical element of the type A → Fam^{2}(A) has the form

λ a.⟨B(a), λ b.⟨C(a, b), λ c.a[b/c]⟩⟩

Given such a structure, we can define two predicate transformers.

\begin{aligned}P^{□◇} & = & \{a | Πb : B(a).Σc : C(a, b).P (a[b/c])\} \\ P^{◇□} & = & \{a | Σb : B(a).Πc : C(a, b).P (a[b/c])\} \end{aligned}

The barred elements of A are those in the least prefixed point of .^{◇□} .

Bar = μP.P^{◇□} ⊆ P

The positive elements of A are those in the greatest postfixed point of .^{□◇} .

Pos = νP.P ⊆ P^{□◇}

Observe that an element of Bar(a) for some a : A has the form ⊔_{b}f, where b : B(a) and f : Πc : C(a, b).Bar(a[b/c]).

Localisation. If use a ⟨U, T ⟩ localised version of the Fam functor, so that an interaction system is a coalgebra for (fam_{⟨U,T ⟩})^{2}, then a typical localised interaction system has the form

λ a : A.⟨b̂(a) : U, λ b : T (b̂(a)).⟨ĉ(a, b) : U, λ c : T (ĉ(a, b)).a[b/c]⟩⟩

This doesn’t look so nice. But it may not be the right thing way to localise things.