3.1.1 Mealy Machine

Let \(\Sigma\) and \(\Gamma\) be two alphabets. A Mealy Machine \(\mathcal{M}\) is a tuple \((q_0, Q, \delta, \lambda)\) such that

1. \(Q\) is a finite set of states.
2. \(q_0 \in Q\) is the initial state.
3. \(\delta \colon Q \times \Sigma \to Q\) is a transition function.
4. \(\lambda \colon Q \times \Sigma \to \Gamma\) is an output function.

The semantics of a Mealy Machine is given by the following inductive equations: \[ \mathcal{M}(w) :=\mathcal{M}(q_0, w) \quad \mathcal{M}(q,\varepsilon) :=\varepsilon \quad \mathcal{M}(q,au) :=\lambda(q,a) \mathrel{\cdot}\mathcal{M}(\delta(q,a), u) \]

3.1.2 Flip-Flop Machine

A flip-flop machine is a Mealy Machine such that for all letters \(a \in \Sigma\), either \(\delta(\cdot,a)\) is the identity function, or it is a constant function. It is a binary flip-flop machine when \(Q = \{ 0,1 \}\).

3.1.3 Mealy Machine With Lookahead

Let \(\Sigma\) and \(\Gamma\) be two alphabets. A Mealy Machine with Lookahead \(\mathcal{M}\) is a tuple \((q_0, Q, \delta, \lambda)\) such that

1. \(Q\) is a finite set of states.
2. \(q_0 \in Q\) is the initial state.
3. \(\delta \subseteq Q \times \Sigma \times Q\) is a transition relation.
4. \(\lambda \colon Q \times \Sigma \times Q \to \Gamma\) is an output function.

In addition to this syntactic definition, we furthermore assume that for each \(w \in \Sigma^*\), there exists at most one path in the automaton \((q_0, Q, \delta)\) starting from \(q_0\) and reading \(w\).

The semantics of the Mealy Machine is given by considering potential runs of the machine. Because of the absence of ambiguity, it defines a partial map \(\mathcal{M} \colon \Sigma^* \rightharpoonup\Gamma^*\).

3.1.4 Sequential Functions

Let \(\Sigma\) and \(\Gamma\) be two alphabets. A sequential transducer \(A\) is a tuple \((q_0, Q, \delta, \lambda)\) such that

1. \(Q\) is a finite set of states.
2. \(q_0 \in Q\) is the initial state.
3. \(\delta \colon Q \times \Sigma \rightharpoonup Q\) is a partial transition function.
4. \(\lambda \colon Q \times \Sigma \to \Gamma^*\) is an output function.

The semantics is defined as for Mealy Machines.

Warning: this is sometimes called pure sequential functions.

3.2.1 Presburger Arithmetic

Formulas of the Presburger Arithmetic are built from the following grammar: \[ \begin{aligned} \varphi &:=\top \mid \bot \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \lnot \varphi \mid \exists x. \varphi \mid x = y + z \end{aligned} \]

Given a valuation \(\nu \colon \vec{x} \to \mathbb{N}\), we define the semantics of \(\varphi\) inductively as follows:

\[ \begin{aligned} \nu \models \top &\iff \text{true} \\ \nu \models \bot &\iff \text{false} \\ \nu \models \varphi \land \psi &\iff \nu \models \varphi \text{ and } \nu \models \psi \\ \nu \models \varphi \lor \psi &\iff \nu \models \varphi \text{ or } \nu \models \psi \\ \nu \models \lnot \varphi &\iff \text{ not } (\nu \models \varphi) \\ \nu \models \exists x. \varphi &\iff \text{ there exists } n \in \mathbb{N}\text{ s.t. } \nu[x \mapsto n] \models \varphi \\ \nu \models x = y + z &\iff \nu(x) = \nu(y) + \nu(z) \end{aligned} \]

3.2.2 Topology and Continuous functions

Let \(X\) be a set. A topology over \(X\) is a subset \(\tau\) of \(\mathop{\mathcal{P}}(X)\) closed under finite intersections and arbitrary unions. In a topological space \((X, \tau)\), the subsets in \(\tau\) are called open subsets, and their complement are called closed subsets.

A function \(f \colon (X, \tau) \to (Y,\theta)\) is continuous whenever for all open subset \(U \in \theta\), its pre-image \({f}^{-1}\left(U\right)\) is an open subset of \(\tau\). Equivalently, it is continuous if the pre-image of closed subsets are closed subsets.

3.2.3 Lipschitz functions

A function \(f \colon (X,d_X) \to (Y, d_Y)\) is Lipschitz if there exists a constant \(K \geq 0\) such that for all \(x_1,x_2 \in X^2\), \(d_Y(f(x_1), f(x_2)) \leq K d_X(x_1, x_2)\).

3.2.4 Prefix Distance

Let \(\Sigma^*\) be a finite alphabet. The prefix distance between two words \(u,v\) is \(\left| u \right|_{} + \left| v \right|_{} - 2 \left| w \right|_{}\) where \(w\) is the longest common prefix of \(u\) and \(v\).

3.2.5 Regular Topology

Let \(\Sigma\) be a finite alphabet. We equip \(\Sigma^*\) with a metric distance as follows: to a pair of words \(u,w\), we associate the minimal size \(s(u,w)\) of a deterministic automaton that separates \(u\) from \(w\). The distance between two words \(u\) and \(w\), is defined as \(d(u,w) :=2^{-s(u,w)}\). The regular topology is the topology defined by this metric on \(\Sigma^*\).

Equivalently, the regular topology is the coarsest topology containing the regular languages as closed subsets.