Minimal Realization in Bicategories of Automata ^{∗}

Robert Rosebrugh Department of Mathematics and Computer Science Mount Allison University Sackville, N. B. E0A 3C0 Canada

N. Sabadini Dipartimento di Scienze dell’Informazione Università di Milano via Comelico, 39 30135 Milano, Italy

R. F. C. Walters School of Mathematics and Statistics University of Sydney Sydney, NSW 2006 Australia

Abstract

The context of this article is the program to develop monoidal bicategories with a feedback operation as an algebra of processes, with applications to concurrency theory. The objective here is to study reachability, minimization and minimal realization in these bicategories. In this setting the automata are 1-cells in contrast with previous studies where they appeared as objects. As a consequence we are able to study the relation of minimization and minimal realization to serial composition of automata using (co)lax (co)monads. We are led to define suitable behaviour categories and prove minimal realization theorems which extend classical results.

∗This work has been supported by NSERC Canada, Italian MURST and the Australian Research Council

1 Introduction

Katis, Sabadini, Walters, and Weld have described bicategories equipped with operations of serial and parallel composition, and feedback modelled as, respectively, composition of 1cells, a tensor product and an operation called feedback [KSW,SWW]. The bicategories are constructed from a base category C with a symmetric monoidal tensor ⊗. Objects are those of C and arrows (or processess) from X to Y are pairs (U, α) where α : X ⊗ U ⟶ U ⊗ Y. As mentioned above, composition models serial composition of circuits, there is a tensor product on circuits, and circuits from X ⊗ Q to Q ⊗ Y have a feedback operation whose result is a circuit from X to Y. In this article we concentrate on serial composition. In the case that the tensor is cartesian product the 1-cells were called circuits and used to study physical devices. In the case that the tensor is sum they were called Elgot automata and used as a model of algorithm. In [KSW] behaviour functors for these bicategories are also considered.

In this article our objective is to study three bicategories of automata: the bicategory of Mealy automata A which adds an initial state to the circuit model; the bicategory of Elgot automata E; and the bicategory of Σ-automata F which generalizes Elgot automata by labelling transitions from an alphabet Σ. The corresponding behaviours are, respectively, certain functions between input and output monoids, partial functions with duration, and certain matrices of languages. In each case we study reachability and minimization, and prove a minimal realization theorem. Reachability and minimization are described by idempotent (co)monads. Since the automata are arrows rather than objects, we are able to extend classical results to relate serial composition of automata with the reachability and minimization (co)monads found.

In Section 2 we define the bicategory A whose 1-cells are circuits with an initial state. Except for the lack of a finiteness condition, these are the classical Mealy automata [HU] and we use that name. This provides a setting in which both reachability and minimization can be considered. Reachability is described by a comonad (as has already been noted by Adamek and Trnkova [AT]) on each hom category and the coalgebras are the reachable automata. Minimization is a described by monads on the hom categories, and the algebras are minimal automata. With an appropriate definition of the behaviour of Mealy automata, we are able to prove a minimal realization theorem which extends Nerode’s theorem [Ner]. It provides a variant of Goguen’s minimal realization theory [Gog] and we extend this to include serial composition. The local situation, i. e. in a single hom category, is summarized in the following diagram. The reachable automata from X to Y are denoted A_{R}(X, Y); the subcategory of minimized automata is A_{R}^{M}(X, Y) and behaviours from X to Y are denoted B_{A}(X, Y). In the diagram F is minimization, E is behaviour and N is minimal realization.

[figure: A_{R}(X, Y); B_{A}(X, Y); N; E; ⊣; A_{R}(X, Y); I; F; ⊣; (A_{R})^{M}(X, Y); E′; N′; ≃]

In Section 3 we consider the bicategory E of Elgot automata which model algorithms and whose natural semantics is a partial function with duration. We again find a local comonad for reachability, and a local monad for minimization. We prove a minimal realization theorem here as well.

In Section 4 we generalize to allow labelled transitions, defining the bicategory F of Σautomata. Here the behaviour category has considerable interest—the arrows are matrices of languages with an ‘anti-prefix’ property.

To extend the results to the full process bicategories, i. e. to take account of serial composition, requires the (co)lax (co)monads introduced by Carboni and Rosebrugh [CR]. Reachability, minimization and our minimal realizations are idempotent (co)lax (co)monads. In Section 5 we recall results on lax monads and consider the idempotent case which concerns us.

Finally, in Section 6 we complete the picture above by showing that the minimizationminimal realization theory is compatible with serial composition. That is, the diagram above is valid in each case without the local restriction.

Throughout this article we are using the category set of sets as base category. In each section we use various algebraic properies of set. For the definition of the bicategory of Mealy automata we use only products. Elgot automata require only sums, and Σ-automata require the fact that set is a distributive category.

The authors wish to ackowledge discussions with Stephen Bloom.

2 Mealy Automata

We begin by defining a bicategory of circuits with initial state which we call Mealy automata. The initial state allows us to define the behaviour of a Mealy automaton as a function between free monoids. We define a category of behaviours so that behaviour is a homomorphism of bicategories. For Mealy automata reachability is a useful concept and we find local comonad structures compatible with serial composition. Our main result in this section, Theorem 17, involves a realization of behaviours of reachable Mealy automata using a Nerode-type construction.

Definition 1 The bicategory A of Mealy automata in set has

• Objects: the objects X, Y, ... of set

• Arrows: from X to Y are triples (U, α, u_{0}) where U is an object of set, α : X × U ⟶ U × Y and u_{0} : 1 ⟶ U (the input set is X, the output set is Y and the state set is U.)

• Identity arrow: on X is (1, t, 1_{1}) where t : X × 1 ⟶ 1 × X

• 2-Cells: from (U, α, u_{0}) to (U′, α′, u′_{0}) are arrows θ : U ⟶ U′ of set such that θu_{0} = u′_{0} and (θ × Y) · α = α′ · (X × θ)

• Composition of arrows: if (U, α, u_{0}) : X ⟶ Y and (V, β, v_{0}) : Y ⟶ Z then (V, β, v_{0})(U, α, u_{0}) = (U × V, (U × β)(α × V), (u_{0}, v_{0}))

• Vertical composition of 2-cells: if θ : (U, α, u_{0}) ⟶ (U′, α′, u′_{0}) and θ′ : (U′, α′, u′_{0}) ⟶ (U′′, α′′, u′′_{0}) then their vertical composite θ′ · θ is the arrow θ′θ of set

• Horizontal composition of 2-cells: if θ and ψ are horizontally composable their composite, denoted ψ ∘ θ is θ × ψ in set

Remark 2 If all references to initial state are removed from the preceding definition we obtain precisely the bicategory of circuits Circ as introduced in [KSW]. There is an evident forgetful homomorphism of bicategories A ⟶ Circ.

For further work, we first need to extend the domain of α to words in X^{∗}, the free monoid on X.

Definition 3 Let (U, α, u_{0}) : X ⟶ Y be a Mealy automaton and write α = < α_{U}, α_{Y} > . Define α_{U}^{∗} : X^{∗}×U ⟶ U inductively by: α_{U}^{∗}(ϵ, u) = u and for w ∈ X^{∗}, x ∈ X: α_{U}^{∗}(wx, u) = α_{U}(x, α_{U}^{∗}(w, u)). Similarly, α_{Y}^{∗} : X^{∗} × U ⟶ Y^{∗} is defined inductively by α_{Y}^{∗} (ϵ, u) = ϵ and for w ∈ X^{∗}, x ∈ X: α_{Y}^{∗} (wx, u) = α_{Y}^{∗} (w, u)α_{Y} (x, α_{U}^{∗}(w, u)).

Note that α_{U}^{∗}(wv, u) = α_{U}^{∗}(v, α_{U}^{∗}(w, u)) and α_{Y}^{∗} (wv, u) = α_{Y}^{∗} (w, u)α_{Y}^{∗} (v, α_{U}^{∗}(w, u)). Both equations are easily proved by induction on the length of v and are needed below.

We say that f : X^{∗} ⟶ Y^{∗} preserves initial subwords if whenever w = w_{1}w_{2} we have f(w) = f(w_{1})v for some v in Y^{∗}.

Definition 4 The category, B_{A}, of behaviours has the same objects as set. For objects X and Y the set of behaviours from X to Y, B_{A}(X, Y), is the set of functions f : X^{∗} ⟶ Y^{∗} for which f preserves initial subwords and length. Composition in B_{A} is inherited from set.

This notion of behaviour is derived from that of complete sequential machine mapping [Gin]. Under the condition of length preservation, the preservation of initial subwords implies that if w = w′x for x in X then f(w) = f(w′)y for some y in Y.

Definition 5 Let (U, α, u_{0}) : X ⟶ Y be in A and α =< α_{U}, α_{Y} > . The behaviour of (U, α, u_{0}) is the arrow E(U, α, u_{0}) : X ⟶ Y in B_{A}(X, Y) defined by E(U, α, u_{0})(w) = α_{Y}^{∗} (w, u_{0}) for w ∈ X^{∗}.

That the conditions for E(U, α, u_{0}) to be in B_{A}(X, Y) are satisfied is easily proved by induction. So are the following.

Lemma 6 If there is a 2-cell ϕ : (U, α, u_{0}) ⟶ (V, β, v_{0}) then for w ∈ X^{∗} and u ∈ U we have ϕ(α_{U}^{∗}(w, u)) = β_{V}^{∗} (w, ϕ(u)).

Proof. We procede by induction on the length of w. If w = ϵ, we have ϕ(α_{U}^{∗}(ϵ, u)) = ϕ(u) = β_{V}^{∗} (ϵ, ϕ(u)). Next suppose ϕ(α_{U}^{∗}(w, u)) = β_{V}^{∗} (w, ϕ(u)) and x ∈ X. We have ϕ(α_{U}^{∗}(wx, u)) = ϕ(α(x, α_{U}^{∗}(w, u))) = β(x, ϕ(α^{∗}(w, u)) = β(x, β_{V}^{∗} (w, ϕ(u)) = β_{V}^{∗} (wx, ϕ(u)), where the second equality is the definition of ϕ. The result follows.

Lemma 7 If there is a 2-cell ϕ : (U, α, u_{0}) ⟶ (V, β, v_{0}) then E(U, α, u_{0}) = E(V, β, v_{0}).

Proof. Again, we procede by induction on the length of w ∈ X^{∗}. Suppose w = ϵ. Then E(U, α, u_{0})(ϵ) = α_{Y}^{∗} (ϵ, u_{0}) = ϵ = β_{Y}^{∗} (ϵ, v_{0}) = E(V, β, v_{0})(ϵ). Next suppose E(U, α, u_{0})(w) = E(V, β, v_{0})(w) and x ∈ X. Then we get

E(U, α, u_{0})(wx) = α_{Y}^{∗} (wx, u_{0})
= α_{Y}^{∗} (w, u_{0})α_{Y} (x, α_{U}^{∗}(w, u_{0}))
= β_{Y}^{∗} (w, v_{0})β_{Y} (x, ϕ(α_{U}^{∗}(w, u_{0})))
= β_{Y}^{∗} (w, v_{0})β_{Y} (x, β_{V}^{∗} (w, ϕ(u_{0})))
= β_{Y}^{∗} (w, v_{0})β_{Y} (x, (β_{V}^{∗} (w, v_{0})))
= β_{Y}^{∗} (wx, v_{0}) = E(V, β, v_{0})(wx)

where the third equality is by the inductive assumption and the fourth uses the previous Lemma.

Recall that the category B_{A} may be viewed as a bicategory with discrete hom categories.

Proposition 8 Behaviour, E, extends to homomorphism of bicategories from A to B_{A}.

Proof. First, E is locally functorial by Lemma 7. A straightforward calculation using the equations after Definition 5 applied to a composite automaton shows that E preserves composition of 1-cells up to isomorphism.

Minimization of automata classically proceeds in two steps: first non-reachable states are discarded, and then states with equivalent behaviour are identified. We consider local versions of these steps in the bicategory of Mealy automata beginning with reachability.

Definition 9 For an automaton (U, α, u_{0}) : X ⟶ Y, the reachable states are U_{R} = {u ∈ U | ∃w ∈ X^{∗} α_{U}^{∗}(w, u_{0}) = u}. The reachable kernel of (U, α, u_{0}) is R(U, α, u_{0}) = (U_{R}, α_{R}, u_{0}), where α_{R} is the restriction of α.

We note immediately that R : A(X, Y) ⟶ A(X, Y) is functorial: the function θ : U ⟶ U′ defining a 2-cell (U, α, u_{0}) ⟶ (U′, α′, u′_{0}) clearly restricts to θ_{R} : U_{R} ⟶ U′_{R}. R is also evidently idempotent and there is an inclusion of (U_{R}, α_{R}, u_{0}) in (U, α, u_{0}). These inclusions are components of a natural transformation ρ : R ⟶ 1_{A}(X, Y). Thus,

Proposition 10 R is an idempotent comonad on A(X, Y) with counit ρ.

Coalgebras for R(= R(X, Y)) are called reachable automata, and they define a full subcategory A_{R}(X, Y) of A(X, Y). In Section 6 we will need the following.

Proposition 11 Let (U, α, u_{0}) : X ⟶ Y and (V, β, v_{0}) : Y ⟶ Z be Mealy automata. The assignment r_{UV} (u, v) = (u, v) defines a morphism of Mealy automata:

r_{UV} : R((V, β, v_{0})(U, α, u_{0})) ⟶ R(V, β, v_{0})R(U, α, u_{0}) : X ⟶ Z.

Proof. The underlying function of the comparison is an inclusion which is compatible with the actions. Indeed, let (u, v) ∈ (U × V)_{R}. We claim that (u, v) ∈ U_{R} × V_{R}. To see this recall that (U × β)(α × V)(x, u, v) = (α_{U}(x, u), β_{V} (α_{Y} (x, u), v), β_{Z}(α_{Y} (x, u), v)) and consequently (U × β)(α × V)_{U×V}^{∗} (w, (u, v)) = (α_{U}^{∗}(w, u), β_{V}^{∗} (α_{Y}^{∗} (w, u), v)). Thus, if (U × β)(α × V)_{U×V}^{∗} (w, (u_{0}, v_{0})) = (u, v)) then (α_{U}^{∗}(w, u_{0}), β_{V}^{∗} (α_{Y}^{∗} (w, u_{0}), v_{0})) = (u, v).

Next we consider state minimization for Mealy automata. As in classical automata theory, we define an equivalence relation on states and use the quotient set as states in constructing a ‘minimal’ automaton with the same behaviour.

The appropriate equivalence relation on states of (U, α, u_{0}) is defined by u ∼_{α} u′ iff ∀w ∈ X^{∗} we have α_{Y}^{∗} (w, u) = α_{Y}^{∗} (w, u′). Thus states are declared equivalent if they have the same output for all of X^{∗} under α^{∗}. The quotient automaton is M(U, α, u_{0}) = (U_{M}, α_{M}, [u_{0}]) where U_{M} = U/ ∼_{α} and α_{M} is defined on classes in U_{M} by α_{M}(x, [u]) = ([α_{U}(x, u)], α_{Y} (x, u)), where α =< α_{U}, α_{Y} >. This construction is well-defined. We give an example.

Example 12 Consider the Mealy automaton from X = {a, b} to Y = {0, 1} whose states are U = {u_{0}, u_{1}, u_{2}}, start state is u_{0} and action α is indicated in the following picture, where e. g. α(a, u_{0}) = (u_{1}, 1)

[figure: u_{0}; u_{1}; a/1; u_{2}; b/0; a/0; b/1; b/1; a/0]

To determine ∼_{α} note that α_{Y} (u_{0}, a) = 1 while α_{Y} (u_{1}, a) = 0, so u_{0} is not equivalent to u_{1}. On the other hand an easy induction shows that α_{Y}^{∗} (u_{1}, w) = α_{Y}^{∗} (u_{2}, w) for all w ∈ X^{∗} so u_{1} ∼_{α} u_{2}. Thus the minimized automaton has the following state diagram:

[figure: [u_{0}]_{α}; [u_{1}]_{α}; a/1; b/0; a/0; b/1]

The behaviour of both the original and minimized automata is given by f : X^{∗} ⟶ Y^{∗} where for w in X^{∗}:

f(w) = \{ \begin{matrix}ϵ & if w = ϵ \\ 1v & if w = aw′ \\ 0v & if w = bw′ \end{matrix}

and v is the image of w′ under the homomorphism from X^{∗} to Y^{∗} mapping a to 0 and b to 1.

M is functorial on A(X, Y) and idempotent. The quotient mapping defines a 2-cell η_{(U,α,u_{0})} : (U, α, u_{0}) ⟶ M(U, α, u_{0}). The η_{(U,α,u_{0})} are components of a natural transformation from 1_{A(X,Y)} to M.

Proposition 13 The functor M is an idempotent monad on A(X, Y) with unit η.

Algebras for M(= M(X, Y)) are called minimal automata, and define a full subcategory A^{M}(X, Y) of A(X, Y). For use in Section 6 we note the following.

Proposition 14 Let (U, α, u_{0}) : X ⟶ Y and (V, β, v′_{0}) : Y ⟶ Z be Mealy automata. The assignment m_{UV} ([u], [v]) = [(u, v)] defines a 1-cell of Mealy automata:

m_{UV} : M(V, β, v′_{0})M(U, α, u_{0}) ⟶ M((V, β, v′_{0})(U, α, u_{0})) : X ⟶ Z

.

Proof. The underlying function of the comparison is easily described. Indeed, for ([u], [v]) ∈ U_{M} × V_{M} we define m_{UV} ([u], [v]) = [(u, v)] ∈ (U × V)_{M}. To see that this is well-defined, recall that (U × β)(α × V)(x, u, v) = (α_{U}(x, u), β_{V} (α_{Y} (x, u), v), β_{Z}(α_{Y} (x, u), v)). Suppose that u ∼ u′ and v ∼ v′. Denote the action of the composite automaton (V, β, v′_{0})(U, α, u_{0}) by γ, so for any x ∈ X we have γ_{Z}(x, (u, v)) = β_{Z}(α_{Y} (x, u), v) = β_{Z}(α_{Y} (x, u′), v) = β_{Z}(α_{Y} (x, u′), v′) = γ_{Z}(x, (u′, v′)). Consequently, for any w ∈ X^{∗} we have γ_{Z}^{∗}(w, (u, v)) = γ_{Z}(w, (u′, v′)) so [(u, v)] = [(u′, v′)]. Similar arguments show that m_{UV} is a morphism of A.

We observe that taking the reachable kernel and the minimization for Mealy automata are processes which commute up to isomorphism, i. e. the minimization of the reachable kernel of (U, α, u_{0}) is isomorphic to the reachable kernel of its minimization. These are simply seen from the definitions above. Consequently, the minimization monad restricts to a monad M′ on A_{R}(X, Y) and the reachability comonad restricts to a comonad R′ on A^{M}(X, Y). The category of algebras for the restriction of M is isomorphic to the coalgebras for the restriction of R. The situation we have been describing is summed up in the following diagram. The pairs of functors are adjoint and both the inner and outer squares commute. The I’s (resp. J’s) are inclusions adjoint to the reflectors F and F′ (resp. coreflectors G and G′.)

[figure: A^{M}(X, Y); (A_{R})^{M′}(X, Y); A(X, Y); A_{R}(X, Y); G; F; F′; (A^{M})_{R′}(X, Y); J′; G′; ≅; I; J; I′]

Our next objective is the adjunction between minimal realization and behaviour. Though we have defined behaviour for an arbitrary automaton, the realization of a behaviour constructed below is necessarily reachable, so our adjunction refers to A_{R}(X, Y). We begin construction of the minimal realization of a behaviour by defining a crucial equivalence relation. Let f : X ⟶ Y be a behaviour from X to Y. For w, w′ ∈ X^{∗}, we define w ∼_{f} w′ iff

∀v ∈ X^{∗} f(wv) = f(w)y and f(w′v) = f(w′)y′ ⇒ y = y′.

It is easy to check that ∼_{f} is indeed an equivalence relation and we denote equivalence classes by [w]_{f}.

Definition 15 The Nerode automaton of a behaviour f : X ⟶ Y is the Mealy automaton Nf = (X^{∗}/ ∼_{f}, α_{f}, [ϵ]_{f}) with α_{f}(x, [w]_{f}) = ([wx]_{f}, y) where w ∈ X^{∗}, x ∈ X, y ∈ Y and f(wx) = f(w)y.

We first have to ensure that α_{f} is well-defined i.e. if w ∼_{f} w′ then wx ∼_{f} w′x and y = y′ where f(w′x) = f(w′)y. For any v ∈ X^{∗} we have f(wxv) = f(wx)z = f(w)yz for some y ∈ Y and z ∈ Y^{∗}. Similarly, f(w′xv) = f(w′x)z′ = f(w′)y′z′. Since w ∼_{f} w′, we conclude that yz = y′z′ whence y = y′, z = z′ and so also wx ∼_{f} w′x, as required.

We also note that Nf is reachable by its definition. As an example we construct the Nerode automaton for the behaviour found in in Example 12 above.

Example 16 Recall that f in B_{A}(X, Y) was defined (as a function from X^{∗} to Y^{∗}) by the formula:

f(w) = \{ \begin{matrix}ϵ & if w = ϵ \\ 1u & if w = aw′ \\ 0u & if w = bw′ \end{matrix}

and u is the image of w′ under the homomorphism from X^{∗} to Y^{∗} mapping a to 0 and b to 1. We need to determine the equivalence relation ∼_{f} and its classes. This is straightforward since it is easy to show that (i) a ∼_{f} b ∼_{f} aw ∼_{f} bw for any w ∈ X^{∗} and (ii) ϵ ≁_{f} a. To see the relations (i), note that if v is arbitrary in X^{∗} then for any w ∈ {a, b, aw′, bw′} we have f(wv) = f(w)u where u is the image of v under the homomorphism above, independent of f(w). For (ii) it is enough to observe that f(ϵb) = f(ϵ)0 while f(ab) = f(a)1 and 0 ≠ 1 whence ϵ ≁_{f} a. Now the action on Nf and the isomorphism of Nf with the minimized automaton displayed in Exercise 12 are obvious.

The following result is a variant of Goguen’s adjunction between minimal realization and behaviour. He considered machines which emitted a single output letter after reading the entire input. His behaviours were arbitrary functions from X^{∗}toY. We have taken account of the entire output sequence and consequently need the more complete definition of behaviours found above. In case Y = {0, 1} and all objects are finite sets, the result is a version of Nerode’s Theorem [Ner].

Theorem 17 The behaviour of the Nerode automaton of f is f, i.e. ENf = f. Moreover, we have

E ⊣ N : B_{A}(X, Y) ⟶ A_{R}(X, Y).

Proof. We prove the first statement by induction. First, E(Nf)(ϵ) = ϵ = f(ϵ). Now let w ∈ X^{∗} and x ∈ X. Assuming E(Nf)(w) = f(w), we have

E(Nf)(wx) = E(Nf)(w)(α_{f})_{Y} (x, (α_{f})_{U}^{∗}(w, [ϵ]_{f}))
= f(w)(α_{f})_{Y} (x, (α_{f})_{U}^{∗}(w, [ϵ]_{f}))
= f(w)(α_{f})_{Y}^{∗} (x, [w]_{f})
= f(w)y where f(w)y = f(wx)
= f(wx).

The desired equality of behaviours follows.

For the stated adjunction, we need to show that 2-cells (in B_{A}(X, Y)) from E(U, α, u_{0}) to f are in natural bijection with 2-cells (in A_{R}(X, Y)) from (U, α, u_{0}) to Nf. Since B_{A} is locally discrete, this amounts to showing that E(U, α, u_{0}) = f if and only if there is a unique 2-cell from (U, α, u_{0}) to Nf.

For sufficiency we observe that if there is (U, α, u_{0}) ⟶ Nf, then E(U, α, u_{0}) = ENf = f, by Lemma 7 and the result of the previous paragraph.

For necessity, suppose E(U, α, u_{0}) = f and we define a unique 2-cell ϕ : (U, α, u_{0}) ⟶ Nf. We begin by recalling that (U, α, u_{0}) is reachable and define \overline{ϕ} : U ⟶ U_{f} by \overline{ϕ}(u) = [w]_{f} for some w ∈ X^{∗} such that α_{U}^{∗}(w, u_{0}) = u. We need to show that \overline{ϕ} is well-defined, that it defines an 2-cell in A_{R}, and that it is the only such 2-cell.

We show first that \overline{ϕ}(u) does not depend on the choice of w ∈ X^{∗} such that α_{U}^{∗}(w, u_{0}) = u. Indeed, suppose that α_{U}^{∗}(w, u_{0}) = u = α_{U}^{∗}(w′, u_{0}). For v ∈ X^{∗}, let f(wv) = f(w)y and f(w′v) = f(w′)y′. For brevity denote E(U, α, u_{0}) by E and recall that E = f, so f(w)y = f(wv) = E(wv) = E(w)α_{Y}^{∗} (v, u) = f(w)α_{Y}^{∗} (v, u) and we conclude y = α_{Y}^{∗} (v, u). Similarly, f(w′)y′ = f(w′)α_{Y}^{∗} (v, u). Thus y = α_{Y}^{∗} (v, u) = y′.

Next, \overline{ϕ}(u_{0}) = [ϵ]_{f}, the initial state of Nf and to see that α_{f}(X × \overline{ϕ}) = (\overline{ϕ} × Y)α, let (x, u) ∈ X × U. Suppose α_{U}^{∗}(w, u_{0}) = u since (U, α, u_{0}) is reachable. Now α_{f}(X × \overline{ϕ})(x, u) = α_{f}(x, \overline{ϕ}(u)) = α_{f}(x, \overline{ϕ}(α_{U}^{∗}(w, u_{0})) = α_{f}(x, [w]_{f}) = ([wx]_{f}, y) and f(wx) = f(w)y. On the other hand,

(\overline{ϕ} × Y)α(x, u) = (\overline{ϕ}(α_{U}(x, u)), α_{Y} (x, u))
= (\overline{ϕ}(α_{U}(x, α_{U}^{∗}(w, u_{0})), α_{Y} (x, α_{U}^{∗}(w, u_{0})))
= (\overline{ϕ}(α_{U}^{∗}(wx, u_{0}), y′)
where α_{Y}^{∗} (wx, u_{0}) = E(U, α, u_{0})(wx) = f(wx) = f(w)y′
= ([wx]_{f}, y)

Finally, we show \overline{ϕ} is the unique 2-cell from (U, α, u_{0}) to Nf. If ψ is another such 2-cell then ψ(u_{0}) = [ϵ] = \overline{ϕ}(u_{0}) is necessary, so ψ = \overline{ϕ} on all states reachable from u_{0} by words of length 0. Now assume ψ = \overline{ϕ} on all states reachable from u_{0} by words of length | w | or less. For any x ∈ X if u = α_{U}^{∗}(wx, u_{0}), letting u′ = α_{U}^{∗}(w, u_{0}), we have

ψ(u) = ψ(α_{U}(x, u′)) by definition of u′
= (α_{f})_{U}(x, ψ(u′)) since ψ in A_{R}
= (α_{f})_{U}(x, \overline{ϕ}(u′)) by hypothesis
= \overline{ϕ}(α_{U}(x, u′))
= \overline{ϕ}(u)

So ψ = \overline{ϕ}.

We consider the equivalence of reachable minimized automata and behaviours in Section 6. With that exception, the theorem above completes the description of reachability, minimization and minimal realization for Mealy automata summarized in the diagram in the Introduction.

3 Elgot Automata

This section studies a bicategory of automata which can be used to model algorithms. The name arises from Elgot’s work on sequential algorithms. Elgot automata have been used by Sabadini, Walters and Vigna [SWV] to define partial recursive functions, and by Vigna [Vig] to define the Blum-Shub-Smale computable functions [BSS].

Definition 18 [KSW] The bicategory E of Elgot automata in set has

• Objects: the objects X, Y, ... of set

• Arrows: from X to Y are pairs (U, α) where U is an object of set (called the internal states of (U, α)) and α : X + U ⟶ U + Y (the transition morphism)

• Identity arrow: on X is (0, 1_{X})

• 2-Cells: from (U, α) to (U′, α′) are functions θ : U ⟶ U′ of set such that (θ + Y) · α = α′ · (X + θ)

• Composition of arrows: if (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z then (V, β)(U, α) = (U + V, (U + β)(α + V))

• Vertical composition of 2-cells: if θ : (U, α) ⟶ (U′, α′) and θ′ : (U′, α′) ⟶ (U′′, α′′) then their vertical composite θ′ · θ is the function θ′θ of set

• Horizontal composition of 2-cells: if θ and ψ are horizontally composable their composite, denoted ψ ∘ θ is θ + ψ in set

The semantics of an Elgot automaton might be viewed simply as the partial function from X to Y given, where defined, by the unique value in Y resulting from iterating α one or more times. To obtain our minimal realization theorems we will need to record also the “duration” of the process. We use the notation “⇀” to denote a partial function.

Definition 19 Let (U, α) : X ⟶ Y be an Elgot automaton. The behaviour of (U, α) is the partial function E(U, α) : X ⇀ Y × IN defined by E(U, α)(x) = (y, n) if α^{n+1}(x) = y ∈ Y (and undefined otherwise.)

Motivated by the preceding definition, we define a category of behaviours B_{E} to have the same objects as set, and as arrows from X to Y, the partial functions from X to Y × IN. In B_{E} the composite of f : X ⟶ Y and g : Y ⟶ Z is defined by gf(x) = (z, m + n) when both f(x) = (y, n) and g(y) = (z, m) are defined, and undefined otherwise. As we observed for Mealy automata:

Lemma 20 If there is a 2-cell ϕ : (U, α) ⟶ (U′, α′) in E then E(U, α) = E(U′, α′).

Proof. This follows by induction from the fact that an 2-cell of automata is a function between state objects which commutes with the action.

Viewing B_{E} as a bicategory with discrete hom categories we get:

Proposition 21 Behaviour, E, extends to homomorphism of bicategories from E to B_{E}.

Proof. First, E is locally functorial by Lemma 20. It is easy to see that the behaviour of a serial composite of Elgot automata is the composition in B_{E} of their behaviours.

Definition 22 Let (U, α) : X ⟶ Y be an Elgot automaton. The object of reachable states of (U, α) is

U_{R} = {u ∈ U | ∃x ∈ X ∃n ∈ IN α^{n}(x) = u}.

The reachable kernel of (U, α) is the automaton R(U, α) = (U_{R}, α_{R}) : X ⟶ Y where α_{R} : X + U_{R} ⟶ U_{R} + Y is the restriction of α.

The first thing to observe is that R : E(X, Y) ⟶ E(X, Y) is functorial, idempotent and that there is a 2-cell ρ_{(U,α)} : R(U, α) ⟶ (U, α) which is the component of a natural transformation from R to 1_{E(X,Y)}. Each of these facts follows after a short diagram chase. Moreover, it is easy to see that Rρ = ρR, since each amounts to a transformation with identity components. We summarize:

Proposition 23 The functor R is an idempotent comonad on E(X, Y) with counit ρ.

Corollary 24 The behaviour of the reachable kernel, R(U, α), of an Elgot automaton, (U, α) is the same as that of (U, α).

Coalgebras for the local reachability comonads are ‘reachable’ Elgot automata, i.e. automata all of whose internal states are visited under the iterated action of α on at least one x ∈ X. We note, for later use, a comparison between the reachable kernel of a composite and the composite of reachable kernels.

Proposition 25 If (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z, then there is a canonical 2-cell r_{UV} : R((U, α)(V, β)) ⟶ R(U, α)R(V, β).

Proof. To see this, we observe that if w ∈ (U + V)_{R}, then w ∈ U_{R} + V_{R}, and that the appropriate restrictions of α and β are defined.

We have a minimization theory for Elgot automata which will lead to a particularly simple description of minimized automata. We begin with an equivalence relation on states of (U, α): u ∼_{α} u′ iff for all n > 0, for all y ∈ Y, α^{n}(u) = y iff α^{n}(u′) = y. Thus states are declared equivalent if they reach the same point in Y after the same duration, or if they both never reach Y. We can construct a ‘quotient’ automaton M(U, α) = (U_{M}, α_{M}). We define U_{M} = U/ ∼_{α} and α_{M} is defined on X + U_{M} by

α_{M}(x) = \{ \begin{matrix}[u] & if α(x) = u ∈ U \\ y & if α(x) = y ∈ Y \end{matrix} α_{M}([u]) = \{ \begin{matrix}[u′] & if α(u) = u′ ∈ U \\ y & if α(u) = y ∈ Y. \end{matrix}

Proposition 26 The quotient arrow η : U ⟶ U_{M} underlies a 2-cell in E denoted η_{(U,α)} : (U, α) ⟶ M(U, α). Applying M to it gives an isomorphism, and M is an idempotent monad on E(X, Y).

Any algebra for M is a reachable automaton isomorphic to one of the following. States are (some of) the pairs consisting of an element of y in Y and a positive integral ‘duration to Y’ (plus possibly a ‘non-terminating’ state). The action on input x is direct transition from X to Y or direct transition from X to an internal state. On state (y, n) the action is ‘reduction of duration’ to (y, n−1) when n ≥ 2, and (y, 1) to y. The picture below illustrates the idea, and guides the proof of the preceding proposition.

[figure: x_{0}; (y, n − 1); x_{1}; (y, n); x_{2}; (y′, n′); (y, n − 1); (y′, n′ − 1); ⋯; ⋯; (y, 1); y; (y′, 1); y′; x_{3}; y′′; ⋮; ⋮; ⋮; x_{i}; ∗; ⋮; ⋮; ⋮; X; U_{M}; Y]

Our next objective is a minimal realization of any behaviour in B_{E}. The idea is simply to construct an automaton like that pictured above for a specified behaviour. Let f : X ⟶ Y × IN be a behaviour from X to Y. The state set for the minimal realization automaton Nf is:

U_{f} = \{ \begin{matrix}\{(y, m) | ∃n ≥ m ≥ 1 ∃x ∈ X f(x) = (y, n)\} & if f is fully defined \\ \{(y, m) | ∃n ≥ m ≥ 1 ∃x ∈ X f(x) = (y, n)\} ⋃\{∗\} & otherwise \end{matrix}

The action for the minimal automaton is defined on X by:

α_{f}(x) = \{ \begin{matrix}f(x) & if p_{2}(f(x)) > 0 \\ p_{1}(f(x)) & if p_{2}(f(x)) = 0 \\ * & if f(x) not defined \end{matrix}

where the p_{i} are projections from Y × IN. On U_{f} we define:

α_{f}(u) = \{ \begin{matrix}(y, n − 1) & if u = (y, n) and n > 1 \\ y & if u = (y, 1) \\ * & if u = ∗ \end{matrix}

This makes α_{f} : X + U_{f} ⟶ U_{f} + Y, and we note that the automaton Nf = (U_{f}, α_{f}) is reachable.

Proposition 27 The behaviour of Nf = (U_{f}, α_{f}) is f. Furthermore, we have E is left adjoint to N : B_{E}(X, Y) ⟶ E_{R}(X, Y).

Proof. The diagram above indicates why the first statement holds: the constructed automaton simply has states which provide transitions of correct duration for elements of X where f is defined and a loop elsewhere.

For the adjunction, we show that 2-cells (in B_{E}(X, Y)) from E(U, α) to f correspond to 2-cells (in E_{R}(X, Y)) from (U, α) to Nf. Since B_{E} is locally discrete, that is to show that E(U, α) = f if and only if there is a unique 2-cell from (U, α) to Nf.

For sufficiency observe that if there is (U, α) ⟶ Nf, then E(U, α) = ENf = f, by Lemma 20 and the previous paragraph.

For necessity, we suppose E(U, α) = f and seek to define a unique 2-cell ϕ : (U, α) ⟶ Nf. Recalling that (U, α) is reachable we define ϕ : U ⟶ U_{f} by:

ϕ(u) = \{ \begin{matrix}(y, n) & if α^{n}(u) = y for some n > 0 \\ * & if there is no such y \end{matrix}

We need to show that ϕ is well-defined, that it defines a 2-cell in E_{R}, and that it is the only such 2-cell. The first two follow immediately from E(U, α) = f. For the last simply observe that (y, n) is the only state of U_{f} for which α_{f}(y, n)^{n} = y, while ∗ is the only ‘looping’ state. Hence, the requirement that ϕ be a morphism leaves no choice in the definition of ϕ(u).

4 Σ-Automata and Matrices of Languages

Let Σ be an alphabet which we fix for this section. The model in the preceding section is here generalized to allow deterministic state transitions labeled by elements of Σ. The resulting behaviours are certain matrices of languages. Non-deterministic automata whose behaviours are also matrices have been considered by Bloom, Sabadini and Walters [BSW].

Definition 28 The bicategory F of Σ-automata in set has

• Objects: the objects X, Y, ... of set • Arrows: from X to Y are pairs (U, α) where U is an object of set

(called the internal states of (U, α)) and α : X + (U × Σ) ⟶ U + Y the transition morphism, with components α_{X} : X ⟶ U + Y and α_{U} : U × Σ ⟶ U + Y

• Identity arrow: on X is (0, 1_{X})

• 2-Cells: from (U, α) to (U′, α′) are functions θ : U ⟶ U′ of set such that (θ + Y) · α = α′ · (X + (θ × Σ))

• Composition of arrows: if (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z then (V, β)(U, α) = (U + V, (U + β)(α + (V × Σ))(X + δ)) where δ : (U + V) × Σ ⟶ U × Σ + V × Σ is the distributive law

• Vertical composition of 2-cells: if θ : (U, α) ⟶ (U′, α′) and θ′ : (U′, α′) ⟶ (U′′, α′′) then their vertical composite θ′ · θ is the function θ′θ of set

• Horizontal composition of 2-cells: if θ and ψ are horizontally composable their composite, denoted ψ ∘ θ is θ + ψ in set

The idea here is that transitions among states of a Σ-automaton are labelled by elements of Σ. An Elgot automaton is essentially the special case where Σ has one element. We write Σ^{+} for the free semi-group on Σ (or the words of length one or more in Σ^{∗}.)

Definition 29 Let (U, α) : X ⟶ Y be a Σ-automaton. Define a partial function α_{U}^{+} : U × Σ^{+} ⇀ U + Y as follows. For a ∈ Σ and w ∈ Σ^{+}

α_{U}^{+}(u, a) = α_{U}(u, a) α_{U}^{+}(u, wa) = \{ \begin{matrix}α_{U}(α^{+}(u, w), a) & if α_{U}^{+}(u, w) ∈ U \\ undefined otherwise. \end{matrix}

Define a partial function α^{∗} : X × Σ^{∗} ⇀ U + Y by α^{∗}(x, ϵ) = α_{X}(x) and for w ∈ Σ^{+},

α^{∗}(x, w) = \{ \begin{matrix}α^{+}(α(x), w) & if α_{X}(x) ∈ U \\ undefined otherwise. \end{matrix}

This extension of α to Σ^{∗} allows us to define the behaviour of a Σ-automaton. For each x ∈ X and each y ∈ Y we have a language over Σ which is the set of labels of paths under the action of α from X to Y. Together we obtain an X × Y matrix of languages. More precisely, Definition 30 Let (U, α) : X ⟶ Y be a Σ-automaton. The behaviour of (U, α) is the X × Y matrix of Σ-languages E(U, α)_{x,y} where E(U, α)_{x,y} = {w ∈ Σ^{∗}|α^{∗}(x, w) = y}.

Notice that this definition can be interpreted as generalizing that of behaviour for an Elgot automaton. If we have an Elgot automaton (U, α) : X ⟶ Y we can define a Σautomaton for Σ_{a} = \{a\} as \overline{α} : X + (U × Σ_{a}) ⟶ U + Y where \overline{α}_{X}(x) = α_{X}(x) for x ∈ X and \overline{α}_{U}(u, a) = α_{U}(u). Then observe that \overline{α}^{∗}(x, a^{n}) = α^{n+1}(x) and both sides of the equation are either are either defined or undefined. Thus E(U, α)(x) = (y, n) iff E(U, \overline{α})_{x,y} = \{a^{n}\} (and E(U, α)(x) is undefined iff E(U, \overline{α})_{x,y} = ∅ for all y.)

We note some important properties of behaviours. First, since our automata are deterministic, for a fixed x the E(U, α)_{x,y} are pairwise disjoint. Moreover, if w ∈ E(U, α)_{x,y} and v ∈ Σ^{+} then wv ∉ E(U, α)_{x,y′} for any y′ (including y). This motivates the following definitions.

Definition 31 A language L ⊆ Σ^{∗} is anti-prefix if for all w, v ∈ Σ^{∗}(w ∈ L and wv ∈ L imply v = ϵ). Languages L_{1} and L_{2} are anti-prefix-disjoint if for all w, v ∈ Σ^{∗}(w ∈ L_{1} implies wv ∉ L_{2}), and vice versa.

Note that we may take v = ϵ in the second definition, so anti-prefix-disjoint languages are disjoint.

Proposition 32 Let L and M be X×Y and Y ×Z matrices of languages such that the entries of L and M are anti-prefix languages and the entries in each row of L and M are pairwise anti-prefix-disjoint. The X×Z matrix K = LM with entries defined by K_{x,z} = ⋃_{y∈Y} L_{x,y}M_{y,z} has anti-prefix entries and entries in each row are pairwise anti-prefix-disjoint.

Proof. We first show that the entries of LM are anti-prefix. Let w ∈ LM_{x,z} so there are y ∈ Y, w_{1} ∈ L_{x,y}, w_{2} ∈ M_{y,z} such that w = w_{1}w_{2}. Now suppose wv ∈ LM_{x,z} so there are y′ ∈ Y, v_{1} ∈ L_{x,y′}, v_{2} ∈ M_{y′,z} such that w = v_{1}v_{2}. We distinguish 3 cases: Case 1: |v_{1}| < |w_{1}|. In this case w_{1} = v_{1}v_{3} for some v_{3} with |v_{3}| > 0. If y = y′ this contradicts the prefix property of L_{x,y}. Otherwise, since entries in a row of L are pairwise anti-prefix-disjoint v_{1} ∈ L_{x,y′} implies w_{1} = v_{1}v_{3} ∉ L_{x,y}, a contradiction. Case 2: |v_{1}| = |w_{1}|. In this case v_{1} = w_{1} so y = y′ since the entries in a row of L are anti-prefix disjoint. Then w_{2} ∈ M_{y,z} and w_{2}v = v_{2} ∈ M_{y,z} imply that v = ϵ. Case 3: |v_{1}| > |w_{1}|. In this case v_{1} = w_{1}v_{3} for some v_{3} and a contradiction similar to Case 1 ensues. We conclude that v = ϵ.

Next we show that the entries in a row of K are pairwise anti-prefix disjoint. Let w ∈ K_{x,z} so there are y ∈ Y, w_{1} ∈ L_{x,y}, w_{2} ∈ M_{y,z} such that w = w_{1}w_{2}. Let v ∈ Σ^{∗}. We must show that wv ∉ K_{x,z′} for z′ ≠ z. Again we have 3 cases: Case 1: |v_{1}| < |w_{1}|. In this case w_{1} = v_{1}v_{3} for some v_{3} with |v_{3}| > 0. As above this contradicts the properties of L. Case 2: |v_{1}| = |w_{1}|. In this case v_{1} = w_{1} so y = y′ since the row entries of L are anti-prefix disjoint. Then w_{2} ∈ M_{y,z} implies w_{2}v = v_{2} ∉ M_{y,z′} since the row entries of M are anti-prefix-disjoint. Case 3: |v_{1}| > |w_{1}|. Again this is similar to Case 1. We conclude that wv ∉ K_{x,z′}.

The preceding Proposition allows the definition of a suitable receiving category for the behaviours of Σ-automata. The category B_{F} has objects sets, arrows from X to Y given by X × Y matrices of anti-prefix languages over Σ with entries in each row pairwise anti-prefix-disjoint. Composition is defined using the matrix multiplication of the preceding proposition. We define the matrix of the composite of L : X ⟶ Y and M : Y ⟶ Z to be the matrix K = LM, with the product taken in the diagrammatic order. Thus the composite is an arrow of B_{F} by Proposition 32.

Lemma 33 If there is a 2-cell ϕ : (U, α) ⟶ (U′, α′) in F then E(U, α) = E(U′, α′).

Viewing B_{F} as a bicategory with discrete hom categories we get:

Proposition 34 Behaviour, E, extends to homomorphism of bicategories from F to B_{F}.

Proof. First, E is locally functorial by the remarks after Definition 30 and Lemma 33. The behaviour of a serial composite of Σ-automata is the composite in B_{F} of their behaviours. To see this note that the concatenation of a Σ^{∗} word from the first behaviour with one from the second simply describes a path through the composite automaton.

Definition 35 Let (U, α) : X ⟶ Y be a Σ-automaton. The object of reachable states of (U, α) is

U_{R} = {u ∈ U | ∃x ∈ X ∃w ∈ Σ^{∗} α^{∗}(x, w) = u}.

The reachable kernel of (U, α) is the automaton R(U, α) = (U_{R}, α_{R}) : X ⟶ Y where α_{R} : X + U_{R} ⟶ U_{R} + Y is the restriction of α.

We again observe that R : F(X, Y) ⟶ F(X, Y) is functorial, idempotent and that there is a 2-cell ρ_{(U,α)} : R(U, α) ⟶ (U, α) which is the component of a natural transformation from R to 1_{F(X,Y)}. Moreover, Rρ = ρR. We have the following analogues of results for Elgot automata:

Proposition 36 1) The functor R is an idempotent comonad on F(X, Y) with counit ρ.

2) The behaviour of the reachable kernel, R(U, α), of a Σ-automaton, (U, α) is the same as that of (U, α).

3) If (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z, then there is a canonical 2-cell r_{UV} : R((U, α)(V, β)) ⟶ R(U, α)R(V, β).

The coalgebras for the local reachability comonads are the reachable Σ-automata.

The minimization theory we obtain in the case of Σ- automata is also similar to that of the preceding section. We begin with an equivalence relation on states of (U, α): u ∼_{α} u′ iff for all w ∈ Σ^{∗} and for all y ∈ Y we have α_{U}^{+}(u, w) = y iff α_{U}^{+}(u′, w) = y.

Again, we can construct a ‘quotient’ automaton denoted M(U, α) = (U_{M}, α_{M}). We define U_{M} = U/ ∼_{α} and α_{M} is defined on X + U_{M} by

α_{M}(x) = \{ \begin{matrix}[u] & if α(x) = u \\ y & if α(x) = y ∈ Y \end{matrix} and fora ∈ Σ α_{M}([u], a) = \{ \begin{matrix}[u′] & if α(u, a) = u′ ∈ U \\ y & if α(u, a) = y ∈ Y. \end{matrix}

Proposition 37 1) The quotient function η : U ⟶ U_{M} underlies a 2-cell in F denoted η_{(U,α)} : (U, α) ⟶ M(U, α). Applying M to it gives an isomorphism, and (M, η) is an idempotent monad on F(X, Y).

2) The behaviour of M(U, α) is the same as that of (U, α).

3) If (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z in F, then there is a canonical function m_{UV} : M(U, α)M(V, β) ⟶ M((U, α)(V, β)).

The algebras for M have a unique state associated with each path to an element of Y which actually occurs in the behaviour of (U, α).

Our next objective is a minimal realization of any behaviour in B_{F}. Let L = (L_{x,y}) be a behaviour from X to Y. For x, x′ ∈ X and w, w′ ∈ Σ^{∗}, we write (x, w) ∼_{L} (x′, w′) if and only if for all v ∈ Σ^{∗}, for all y ∈ Y wv ∈ L_{x,y} ⟺ w′v ∈ L_{x′,y′}. The state set for the minimal realization automaton is U_{L} = (X × Σ^{∗})/ ∼_{L} . The action for the minimal realization is defined on X + U_{L} by:

α_{L}(x) = \{ \begin{matrix}y & if L_{x,y} = \{ϵ\} \\ [(x, ϵ)] & otherwise \end{matrix} and α_{L}([(x, w)], a) = \{ \begin{matrix}y & if wa ∈ L_{x,y} \\ [(x, wa)] & otherwise. \end{matrix}

With the observation that α_{L} is well-defined, we have α_{L} : X + (U_{L} × Σ) ⟶ U_{L} + Y, and we note that the automaton NL = (U_{L}, α_{L}) is reachable.

Proposition 38 The behaviour of NL is L. Furthermore, we have E is left adjoint to N : B_{F}(X, Y) ⟶ F_{R}(X, Y).

Proof. The situation is similar to that for Elgot automata: the constructed automaton has states which correspond to equivalent deterministic transitions to an output state, plus possibly a loop state. Thus the first statement follows immediately.

For the adjunction, we show that 2-cells (in B_{F}(X, Y)) from E(U, α) to L correspond to 2-cells (in F_{R}(X, Y)) from (U, α) to NL. Since B_{F} is locally discrete, that is to show that E(U, α) = L if and only if there is a unique 2-cell from (U, α) to NL.

First observe that if there is (U, α) ⟶ NL, then E(U, α) = ENL = L, by Lemma 33 and the first paragraph.

For necessity, we suppose E(U, α) = L and seek to define a unique 2-cell ϕ : (U, α) ⟶ NL. Recalling that (U, α) is reachable we define ϕ : U ⟶ U_{L} by:

ϕ(u) = [(x, w)] if α^{∗}(x, w) = u

We need to show that ϕ is well-defined, that it defines a 2-cell in F_{R}, and that it is the only such 2-cell. The first two follow immediately from E(U, α) = L. For the last simply observe that [(x, w)] satisfies α_{L}^{∗}(x, w) = [(x, w)], so ϕ(α^{∗}(x, w)) = α_{L}^{∗}(x, w) = [(x, w)] and the requirement that ϕ be a morphism determines the definition of ϕ(u).

5 Lax Monads

We first recall some definitions for bicategory morphisms and lax monads. In particular, we consider morphisms of bicategories which are identity on objects and which have the structure of a monad on each hom category, and then we give conditions sufficient to guarantee that the hom-category monads define a monoid in a suitable category of bicategory morphisms.

To establish notation, we recall that a morphism of bicategories from B to C is a pair (F, ϕ) in which: F maps objects and 1-cells of B to objects and 1-cells of C; for every object B of B, there is a 2-cell ϕ_{B} : 1_{F B} ⟶ F (1_{B}); and whenever f : B ⟶ B′ and g : B′ ⟶ B′′ are composable, there is a 2-cell ϕ_{gf} : F gF f ⟶ F gf : B ⟶ B′′. The data are subject to equations found in [Ben]. We denote the action of F on a hom category by F (B, B′) : B(B, B′) ⟶ C(F B, F B′). We will also need to consider oplax transformations between morphisms. An oplax transformation σ : (F, ϕ) ⟶ (G, γ) is given by arrows σ_{B} : F B ⟶ GB for all objects B in B, and 2-cells σ_{f} : σ_{B′}F f ⟶ Gfσ_{B}, whenever f : B ⟶ B′ is in B, subject to equations again in [Ben]. Our interest, as noted above, will be in rather special morphisms and transformations. They arise in examples and ensure that we obtain a monoidal category in which to define lax monads.

Proposition 39 [CR](Prop. 2.1) For any class X the following data determine a bicategory which we denote M(X):

1. Objects are bicategories with class of objects X.

2. One-cells are morphisms of bicategories which are identity on objects.

3. Two-cells are oplax transformations whose object components are all identities.

Definition 40 [CR] A lax monad on B with objects B_{o} is a monoid in M(B_{o})(B, B).

We can give explicit criteria of a more elementary sort providing a characterization of morphisms that are lax monads.

Proposition 41 [CR](Prop. 2.3) An endomorphism (T, τ) of B in M(B_{o}) together with, for every pair B, B′ in B, natural transformations

η_{BB′} : 1_{B}(B, B′) ⟶ T (B, B′) ⟵ T^{2}(B, B′) : μ_{BB′}

extends to a lax monad if

1. each (T (B, B′), η_{BB′}, μ_{BB′}) is a monad on B(B, B′);

2. for all B,

τ_{B} = η_{1_{B}};

3. if f : B ⟶ B′ and g : B′ ⟶ B′′ are 1-cells in B then

τ_{gf}(η_{g} ∘ η_{f}) = η_{gf} : gf ⟶ T gf

and

μ_{gf}T τ_{gf}τ_{T gT f} = τ_{gf}(μ_{g} ∘ μ_{f}) : T^{2}gT^{2}f ⟶ T gf

Conversely, a lax monad determines transformations η_{BB′} and μ_{BB′} satisfying 1, 2 and 3.

In fact the lax monads and colax comonads considered below are (locally) idempotent, i.e. for any arrow f : B ⟶ B′ in B we have T η_{f} = η_{T f} and the common value is inverted by μ_{f}, so that (locally) T^{2} ≅ T. In this case we have a simplification:

Proposition 42 If ((T, τ), η, μ) is idempotent, then the equation involving μ in 3. of the preceding proposition follows from the other data.

Proof. To show that μ_{gf}T τ_{gf}τ_{T gT f} = τ_{gf}(μ_{g} ∘ μ_{f}) we show that (μ_{gf})^{−1}τ_{gf} = T τ_{gf}τ_{T gT f}(μ_{g} ∘ μ_{f})^{−1}. Now (μ_{gf})^{−1} = η_{T gf} and (μ_{g} ∘ μ_{f})^{−1} = μ_{g}^{−1} ∘ μ_{f}^{−1} = η_{T g} ∘ η_{T f}. Note that the following diagram commutes by naturality of η, and the equation above involving η.

[figure: T^{2}gT^{2}f; τ_{T gT f}; η_{T g} ∘ η_{T f}; η_{T gT f}; T (T gT f); T^{2}gf; T τ_{gf}; T gT f; T gf; τ_{gf}; η_{T gf}]

Thus (μ_{gf})^{−1}τ_{gf} = η_{T gf}τ_{gf} = T (τ_{gf})η_{T gT f} = τ_{T gT f}(η_{T g} ∘ η_{T f}) = T τ_{gf}τ_{T gT f}(μ_{g} ∘ μ_{f})^{−1}.

In view of condition 1. of Proposition 41, there is a local category of (Eilenberg-Moore) algebras for each pair of objects. The main result of [CR] constructs a bicategory with these algebras as hom categories assuming local exactness conditions on the underlying morphism (T, τ). This construction of algebras simplifies in case the monad is idempotent. In fact, no exactness is required of the local monads in this case.

Proposition 43 Let ((T, τ), η, μ) be an idempotent lax monad on a bicategory, B. The following data determine a bicategory denoted B^{T}:

1. objects are those of B;

2. for objects B and B′ of B, the hom category is B^{T} (B, B′);

3. composition of 1-cells f : B ⟶ B′, g : B′ ⟶ B′′ is defined by T (gf)

4. horizontal composition of 2-cells is also defined by application of T

Proof. In [CR] it is shown that the underlying arrow of the composite of (f, ϕ) in B^{T} (B, B′) with (g, γ) in B^{T} (B′, B′′) is the joint coequalizer of two parallel pairs of 2-cells, one of which is T (g ∘ϕ) : T (gT f) ⟶ T (gf) and μ_{gf}T τ_{gf}T (η_{g} ∘T f) : T (gT f) ⟶ T (gf) (and the other pair just interchanges the roles of ϕ and γ.) We claim that these 2-cells are equal. Now assuming that the monad is idempotent means that μ_{gf} = (T η_{gf})^{−1} and since algebras for T (B, B′) are the objects (of T (B, B′)) for which the unit is invertible, we have ϕ = η_{f}^{−1}. Thus our claim holds if T η_{gf}T (g ∘ η_{f}^{−1}) = T τ_{gf}T (η_{g} ∘ T f), so if η_{gf}g ∘ η_{f}^{−1} = τ_{gf}η_{g} ∘ T f. But from the first of equations 3. in Proposition 41, η_{gf} = τ_{gf}(η_{g}∘η_{f}) so η_{gf}g∘η_{f}^{−1} = τ_{gf}(η_{g}∘η_{f})g∘η_{f}^{−1} = τ_{gf}η_{g}∘T f as required. The other pair of 2-cells is similarly equal so the required joint coequalizer is just T (gf), which is then the composite of (f, ϕ) and (g, γ) as claimed. The horizontal composite is similar.

In the next section we will need to consider a dual of the concepts described above, namely colax comonads. A comorphism of bicategories is (G, γ) : B ⟶ C where G maps objects and 1-cells of B to objects and 1-cells of C. For every object B of B there is a 2-cell γ_{B} : G(1_{B}) ⟶ 1_{GB}; and whenever f : B ⟶ B′ and g : B′ ⟶ B′′ are composable, there is a 2-cell γ_{gf} : Ggf ⟶ GgGf : B ⟶ B′′, subject to appropriate equations. An opcolax transformation σ : (G, γ) ⟶ (H, ν) between comorphisms is given by arrows σ_{B} : GB ⟶ HB for all objects B in B, and 2-cells σ_{f} : Hfσ_{B} ⟶ σ_{B′}Gf,whenever f : B ⟶ B′ is in B, again subject to equations. As above we obtain a bicategory C(X) of identity on objects comorphisms and define a colax comonad on B to be a comonoid in C(B_{′})(B, B). We will not state the obvious duals of propositions in this section, but we will use them without further comment in the next section.

6 Applications to Automata

In Sections 2, 3 and 4 we have identified various local (co-)monads for reachability and minimization. Our purpose in this section is to apply the results in the preceding section to demonstrate that these local (co-)monads extend to lax (co-)monads defined on the bicategories of automata concerned. That is, they are compatible with serial composition up to a comparison morphism. We show further that the Nerode adjunctions described above also extend to the (bi-)categories in question.

We begin with Mealy automata, considering reachability first and then minimization.

The notation is from Section 2. In the case of reachability we deal with identity on objects endocomorphisms.

Proposition 44 The comonads R(X, Y) defined on A extend to an idempotent colax comonad R : A ⟶ A, and the algebras for R(X, Y) are the one-cells of a bicategory, denoted A_{R} of reachable automata.

Proof. We first need to show that the local functors R(X, Y) have the structure of a comorphism (R, r) on M. Recall that the identity Mealy automaton 1_{X} on X is (essentially the identity arrow) (1, t, 1_{1}) : X ⟶ X where t : X × 1 ⟶ 1 × X. Since RX = X and since we easily see R(1_{X}) = 1_{X}, we simply take r_{X} : R(1_{X}) ⟶ 1_{RX} to be the identity. Let (U, α, u_{0}) : X ⟶ Y and (V, β, v_{0}) : Y ⟶ Z. The comparison 2-cell for their composite is r_{UV} from Proposition 11.

Since the R(X, Y) are idempotent comonads, by Proposition 42 we have to check only equations 2. and the first of equations 3. in Proposition 41 to see that the R(X, Y) extend. Both r_{X} and ρ_{1_{X}} are identities so equations 2. are satisfied. For the first of equations 3. we note that

(ρ_{V} ∘ ρ_{U})r_{UV} : (U × V)_{R} ⟶ U_{R} × V_{R} ⟶ U × V

is simply the inclusion ρ_{UV} : (U × V)_{R} ⟶ U × V.

The colax structure provides a comparison between the reachable kernel of a serial composite (in A) and the serial composite of reachable kernels. Serial composition of reachable automata is just composition of 1-cells in the bicategory of coalgebras. The explicit description of composition in A_{R} is simply that the composite of reachable automata in A_{R} is the reachable kernel of their composite in A. Comments of the same sort apply to the colax comonads for reachability and lax monads for minimization described below.

The next result follows immediately from Theorem 3.6 of [CR], and the preceding Proposition.

Corollary 45 The idempotent colax comonad (R, ρ) : A ⟶ A factors as

A ⟶^{G} A_{R} ⟶^{J} A

where G is a bicategory homomorphism. For all X, Y we have J(X, Y) ⊣ G(X, Y), and so A_{R}(X, Y) is a coreflective subcategory of A(X, Y) with coreflector G

We now turn to the similar results for minimization of Mealy automata.

Proposition 46 The monads M(X, Y) : A(X, Y) ⟶ A(X, Y) extend to a lax monad on A. Algebras for M(X, Y) are the one-cells of a bicategory, denoted A^{M} of minimized automata.

Proof. Again we first show that the local functors M(X, Y) have the structure of a morphism (M, m) on M. The identity Mealy automaton 1_{X} on X is (essentially the identity arrow) (1, t, 1_{1}) : X ⟶ X where t : X × 1 ⟶ 1 × X. Thus M(1_{X}) = 1_{X} and since MX = X we take m_{X} : 1_{MX} ⟶ M(1_{X}) to be the identity. The comparison 2-cell for a composite (V, β, v_{0})(U, α, u_{0}) : X ⟶ Z is m_{UV} from Proposition 14.

Since the M(X, Y) are idempotent monads, by Proposition 42 we have to check only equations 2. and the first of equations 3. in Proposition 41 to see that the M(X, Y) extend. Both m_{X} and μ_{1_{X}} are identities so equations 2. are satisfied. For the first of equations 3. we note that m_{UV} (μ_{V} ∘ μ_{U}) is simply the quotient μ_{UV} : U × V ⟶ (U × V)_{M}.

Composition in A^{M} is easy to describe: the composite of minimized automata in A^{M} is the minimization of their composite in A.

Corollary 47 The idempotent lax monad (M, η) : A ⟶ A factors as

A ⟶^{F} A^{M} ⟶^{I} A

where F is a bicategory homomorphism, for all X, Y we have F (X, Y) ⊣ I(X, Y), and so A^{M}(X, Y) is a reflective subcategory of A(X, Y) with reflector F

The situation we have been describing is summed up in the following proposition. The pairs of functors are locally adjoint and provide examples of the various notions of local adjunction in the literature.

Proposition 48 In the following diagram both the inner and outer squares commute. The I’s (resp. J’s) are locally reflective (resp. coflective) inclusions.

[figure: A^{M}; (A_{R})^{M′}; A; A_{R}; G; F; F′; (A^{M})_{R′}; J′; G′; ≅; I; J; I′]

Theorem 49 The Nerode automaton construction extends to a morphism of bicategories, N : B_{A} ⟶ A_{R}, and E and N determine a local adjunction. Moreover, N factors as N = I′N′, E factors as E = E′F′, and N′ and E′ determine an equivalence B_{A} ≅ (A_{R})^{M′} as indicated in the diagram.

[figure: A_{R}; B_{A}; N; E; A_{R}; (A_{R})^{M′}; I′; F′; (A_{R})^{M′}; E′; N′; ≃]

Proof. Suppose that f : X ⟶ Y and g : Y ⟶ Z are composable behaviours. We need a 2-cell ν_{gf} : NgNf ⟶ Ngf in A_{R}. Note that the composite NgNf is in A_{R}, so is that described in Corollary 44. Recall that the composite in A of Nf and Ng has internal states X^{∗}/ ∼_{f} ×Y^{∗}/ ∼_{g}, i.e. pairs ([w]_{f}, [v]_{g}) where w ∈ X^{∗}, v ∈ Y^{∗}. An easy calculation shows that the reachable states are pairs of the form ([w]_{f}, [f(w)]_{g}). After this observation, it is easy to see that defining ν([w]_{f}, [f(w)]_{g}) = ν([w]_{gf}) provides the required structure.

We also need ν_{X} : 1_{X} ⟶ N1_{X}, but this 2-cell can be taken to be an identity since N1_{X} has only one internal state (the equivalence relation ∼_{1_{X}} is the all relation.)

In the diagram above, we can define E′ to be EI′ and N′ to be F′N. To establish the theorem, we verify that these provide factorizations of E and N as E ≅ E′F′ and N ≅ I′N′, and then show that both composites of E′ and N′ are isomorphic the identity.

First, E′F′ = EI′F′ by definition. Since F′ is minimization, applying it does not affect behaviour, so we have EI′F′ = E, and the first iso is established. Next, I′N′ = I′F′N by definition. Now Nf is a minimized automaton, so application of I′F′ is essentially the identity and the second iso follows.

For the equivalence, note that E′N′ = EI′F′N by definition, and as just observed, I′F′N ≅ N, so E′N′ ≅ EN, but ENf = f by the previous Theorem. Finally, N′E′ = F′NEI′ by definition. Now a reachable, minimal Mealy automaton I′A is isomorphic to the Nerode automaton of its behaviour, i.e. NEI′A ≅ I′A. (The unit of the adjunction in the previous Theorem provides the comparison which is epic by reachability and monic by minimality.) Thus N′E′A = F′NEI′A ≅ F′I′A ≅ A.

Using notation from Section 4, we consider the situation for Σ-automata. Recall that we can view the Elgot automata of Section 3 as a special case.

Proposition 50 The monads R(X, Y) defined on F extend to an idempotent colax comonad R : F ⟶ F, and the algebras for R(X, Y) are the one-cells of a bicategory, denoted F_{R} of reachable Σ-automata.

Proof. Recall first from Proposition 36 that if (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z, there is a comparison 2-cell r_{UV} : R((U, α)(V, β)) ⟶ R(U, α)R(V, β). The equations for a colax comonad are trivial in this situation so the result follows from Proposition 43.

The composite of reachable automata in F_{R} is the reachable coreflection of their composite in F.

Corollary 51 The idempotent colax comonad (R, ρ) : F ⟶ F factors as

F ⟶^{G} F_{R} ⟶^{J} F

where G is a bicategory homomorphism. For all X, Y we have J(X, Y) ⊣ G(X, Y), and so F_{R}(X, Y) is a coreflective subcategory of F(X, Y) with coreflector G.

Once again, the minimal realization-behaviour adjunction is essentially the minimization local adjunction. We begin with minimization.

Proposition 52 The monads M(X, Y) : F(X, Y) ⟶ F(X, Y) extend to a lax monad on F. Algebras for M(X, Y) are the one-cells of a bicategory, denoted F^{M} of minimized Σ-automata.

Proof. Recall first from Proposition 37 that if (U, α) : X ⟶ Y and (V, β) : Y ⟶ Z, there is a comparison 2-cell m_{UV} : M(U, α)M(V, β) ⟶ M((U, α)(V, β)). The equations for a lax monad also follow easily, so the result follows from Proposition 43.

The composite of minimized Σ-automata in F^{M} is the minimization of their composite in F.

Corollary 53 The idempotent lax monad (M, η) : F ⟶ F factors as

F ⟶^{F} F^{M} ⟶^{I} F

where F is a bicategory homomorphism. For all X, Y we have F (X, Y) ⊣ I(X, Y), and so F^{M}(X, Y) is a reflective subcategory of F(X, Y) with reflector F

As with Mealy automata, it is easy to see that reachable kernel and minimization commute. Thus we obtain lax monads for reachability (resp. minimization) on F^{M} (resp. F_{R}) whose local algebras coincide, i. e. (F^{M})_{R′} ≅ (F_{R})^{M′}, where the primed monads act as R (resp. M) did on F. We sum up with the following proposition.

Proposition 54 In the following diagram both the inner and outer squares commute. The I’s (resp. J’s) are locally reflective (resp. coflective) inclusions.

[figure: F^{M}; (F_{R})^{M′}; F; F_{R}; G; F; F′; (F^{M})_{R′}; J′; G′; ≅; I; J; I′]

Finally, the minimized reachable Σ-automata have the same relation to their behaviours as Mealy automata.

Theorem 55 The minimal realization construction on B_{F} extends to a morphism of bicategories, N : B_{F} ⟶ F_{R}, and E and N determine a local adjunction. Moreover, N factors as N = I′N′, E factors as E = E′F′, and N′ and E′ determine an equivalence B_{F} ≅ (F_{R})^{M′} as indicated in the diagram.

[figure: F_{R}; B_{F}; N; E; F_{R}; (F_{R})^{M′}; I′; F′; (F_{R})^{M′}; E′; N′; ≃]

Proof. The proof is very similar to the proof in the case of Mealy automata once we make the observation that N is actually a lax functor in this situation also.

References

[AT] J. Adamek and V. Trnkova. Automata and Algebras in Categories.

Kluwer, 1990.

[Ben] J. Bénabou. Introduction to bicategories. Lecture Notes in Math., no. 47, 1–77, 1967.

[BP] R. Betti and J. Power. On local adjunctions of distributive bicategories. Bolletino della Unione Matematica Italiana, (7) 2-B:931– 947, 1988.

[BSS] L. Blum, M. Shub, and S. Smale. On a theory of computation and complexity over the real numbers: NP completeness, recursive functions and universal machines. Bulletin of the American Mathematical Society, 21:1–46, 1989.

[BSW] S. Bloom, N. Sabadini, and R. F. C. Walters. Matrices, machines and behaviors. Preprint, 1994.

[CR] Aurelio Carboni and Robert Rosebrugh. Lax monads. Journal of Pure and Applied Algebra, 76:13–32, 1991.

[Gin] S. Ginsburg. The Mathematical Theory of Context-Free Languages. McGraw-Hill, 1966.

[Gog] J. A. Goguen. Minimal realization of machines in closed categories. Bulletin of the AMS, 78:777–783, 1972.

[HU] J. Hopcroft and J. D. Ullman. Introduction to automata theory, languages and computation. Addison-Wesley, 1979.

[Jay] Barry Jay. Local adjunctions. Journal of Pure and Applied Algebra, 53:227–238, 1988.

[KSW] P. Katis, N. Sabadini, and R.F.C. Walters. Bicategories of processes. Journal of Pure and Applied Algebra, to appear.

[Ner] A. Nerode. Linear automaton transformations. Proc. Amer. Math. Soc., 9:541–544, 1958.

[SWV] N. Sabadini, R.F.C. Walters, and S. Vigna. A note on recursive functions. Mathematical structures in computer science, 6:127– 139, 1996.

[SWW] N. Sabadini, H. Weld, and R.F.C. Walters. On categories of asynchronous circuits. School of mathematics and statistics research reports, University of Sydney, (93-34), 1994.

[Vig] S. Vigna. On relations between distributed computability and the BSS model. Theoretical computer science, 162:5–21, 1996.