Simulating Finite Eilenberg Machines with a Reactive Engine

AbstractEilenberg machines have been introduced in 1974 in the field of formal language theory. They are finite automata for which the alphabet is interpreted by mathematical relations over an abstract set. They generalize many finite state machines. We consider in the present work the subclass of finite Eilenberg machines for which we provide an executable complete simulator. This program is specified using the Coq proof assistant. The correctness of the algorithm is also proved formally and mechanically verified using Coq. Using its extraction mechanism, the Coq proof assistant allows to translate the specification into an executable OCaml program. The algorithm and specification are inspired from the reactive engine of Gérard Huet. The finite Eilenberg machines model includes deterministic and non-deterministic automata (DFA and NFA) but also real-time transducers. As an example, we present a pushdown automaton (PDA) recognizing ambiguous λ-terms is shown to be a finite Eilenberg machine. Then the reactive engine simulating the pushdown automaton provides a complete recognizer for this particular context-free language