ora-0082

5.4 Automata and machine inference as coalgebra learning

The longstanding program of inferring finite-state machines, sequential machines, and computable devices from examples or experiments is an especially literal instance of UOCL. Fix an input alphabet \(A\) and an output object \(O\). A deterministic Moore machine is a coalgebra

\begin{equation} c:X\longrightarrow O\times X^{A} \end{equation}
5.4

for the endofunctor \(F(X)=O\times X^A\). When \(O=2\), this is a deterministic language acceptor: the first component records acceptance and the second gives the successor reached by each input symbol. A finite-state learning problem therefore asks for a finite carrier \(X\), an \(F\)-coalgebra structure on it, and a designated initial state that reproduce the observed behavior.

Fixed doctrine.

The alphabet, output type, endofunctor, deterministic transition law, and usually finiteness of the carrier are supplied before inference. Final semantics determines behavioral equivalence; minimization or an observation table supplies the internal solution construction. Angluin-style membership and equivalence queries are not generic interaction but a particularly strong presentation protocol. Together these commitments explain both the precision of automata-learning theorems and the narrowness of their target.

This formulation exposes the universal object that the learner can actually identify. When a final coalgebra \((\nu F,\zeta )\) exists, every candidate has a unique behavior map

\begin{equation} \mathsf{beh}_c:X\longrightarrow \nu F, \qquad \zeta \circ \mathsf{beh}_c=F(\mathsf{beh}_c)\circ c. \end{equation}
5.5

For deterministic acceptors, \(\mathsf{beh}_c(x)\) is the language accepted from state \(x\); for Moore machines, it is the complete input-indexed output behavior. Classical automata inference consequently learns the image of reachable states in final semantics, usually represented by the minimal automaton, rather than the accidental names or redundant realization of hidden states. Angluin’s \(L^*\) algorithm makes the presentation protocol unusually explicit: membership queries reveal local behavior, while equivalence queries return counterexamples that separate an incorrect conjecture [ Angluin , 1987 ] .