3.1 Bounded Output

Give an algorithm that decides if a polyregular function has finitely many distinct outputs.

3.2 Forward Loops Cannot Go Backwards

Let us call \(\mathsf{ForwardPoly}\) the class of functions computed by for-programs that only have forward loops. Prove that the reverse function is not in \(\mathsf{ForwardPoly}\).

3.3 Nesting Birds

Give an algorithm that inputs a polyregular function \(f\), and decides whether \(f\) can be realised by a for-program that does not nest for loops.

3.4 One Size Fits All

Prove that the following two subclasses of rational functions are equivalent and provide effective conversions:

1. unambiguous NFA with output where every transition is labelled by exactly one output letter.
2. unambiguous NFA with output where for every input word, the output has the same length as the input.

3.5 Be There Or Be Very Weak Square

A semi-blind \(k\)-pebble transducer is obtained by modifying the original model so that when placing a new pebble, the machines does not start from the leftmost position of the input (and stays where it is currently), but such that the pebbles cannot be seen by submachines. Prove that semi-blind \(k\)-pebble transducers cannot compute the squaring function.

3.6 Windowed Transducers

A Mealy machine is called windowed if there exists a constant \(K \in \mathbb{N}\) such that the output of the machine on a given input letter only depends on the letters at distance at most \(K\) from the input letter.

1. Provide an example of a Mealy Machine that is not windowed.
2. Is it decidable whether a Mealy Machine is windowed?

The definition of windowed generalizes naturally to unambiguous NFAs with output where every transition is labelled by a single output letter, called unambiguous NFAs with letter-to-letter output.

3. Is it decidable whether an unambiguous NFA with letter-to-letter output is windowed?

3.7 Minimising growth

Recall that in \(\mathsf{MSO}\)-transductions, we introduced a duplication function \(d_{\alpha, \beta}\) that maps \(w\) to \(\diamond^\beta \prod_{i = 1}^{|w|} w_i (\#)^{\alpha - 1}\). Any regular function is written as the composition of an \(\mathsf{MSO}\)-interpretation (without copies) with a duplication. As a consequence, \(|f(w)| \leq \alpha |w| + \beta\) for some \(\alpha, \beta \in \mathbb{N}\).

Question: assume that there exists \(\alpha', \beta' \in \mathbb{N}\) such that \(|f(w)| \leq \alpha' |w| + \beta'\) for all \(w\). Is it possible to represent \(f\) using \(d_{\alpha',\beta'}\) followed by an \(\mathsf{MSO}\)-interpretation.

3.8 Deatomisation of Bimachines

Let \(\mathbb{A}\) be an infinite set, and \(\mathcal{S}\) be the set of permutations of \(\mathbb{A}\). We define atomic bimachines with input alphabet \((\Sigma \cup \mathbb{A})\) and output alphabet \((\Gamma \cup \mathbb{A})\) via the existence of a finite monoid \(M\) and a morphism \(\mu \colon (\Sigma \cup \mathbb{A})^* \to M\) such that \(\mu(a) = 1_M\) for all \(a \in \mathbb{A}\), together with a production function \(\pi \colon M \times (\Sigma \cup \mathbb{A}) \times M \to (\Gamma \cup \mathbb{A})^*\), satisfying the following equivariance property (where \(\sigma \in \mathcal{S}\) is lifted from permutations over \(\mathbb{A}\) to an action over \((\Gamma \cup \mathbb{A})^*\) and \((\Sigma \cup \mathbb{A})^*\) in the natural way):

\[ \forall a \in \mathbb{A}, \forall \sigma \in \mathcal{S}, \pi (m, \sigma(a), n) = \sigma(\pi(m,a,n)) \quad . \]

An atom coding function is a function \(c \colon \mathbb{A}\hookrightarrow\langle 1^* \rangle\), i.e., that maps every atom to a unique word of the form \(\langle 1^k \rangle\) for some \(k \in \mathbb{N}\). We say that a function \(f \colon (\mathbb{A}\cup \Sigma)^* \to (\mathbb{A}\cup \Gamma)^*\) is deatomisable if there exists a rational function \(f^\dagger \colon (\Sigma \cup \{ \langle, \rangle, 1 \})^* to (\Gamma \cup \{ \langle, \rangle, 1 \})^*\) such that for all atomic codes \(c \colon \mathbb{A}\hookrightarrow\langle 1^* \rangle\), the following commutes

\[ c \circ f = f^\dagger \circ c \quad . \]

Prove that the following are equivalent:

1. A function \(f\) is deatomisable,
2. It is realisable by an atomic bimachine.