Synthesis of Computable Regular Functions of Infinite Words

TL;DR

This paper develops a decision procedure to determine whether regular functions from infinite words to infinite words are computable, based on their continuity, and provides methods to synthesize corresponding Turing machines.

Contribution

It introduces a generic characterization of continuity for regular functions and shows decidability of their computability, including efficient algorithms for rational functions.

Findings

Decidability of continuity for regular functions.

Equivalence of computability and continuity for regular functions.

Efficient NLogSpace algorithm for rational functions.

Abstract

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming $\omega$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function $f$ (equivalently specified by one of the aforementioned transducer model), is $f$ computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in $\mathsf{NLogSpace}$ (it was already known to be in $\mathsf{PTime}$ by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

Equations

$$\begin{array}[]{lll}p_{1}\xrightarrow{u|u_{1}}q_{1}\xrightarrow{v|v_{1}}q_{1}\\ p_{2}\xrightarrow{u|u_{2}}q_{2}\xrightarrow{v|v_{2}}q_{2}\xrightarrow{wz^{\omega}|y_{2}}\\ \end{array}$$

$$\begin{array}[]{lll}\exists\pi_{1}\colon p_{1}\xrightarrow{u^{\prime}|u_{1}^{\prime}}q_{1},\ \exists\pi_{1}^{\prime}\colon q_{1}\xrightarrow{v|v_{1}}q_{1}\\ \exists\pi_{2}\colon p_{2}\xrightarrow{u^{\prime}|u_{2}^{\prime}}q_{2},\ \exists\pi_{2}^{\prime}\colon q_{2}\xrightarrow{v|v_{2}}q_{2}\\ \big{(}\mathsf{init}(p_{1})\wedge\mathsf{init}(p_{2})\wedge\mathsf{acc}(q_{1})\big{)}\wedge\big{(}\mathsf{mismatch}(u_{1}^{\prime},u_{2}^{\prime})\big{)}\end{array}$$

$$\begin{array}[]{lll}\exists\pi_{1}\colon p_{1}\xrightarrow{u|u_{1}}q_{1},\ \exists\pi_{1}^{\prime}\colon q_{1}\xrightarrow{v|v_{1}}q_{1}\\ \exists\pi_{2}\colon p_{2}\xrightarrow{u|u_{2}}q_{2},\ \exists\pi_{2}^{\prime}\colon q_{2}\xrightarrow{v|v_{2}}q_{2},\ \exists\pi_{2}^{\prime\prime}\colon q_{2}\xrightarrow{w|w_{2}}r_{2}\\ \big{(}\mathsf{init}(p_{1})\wedge\mathsf{init}(p_{2})\wedge\mathsf{acc}(q_{1})\big{)}\wedge\big{(}(v_{2}=\epsilon\wedge\mathsf{mismatch}(u_{1},u_{2}w_{2}))\big{)}\end{array}$$

$$\underset{(i,j)\in Q^2,\text{trav}\in \{LL,RL,LR,RR\}}{\bigwedge }\#u\#\in L(A_{i,j}^{\text{trav}})\iff \#u\#\in L(B_{i,j}^{\text{trav}})$$

$$r={\rho }_0{L}_1{R}_1\dots L_n{R}_n{\rho }_1{\ell }^{\omega }$$

Full text

For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

This work is partially supported by the MIS project F451019F (F.R.S.-FNRS) and the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS and FWO). Emmanuel Filiot is a research associate at F.R.S.-FNRS

This work is partially supported by the ERC Consolidator grant LIPA683080, as well as ANR DELTA (grant ANR-16-CE40-0007)

1. Introduction

Let Inputs and Outputs be two arbitrary sets of elements called inputs and outputs respectively. A general formulation of the synthesis problem is as follows: for a given specification of a function $S\colon\textsf{Inputs}\rightarrow 2^{\textsf{Outputs}}$ relating any input $u\in\mathsf{dom}(S)$111$\mathsf{dom}(S)$ is the domain of $S$, i.e. the set of inputs that have a non-empty image by $S$. to a set of outputs $S(u)\subseteq\textsf{Outputs}$, decide whether there exists a (total) function $f\colon\mathsf{dom}(S)\rightarrow\textsf{Outputs}$ such that $(i)$ for all $u\in\mathsf{dom}(S)$, $f(u)\in S(u)$ and $(ii)$ $f$ satisfies some additional constraints such as being computable in some way, by some device which is effectively returned by the synthesis procedure. Assuming the axiom of choice, the relaxation of this problem without constraint $(ii)$ always has a positive answer. However with additional requirement $(ii)$, a function $f$ realising $S$ may not exist in general. In this paper, we consider the particular case where the specification $S$ is functional,222In this case, we just write $S(u)=v$ instead of $S(u)=\{v\}$. in the sense that $S(u)$ is singleton set for all $u\in\mathsf{dom}(S)$. Even in this particular case, $S$ may not be realisable while satisfying requirement $(ii)$.

The latter observation on the functional case can already be made in the Church approach to synthesis [Alo62, JL69], for which $\textsf{Inputs},\textsf{Outputs}$ are sets of infinite words and $f$ is required to be implementable by a Mealy machine (a deterministic automaton which can output symbols). More precisely, an infinite word $\alpha$ over a finite alphabet $\Sigma$ is a function $\alpha\colon\mathbb{N}\rightarrow\Sigma$ and is written as $\alpha=\alpha(0)\alpha(1)\ldots$. The set of infinite words over $\Sigma$ is denoted by $\Sigma^{\omega}$. In Church $\omega$-regular synthesis, we have $\textsf{Inputs}=\Sigma_{i}^{\omega}$ and $\textsf{Outputs}=\Sigma_{o}^{\omega}$, and functions $S$ are specified by $\omega$-automata over $\Sigma_{i}.\Sigma_{o}$. Thus, such an automaton defines a language $L\subseteq(\Sigma_{i}.\Sigma_{o})^{\omega}$ and in turn, through projection, a function $S_{L}$ defined by $S_{L}(i_{1}i_{2}\dots)=\{o_{1}o_{2}\dots\mid i_{1}o_{1}i_{2}o_{2}\dots\in L\}$. Such a specification is said to be synchronous, meaning that it alternatively reads an input symbol and produces an output symbol. It is also $\omega$-regular because it can be represented as an automaton over $\Sigma_{i}.\Sigma_{o}$. As an example, consider $\Sigma_{i}=\Sigma_{o}=\{a,b,@\}$ and the function $S_{\sf swap}$ defined only for all words of the form $u_{1}\sigma@u_{2}$ such that $u_{1}\in\{a,b\}^{*}$ and $\sigma\in\{a,b\}$ by $S_{\sf swap}(u_{1}\sigma@u_{2})=\sigma u_{1}@u_{2}$. The specification $S_{\sf swap}$ is easily seen to be synchronous and $\omega$-regular, but not realisable by any Mealy machine. This is because a Mealy machine is an input deterministic model and so cannot guess the last symbol before the $@$ symbol.

1.1. Computability of functions over infinite words

In Church synthesis, the notion of computability used for requirement $(ii)$ is that of being computable by a Mealy machine. While this makes sense in a reactive scenario where output symbols (reactions) have to be produced immediately after input symbols are received, this computability notion is too strong in a more relaxed scenario where reactivity is not required. Instead, we propose here to investigate the synthesis problem for functional specifications over infinite words where the computability assumption $(ii)$ for $f$ is just being computable by some algorithm (formally a Turing machine) running on infinite inputs. In other words, our goal is to synthesize algorithms from specifications of functions of infinite words. There are classical computability notions for infinite objects, like infinite sequences of natural numbers, motivated by real analysis, or computation of functions of real numbers. The model of computation we consider for infinite words is a deterministic machine with three tapes: a read-only one-way tape holding the input, a two-way working tape with no restrictions and a write-only one-way output tape. All three tapes are infinite on the right. A function $f$ is computable if there exists such a machine $M$ such that, if its input tape is fed with an infinite word $x$ in the domain of $f$, then $M$ outputs longer and longer prefixes of $f(x)$ when reading longer and longer prefixes of $x$. This machine model has been defined in [Wei00, Chap. 2]. If additionally one requires the existence of a computable function $m\colon\mathbb{N}\rightarrow\mathbb{N}$ such that for all $i\in\mathbb{N}$, for all infinite input $x$, $M$ writes at least $i$ output symbols when reading $m(i)$ input symbols of $x$, we obtain the notion of uniform computability. This offers promptness guarantees on the production of output symbols with respect to the number of symbols read on input.

Obviously, not all functions are computable. In this paper, we aim to solve the following synthesis problem: given a (finite) specification of a (partial) function $f$ from infinite words to infinite words, is $f$ computable (respectively uniformly computable)? If it is the case, then the procedure should return a Turing machine computing $f$ (respectively uniformly computing $f$).

1.2. Examples

The function $S_{\sf swap}$ is computable. Since it is defined over all inputs containing at least one $@$ symbol, if a Turing machine is fed with such a word, it suffices for it to read its input and write it in working tape, until the first $@$ symbol is met. Now go back in the working tape to see the last symbol read before $@$, write the same in output tape. It is followed by further going back to the beginning in the working tape, and copying all the symbols of working tape except the last one from left to right into the output tape. This gives us the prefix $\sigma u_{1}$. The suffix $@u_{2}$ can simply be produced by copying the content of input tape into output tape.

Over the alphabet $\Sigma=\{a,b\}$, consider the function $f_{\infty}$ defined by $f_{\infty}(u)=a^{\omega}$ if $u$ contains infinitely many $a$s, and by $b^{\omega}$ otherwise. This simple function is not computable, as it requires to read the whole infinite input to produce even the very first output symbol. For any word $u\in\Sigma^{*}$, we denote by $\overline{u}$ its mirror (e.g. $\overline{abaa}=aaba$). Consider the (partial) function $f_{\sf mir}$ defined on $(\Sigma^{*}\sharp)^{\omega}$ by $f(u_{1}\sharp u_{2}\sharp\ldots)=\overline{u_{1}}\sharp\overline{u_{2}}\sharp\ldots$. It is computable by a machine that stores its input $u_{1}$ in memory until the first $\sharp$ is read, then outputs $\overline{u_{1}}$, and proceeds with $u_{2}$, and so on. It is however not uniformly computable. Indeed, if it were, with some $m\colon\mathbb{N}\rightarrow\mathbb{N}$, then, for inputs $u_{1}\sharp u_{2}\sharp\cdots$ such that $|u_{1}|>m(1)$, it is impossible to determine the first output symbol (which is the last of $u_{1}$) by reading only a prefix of length $m(1)$ of $u_{1}$.

Finally, consider the (partial) function $f_{\sf dbl}$ defined on $(\Sigma^{*}\sharp)^{\omega}$ by $f(u_{1}\sharp u_{2}\sharp$ $\ldots)=$ $u_{1}u_{1}\sharp$ $u_{2}u_{2}$ $\sharp\ldots$. Similarly as before, it is computable but also uniformly computable: to determine the $i^{\text{th}}$ output symbol, it suffices to read an input prefix of length at most $i$. Indeed, let $u_{1}\sharp u_{2}\sharp\ldots\sharp u$ be a prefix of length $i$ of the input $x$, then $u_{1}u_{1}\sharp u_{2}u_{2}\sharp\ldots\sharp u$ is a prefix of $f(x)$ of length $\geq i$.

1.3. Computability and continuity

There are strong connections between computability and continuity: computable functions are continuous for the Cantor topology, that is where words are close to each other if they share a long common prefix. Intuitively, it is because the very definition of continuity asks that input words sharing longer and longer prefixes also share longer and longer output prefixes. It is the case of the functions $f_{\sf mir}$ and $f_{\sf dbl}$ seen before. Likewise, uniformly computable functions are uniformly continuous. The reverse direction does not hold in general: assuming an effective enumeration $M_{1},M_{2},\dots$ of Turing machines (on finite word inputs), the function $f_{\sf halt}$ defined as $f_{\sf halt}:x\mapsto b_{1}b_{2}b_{3}\ldots$ where $b_{i}\in\{0,1\}$ is such that $b_{i}=1$ if and only if $M_{i}$ halts on input $\epsilon$, is not computable but (uniformly) continuous (as it is constant).

1.4. Beyond synchronous functions: regular functions

Functional specifications in the Church $\omega$-regular synthesis problem range over the class of synchronous functions as described before: they can be specified using automata over $\Sigma_{i}.\Sigma_{o}$. For example, while $S_{\sf swap}$ and $f_{\infty}$ are synchronous, $f_{\sf mir}$ and $f_{\sf dbl}$ are not. In this paper, we intend to go much beyond this class by dropping the synchronicity assumption and consider the so-called class of regular functions. It is a well-behaved class, captured by several models such as streaming $\omega$-string transducers (SST), deterministic two-way Muller transducers with look around (2DMTla), and also by MSO-transducers [AFT12, Thm. 1, Prop. 1]. We propose the model of deterministic two-way transducers with a prophetic Büchi look-ahead (2DFTpla) and show that they are equivalent to 2DMTla. This kind of transducer is defined by a deterministic two-way automaton without accepting states, extended with output words on the transitions, and which can consult another automaton, called the look-ahead automaton, to check whether an infinite suffix satisfies some regular property. We assume this automaton to be a prophetic Büchi automaton [CPP08, Sec. 7], because this class is naturally suited to implement a regular look-ahead, while capturing all regular languages of infinite words. Look-ahead is necessary to capture functions such as $f_{\infty}$. Two-wayness is needed to capture, for instance, functions $f_{\sf dbl}$ and $f_{\sf mir}$.

1.5. Contributions

We call effectively reg-preserving functions those functions that effectively preserve regular languages by inverse image [SH63, Kos74, SM76, PS17]. This includes for instance rational functions, regular functions and the more general class of polyregular functions [Boj18, EHS21]. We first show that for effectively reg-preserving functions, computability and continuity coincide, respectively, uniform computability and uniform continuity (Section 3, Theorem 2). To the best of our knowledge, this connection was not made before. The connection is effective, in the sense that when $f$ is effectively reg-preserving and continuous (resp. uniformly continuous), we can effectively construct a Turing machine computing $f$ (resp. uniformly computing $f$).

For rational functions (functions defined by non-deterministic one-way Büchi transducers), we show that continuity and uniform continuity are decidable in NLogSpace (Section 5, Theorem 8). Continuity and uniform continuity for rational functions were already known to be decidable in PTime, from Prieur [Pri02, Prop. 4]. However, Prieur’s proof techniques do not transfer to the two-way case. We then prove that uniform continuity (and hence uniform computability) is decidable in PSpace for regular functions given by deterministic Büchi two-way transducers with look-ahead (Section 5, Theorem 13). Using the same techniques, we also get the decidability of continuity (and hence computability) for regular functions (Theorem 18) in PSpace. For both problems, we show that this upper-bound is tight, namely, both problems are PSpace-hard.

Our proof technique relies on a characterisation of non-continuous reg-preserving functions by the existence of pairs of sequences of words which have a nice regular structure (Section 4, Lemma 6). Based on this, we derive a decision procedure for continuity of rational functions by checking in NLogSpace a structural transducer pattern. This pattern expresses properties of synchronised loops on two runs of the transducers. The case of regular functions is much more involved as loops in two-way automata or transducers are more complex. We also give a characterisation via a structural pattern which we show to be checkable by a bounded-visit non-deterministic two-way Parikh automaton of polynomial size, yielding the PSpace upper bound as those automata can be checked in PSpace for emptiness [FGM19].

1.6. Related work

The notion of continuity has not been extensively studied in the transducers literature over infinite words. The work by Prieur [Pri02] is the closest to ours, while [CSV13] looks at continuity of regular functions encoded by $\omega$-automata.

Notions of continuity with respect to language varieties have been studied for rational functions of finite words in [CCP17, CCP20]. Our notion of uniform continuity can be linked to continuity with respect to a particular language variety which was not studied in [CCP17] (namely the non-erasing variety generated by languages of the shape $uA^{*}$). A quite strong Lipschitz continuity notion, called bounded variation due to Choffrut (e.g. [Cho03]), was shown to capture, over finite words, the sequential functions (the corresponding topology is however trivial, hence simple continuity is not very interesting in this context).

Another result connecting computability and continuity is from [CKLP15] where the authors find that some notion of computability by $\mathrm{AC}^{0}$ circuits corresponds, over sequential functions, to continuity with respect to some language variety.

Our result on rational functions has been extended recently to rational functions of infinite words over an infinite alphabet in [EFR20]. More precisely, continuity for functions of infinite data words defined by (one-way) transducers with registers has been shown to be decidable. The proof of [EFR20] goes by reduction to the finite alphabet setting and uses our result presented in the paper [DFKL20].

Changes from the conference version

The results in this paper are an extension of the work presented at CONCUR 2020 [DFKL20]. In the conference version, Lemmas 6 and 7 had only a short proof sketch; this version contains the full technical details. A major change from the conference version is in Section 5.2. This has an added contribution, where we present a new proof for the decidability of continuity and uniform continuity for regular functions. To aid us in this, we define what is called a critical pattern (Section 5.2.3) and show that the existence of such patterns in two way transducers help in deciding the continuity of the corresponding regular function (Proposition 10). Finally, in the proof of Theorem 13 and Theorem 18, we analyze the complexity of the pattern detection, which in turn yields a (tight) upper-bound for the complexity of checking continuity and uniform continuity of regular functions; this was left open in the CONCUR 20 paper.

2. Languages, Automata and Transducers over $\omega$-Words

Given a finite set $\Sigma$, we denote by $\Sigma^{*}$ (resp. $\Sigma^{\omega}$) the set of finite (resp. infinite) words over $\Sigma$, and by $\Sigma^{\infty}$ the set of finite and infinite words. Let $\Sigma^{j}$ represent the set of all words over $\Sigma$ with length $j$. We denote by $|u|\in\mathbb{N}\cup\{\infty\}$ the length of $u\in\Sigma^{\infty}$ (in particular $|u|=\infty$ if $u\in\Sigma^{\omega}$). For a word $w=a_{1}a_{2}a_{3}\dots$, $w[{\colon}j]$ denotes the prefix $a_{1}a_{2}\dots a_{j}$ of $w$. Let $w[j]$ denote $a_{j}$, the $j^{\text{th}}$ symbol of $w$ and $w[j{\colon}]$ denote the suffix $a_{j+1}a_{j+2}\dots$ of $w$. For a word $w$ and $i\leq j$, $w[i{\colon}j]$ denotes the factor of $w$ with positions from $i$ to $j$, both included. For two words $u,v\in\Sigma^{\infty}$, $uv$ (resp. $u\prec v$) denotes that $u$ is a prefix (resp. strict prefix) of $v$ (in particular if $u,v\in\Sigma^{\omega}$, $u\preceq v$ if and only if $u=v$). For $u\in\Sigma^{*}$, let ${\uparrow}u$ denote the set of words $w\in\Sigma^{\infty}$ having $u$ as prefix i.e. $uw$. Let mismatch be a function which takes two words, and returns a boolean value, denoted by $\textsf{mismatch}(u,v)$ for $u$ and $v$; it returns true if there exists a position $i\leq|u|,|v|$ such that $u[i]\neq v[i]$, and returns false otherwise. The longest common prefix between two words $u$ and $v$ is denoted by $u\wedge v$ and their distance is defined as $d(u,v)=0$ if $u=v$, and $2^{-|u\wedge v|}$ if $u\neq v$.

A Büchi automaton is a tuple $B=(Q,\Sigma,\delta,Q_{0},F)$ consisting of a finite set of states $Q$, a finite alphabet $\Sigma$, a set $Q_{0}\subseteq Q$ of initial states, a set $F\subseteq Q$ of accepting states, and a transition relation $\delta\subseteq Q\times\Sigma\times Q$. A run $\rho$ on a word $w=a_{1}a_{2}\ldots\in\Sigma^{\omega}$ starting in a state $q_{1}$ in $B$ is an infinite sequence $q_{1}\stackrel{{\scriptstyle a_{1}}}{{\rightarrow}}q_{2}\stackrel{{\scriptstyle a_{2}}}{{\rightarrow}}\dots$ such that $(q_{i},a_{i},q_{i+1})\in\delta$ for all $i\in\mathbb{N}$. Let $\mathsf{Inf}(\rho)$ denote the set of states visited infinitely often along $\rho$. The run $\rho$ is a final run if $\mathsf{Inf}(\rho)\cap F\neq\emptyset$. A run is accepting if it is final and starts from an initial state. A word $w\in\Sigma^{\omega}$ is accepted ($w\in L(B)$) if it has an accepting run. A language $L$ of $\omega$-words is called $\omega$-regular if $L=L(B)$ for some Büchi automaton $B$.

An automaton is co-deterministic if any two final runs on any word $w$ are the same [CPP08, Sec. 7.1]. Likewise, an automaton is co-complete if every word has at least one final run. A prophetic automaton $P=(Q_{P},\Sigma,\delta_{P},Q_{0},F_{P})$ is a Büchi automaton which is co-deterministic and co-complete. Equivalently, a Büchi automaton is prophetic if and only if each word admits a unique final run. The states of the prophetic automaton partition $\Sigma^{\omega}$: each state $q$ defines a set of words $w$ such that $w$ has a final run starting from $q$. For any state $q$, let $L(P,q)$ be the set of words having a final run starting at $q$. Then $\Sigma^{\omega}=\uplus_{q\in Q_{P}}L(P,q)$. It is known [CPP08, Thm. 7.2] that prophetic Büchi automata capture $\omega$-regular languages.

2.1. Transducers

We recall the definitions of one-way and two-way transducers over infinite words. A one-way transducer $\mathcal{A}$ is a tuple $(Q,\Sigma,\Gamma,\delta,Q_{0},F)$ where $Q$ is a finite set of states, $Q_{0},F$ respectively are sets of initial and final states; $\Sigma,\Gamma$ respectively are the input and output alphabets; $\delta\subseteq(Q\times\Sigma\times Q\times\Gamma^{*})$ is the transition relation. We equip $\mathcal{A}$ with a Büchi acceptance condition. A transition in $\delta$ of the form $(q,a,q^{\prime},\gamma)$ represents that from state $q$, on reading a symbol $a$, the transducer moves to state $q^{\prime}$, producing the output $\gamma$. Runs, final runs and accepting runs are defined exactly as in Büchi automata, with the addition that each transition produces some output $\in\Gamma^{*}$.

The output produced by a run $\rho$, denoted $\mathsf{out}(\rho)$, is obtained by concatenating the outputs generated by transitions along $\rho$. Let $\mathsf{dom}(\mathcal{A})$ represent the language accepted by the underlying automaton of $\mathcal{A}$, ignoring the outputs. The relation computed by $\mathcal{A}$ is defined as $[\![\mathcal{A}]\!]=\{(u,v)\in\Sigma^{\omega}\times\Gamma^{\omega}\mid u\in\mathsf{dom}(\mathcal{A}),\rho\leavevmode\nobreak\ \text{is an accepting run of}\leavevmode\nobreak\ u,\mathsf{out}(\rho)=v\}$.333We assume that final runs always produce infinite words, which can be enforced syntactically by a Büchi condition such that any input word produces non-empty output in a single loop execution containing Büchi accepting state. We say that $\mathcal{A}$ is functional if $[\![\mathcal{A}]\!]$ is a function. A relation (function) is rational if it is recognised by a one-way (functional) transducer.

Two-way transducers extend one-way transducers and two-way finite state automata. A two-way transducer is a two-way automaton with outputs. In [AFT12, Prop. 1], regular functions are shown to be those definable by a two-way deterministic transducer with Muller acceptance condition, along with a regular look-around (2DMTla). In this paper, we propose an alternative machine model for regular functions, namely, 2DFTpla. A 2DFTpla is a deterministic two-way automaton with outputs, along with a look-ahead given by a prophetic automaton.

Let $\Sigma_{\vdash}=\Sigma\uplus\{\vdash\}$. Formally, a 2DFTpla is a pair $(\mathcal{T},A)$ where $A=(Q_{A},\Sigma,\delta_{A},S_{A},F_{A})$ is a prophetic Büchi automaton and $\mathcal{T}=(Q,\Sigma,\Gamma,\delta,$ $q_{0})$ is a two-way transducer such that $\Sigma$ and $\Gamma$ are finite input and output alphabets, $Q$ is a finite set of states, $q_{0}\in Q$ is a unique initial state, $\delta\colon Q\times\Sigma_{\vdash}\times Q_{A}\rightarrow Q\times\Gamma^{*}\times\{-1,+1\}$ is a partial transition function. $\mathcal{T}$ has no acceptance condition: every infinite run in $\mathcal{T}$ is a final run. A two-way transducer stores its input ${\vdash}a_{1}a_{2}\dots$ on a two-way tape, and each index of the input can be read multiple times. A configuration of a two-way transducer is a tuple $(q,i)\in Q\times\mathbb{N}$ where $q\in Q$ is a state and $i\in\mathbb{N}$ is the current position on the input tape. The position is an integer representing the gap between consecutive symbols. Thus, before ${\vdash}$, the position is 0, between ${\vdash}$ and $a_{1}$, the position is 1, between $a_{i}$ and $a_{i+1}$, the position is $i+1$ and so on. The 2DFTpla is deterministic: for every word $w=\leavevmode\nobreak\ {\vdash}a_{1}a_{2}a_{3}\ldots\in\leavevmode\nobreak\ {\vdash}\Sigma^{\omega}$, every input position $i\in\mathbb{N}$, and state $q\in Q$, there is a unique state $p\in Q_{A}$ such that $a_{i}a_{i+1}\ldots\in L(A,p)$. Given $w=a_{1}a_{2}\ldots$, from a configuration $(q,i)$, on a transition $\delta(q,a_{i},p)=(q^{\prime},\gamma,d)$, $d\in\{-1,+1\}$, such that $a_{i+1}a_{i+2}\ldots\in L(A,p)$, we obtain the configuration $(q^{\prime},i+d)$ and the output $\gamma$ is appended to the output produced so far. This transition is denoted as $(q,i)\stackrel{{\scriptstyle a_{i},p/\gamma}}{{\longrightarrow}}(q^{\prime},i+d)$. A run $\rho$ of a 2DFTpla $(\mathcal{T},A)$ is a sequence of transitions $(q_{0},i_{0}=0)\stackrel{{\scriptstyle a_{i_{0}},p_{1}/\gamma_{1}}}{{\longrightarrow}}(q_{1},i_{1})\stackrel{{\scriptstyle a_{i_{1}},p_{2}/\gamma_{2}}}{{\longrightarrow}}\cdots$. The output of $\rho$, denoted $\mathsf{out}(\rho)$ is then $\gamma_{1}\gamma_{2}\cdots$. The run $\rho$ reads the whole word $w$ if $\mathsf{sup}\{i_{n}\mid 0\leq n<|\rho|\}=\infty$. The output $[\![(\mathcal{T},A)]\!](w)$ of a word $w$ on run $\rho$ is defined only when $\mathsf{sup}\{i_{n}\mid 0\leq n<|\rho|\}=\infty$, and equals $\mathsf{out}(\rho)$. 2DFTpla are equivalent to 2DMTla, and capture all regular functions. It is easy to see because different representations of $\omega$- look-ahead are equiexpressive, the look-behind of $2\textsf{DMT}\textsubscript{{la}}$ can be eliminated while preserving the expressiveness, and one can encode the acceptance condition of $2\textsf{DMT}\textsubscript{{la}}$ as part of the look-ahead in $2\textsf{DFT}\textsubscript{{pla}}$ (see Appendix A for the proof).

Theorem 1**.**

A function $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ is regular if and only if it is 2DFTpla definable.

{exa}

Consider the function $g\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ over $\Sigma=\Gamma=\{a,b\}$ such that $g(uab^{\omega})=uub^{\omega}$ for $u\in\Sigma^{*}$ and $g(b^{\omega})=b^{\omega}$. The 2DFTpla is shown in Figure 1 with the prophetic look-ahead automaton $A$ on the right. The transitions are decorated as $\alpha,p\mid\gamma,d$ where $\alpha\in\{a,b\}$, $p$ is a state of $A$, $\gamma$ is the output and $d$ is the direction. In transitions not using the look-ahead information, the decoration is simply $\alpha\mid\gamma,d$. Notice that $\mathcal{L}(A,p_{1})=\leavevmode\nobreak\ \Sigma^{+}ab^{\omega}$, $\mathcal{L}(A,p_{2})=\leavevmode\nobreak\ {a}b^{\omega}$, $\mathcal{L}(A,p_{3})=b^{\omega}$, $\mathcal{L}(A,\{p_{4},p_{5}\})$ is the set of words having infinitely many $a$s. Each word in $\Sigma^{\omega}$ has a unique final run.

We also use a look-ahead-free version of two-way transducers in some of the proofs, where we also have a Büchi acceptance condition given by a set of states $F$, just as for Büchi automata. The resulting model is called two-way deterministic Büchi transducer (2DBT). The definitions of configuration, run, and the semantics are done just like for 2DFTpla.

3. Computability versus Continuity

Computability of a function on infinite words can be described intuitively in the following way: there is an algorithm which, given access to the input word, can enumerate the letters in the output word. We also investigate a stronger notion of computability, which we call uniform computability. The main idea is that given some input word $x$ and some position $j$ one can compute the $j^{\text{th}}$ position of the output in time that depends on $j$ but not on $x$. An appealing aspect of uniform computability is that it offers a uniform bound on the number of input symbols one needs to read in order to produce the output at some fixed precision.

{defi}

[Computability/Uniform computability] A function $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ is computable if there exists a deterministic multitape Turing machine $M$ computing it in the following sense. The machine $M$ has a read-only one-way input tape, a two-way working tape, and a write-only one-way output tape. All tapes have a left delimiter $\vdash$ and are infinite to the right. Let $x\in\mathsf{dom}(f)$. For any $j\in\mathbb{N}$, let $M(x,j)$ denote the output produced by $M$ till the time it moves to the right of position $j$, onto position $j+1$ in the input (or $\epsilon$ if this move never happens). The function $f$ is computable by $M$ if for all $x\in\mathsf{dom}(f)$, for all $i\geq 0$, there exists $j\geq 0$ such that $f(x)[{\colon}i]M(x,j)$.

Moreover if there exists a computable function $m\colon\mathbb{N}\rightarrow\mathbb{N}$ (called a modulus of continuity for $M$) such that for all $x\in\mathsf{dom}(f)$, for all $i\geq 0$, $f(x)[{\colon}i]M(x,m(i))$, $f$ is called uniformly computable.

It turns out that there is a quite strong connection between computability and continuity of functions. In particular computable functions are always continuous. This can be seen intuitively since given a deterministic Turing machine, it must behave the same on the common prefixes of two words. Hence two words with a very long common prefix must have images by the machine that have a somewhat long common prefix. This connection also transfers to uniform computability and uniform continuity. We start by formally defining continuity and uniform continuity.

{defi}

[Continuity/Uniform continuity]

 We interchangeably use the following two textbook definitions [Rud76] of continuity.

1. (1)

A function $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ is continuous at $x\in\mathsf{dom}(f)$ if (equivalently)

• (a)

for all $(x_{n})_{n\in\mathbb{N}}$ converging to $x$, where $x_{i}\in\mathsf{dom}(f)$ for all $i\in\mathbb{N}$, $(f(x_{n}))_{n\in\mathbb{N}}$ converges.

• (b)

$\forall i\geq 0$ $\exists j\geq 0$ $\forall y\in\mathsf{dom}(f)$, $|x\wedge y|\geq j\Rightarrow|f(x)\wedge f(y)|\geq i$ 2. (2)

A function is continuous if it is continuous at every $x\in\mathsf{dom}(f)$.

A function $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ is uniformly continuous if:

there exists $m\colon\mathbb{N}\rightarrow\mathbb{N}$, called a modulus of continuity for $f$ such that,

$\forall i\geq 0$, $\forall x,y\in\mathsf{dom}(f)$, $|x\wedge y|\geq m(i)\Rightarrow|f(x)\wedge f(y)|\geq i$.

{exa}

As explained in the introduction, the function $f_{\infty}$ is not continuous, and, as we will see later, is thus not computable. The function $f_{\textsf{halt}}$ is continuous, even uniformly continuous (it is constant) yet is obviously not computable. The function $f_{\textsf{mir}}$ is computable, however is not uniformly continuous, two words can be arbitrarily close but with far away outputs: consider $a^{n}\sharp^{\omega}$ and $a^{n}b\sharp^{\omega}$. Finally, the function $f_{\textsf{dbl}}$ is uniformly computable.

We now investigate the relationship between continuity and computability for functions that are effectively reg-preserving. More precisely, we say that a function $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ is effectively reg-preserving if there is an algorithm which, for any automaton recognising a regular language $L\subseteq\Gamma^{\omega}$, produces an automaton recognising the language $f^{-1}(L)=\{u\mid f(u)\in L\}$.

Two well-studied classes (see e.g. [Fil15]) of reg-preserving functions are the rational and the regular functions, which we will study in Section 5. As announced, continuity and computability coincide for effectively reg-preserving functions:

Theorem 2**.**

An effectively reg-preserving function $f\colon\Sigma^{\omega}\to\Gamma^{\omega}$ is computable (resp. uniformly computable) if and only if it is continuous (resp. uniformly continuous).

Proof 3.1**.**

$\Rightarrow$) This implication is easy and actually holds without the reg-preserving assumption. Assume that $f$ is computable. We prove the continuity of $f$. Let $M$ be the machine computing $f$. Let $x\in\mathsf{dom}(f)$ be the content on the input tape of $M$. Intuitively, the longer the prefix of input $x\in\mathsf{dom}(f)$ is processed by $M$, the longer the output produced by $M$ on that prefix, which converges to $f(x)$, according to the definition of computability. For all $i\geq 0$, define $\mathsf{Pref_{M}}(x,i)$ to be the smallest $j\geq 0$ such that, when $M$ moves to the right of $x[{\colon}j]$ into cell $j+1$, it has output at least the first $i$ symbols of $f(x)$. For any $i\geq 0$, choose $j=\mathsf{Pref_{M}}(x,i)$. Consider any $z\in\mathsf{dom}(f)$ such that $|x\wedge z|\geq j$. After reading $j$ symbols of $x$, the machine $M$ outputs at least $i$ symbols of $f(x)$. Since $|x\wedge z|\geq j$, the first $j$ symbols of $x$ and $z$ are the same, and $M$ being deterministic, outputs the same $i$ symbols on reading the first $j$ symbols of $z$ as well. These $i$ symbols form the prefix for both $f(x),f(z)$, and hence, $|f(x)\wedge f(z)|\geq i$.

Thus, for every $x\in\mathsf{dom}(f)$ and for all $i$, there exists $j=\mathsf{Pref_{M}}(x,i)$ such that, for all $z\in\mathsf{dom}(f)$, if $|x\wedge z|\geq j$, then $|f(x)\wedge f(z)|\geq i$ implying continuity of $f$. Moreover, if $f$ is uniformly computable, then the modulus of continuity of $M$ is in particular a modulus of continuity for $f$ and is thus uniformly continuous.

$\Leftarrow$) The converse direction is less trivial and makes use of the reg-preserving assumption. Suppose that $f$ is continuous. We design the machine $M$, represented as Algorithm 1, which is shown to compute $f$. This machine processes longer and longer prefixes $x[{\colon}i]$ of its input $x$ (for loop at line 2), and tests (line 4) whether a symbol $\gamma$ can be safely appended to the output. The test ensures that the invariant $\textsf{out}\preceq f(x)$ is preserved at any point. Moreover, the continuity of $f$ at $x$ ensures that out is updated infinitely often. The only thing left to obtain computability is that the test of line 4 is decidable. Let $u$ and $v$ be two words, deciding $f({\uparrow}u)\subseteq{\uparrow}v$ is equivalent to deciding if $\mathsf{dom}(f)\cap{\uparrow}u\subseteq f^{-1}({\uparrow}v)$. These sets are effectively regular since $u,v$ are given and $f$ is effectively reg-preserving, and $\mathsf{dom}(f)=f^{-1}(\Gamma^{\omega})$. Since the constructions are effective, and the languages are regular, the inclusion is decidable.

We only have left to show that if $f$ is moreover uniformly continuous, then $M$ has a computable modulus of continuity. We start by showing that $f$ has a computable modulus of continuity. Let us consider the predicate $P(i,j)\colon\forall x,y\ |x\wedge y|\geq j\Rightarrow|f(x)\wedge f(y)|\geq i$. Then we define $m\colon i\mapsto\min\left\{j|\ P(i,j)\right\}$. Since $f$ is uniformly continuous, $m$ is indeed well defined and is a modulus of continuity of $f$. To show that $m$ is computable, we only have to show that $P(i,j)$ is decidable.

Let us consider the negation of $P(i,j)$: there exist $u,x_{1},x_{2},v_{1},v_{2},w_{1},w_{2}$ such that $|u|=j$, and $f(ux_{k})=v_{k}w_{k}$ for $k\in\left\{1,2\right\}$ with $|v_{1}|=|v_{2}|=i$ and $v_{1}\neq v_{2}$. Hence to decide $\neg P(i,j)$, we only have to find two words $v_{1}\neq v_{2}$ in $\Gamma^{i}$, such that $S\neq\emptyset$ where $S=\{vw\mid v\in\Sigma^{j},\leavevmode\nobreak\ \exists w_{1},w_{2},\leavevmode\nobreak\ \text{s.t.}\leavevmode\nobreak\ vw_{1}\in f^{-1}({\uparrow}v_{1}),\leavevmode\nobreak\ vw_{2}\in f^{-1}({\uparrow}v_{2})\}$. Since $f$ is effectively reg-preserving, $S$ is effectively regular. By searching exhaustively for words $v_{1},v_{2}\in\Gamma^{i}$ we get decidability of $P(i,j)$. We only have left to define a modulus of continuity for $M$. Let $m^{\prime}\colon\mathbb{N}\rightarrow\mathbb{N}$ be defined by $m^{\prime}(i)=m(i)+i$. If we read $m(i)$ symbols, we know we can output at least $i$ symbols. Hence in each of the next $i$ steps, we are guaranteed to output a letter. Hence $m^{\prime}$ is a modulus of continuity for $M$ and $f$ is uniformly computable.

Remark 3**.**

Note that we focus on functions that are effectively reg-preserving, but Algorithm 1 is actually more general than that. The continuity-computability equivalence indeed carries over to any class of functions for which the test in line 4 is decidable.

4. A Characterisation of Continuity and Uniform Continuity

We provide here a characterisation of continuity (and uniform continuity) for reg-preserving functions (we don’t need effectiveness here). The characterisation is based on a study of some particular properties of sequences and pairs of sequences which we define below.

Topology preliminaries

A regular word (sometimes called ultimately periodic) over $\Sigma$ is a word of the form $uv^{\omega}$ with $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$. The set of regular words is denoted by $\mathsf{Reg}(\Sigma)$. The topological closure of a language $L\subseteq\Sigma^{\omega}$, denoted by $\bar{L}$, is the smallest language containing it and closed under taking the limit of converging sequences, i.e. $\bar{L}=\left\{x\mid\ \forall u\prec x,\exists y,\ uy\in L\right\}$. A language is closed if it is equal to its closure. A sequence of words $\left(x_{n}\right)_{n\in\mathbb{N}}$ is called regular if there exists $u,v,w\in\Sigma^{*}$, $z\in\Sigma^{+}$ such that for all $n\in\mathbb{N}$, $x_{n}=uv^{n}wz^{\omega}$. The proof of the characterisation of continuity (Lemma 6) requires the following folklore or easy to show propositions:

Proposition 4**.**

Let $L\subseteq\Sigma^{\omega}$ be regular language, then

1. (1)

$\bar{L}$* is regular,* 2. (2)

$L\subseteq\overline{L\cap\mathsf{Reg}(\Sigma)}$* (i.e. the regular words are dense in a regular language),* 3. (3)

any regular word of $\bar{L}$ is the limit of a regular sequence of $L$

Proof 4.1**.**

Proof of Proposition 4.3: Let $L\subseteq\Sigma^{\omega}$ be regular. Let $uv^{\omega}$ be a regular word in $\bar{L}$. By regularity of $L$, there is a power of $v$, $v^{k}$ such that for any words, $w,x$, $wv^{k}x\in L\Leftrightarrow wv^{2k}x\in L$. Let us consider the language $K=\left\{x\mid\ uv^{k}x\in L\right\}$ which is non-empty since $uv^{\omega}\in\bar{L}$. Moreover, $K$ is regular, and thus contains a regular word $wz^{\omega}$. Hence we have that $uv^{\omega}$ is the limit of the sequence $\left(uv^{kn}wz^{\omega}\right)_{n\in\mathbb{N}}$ of $L$.

{defi}

Let $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$.

Let $\left(x_{n}\right)_{n\in\mathbb{N}}$ be a sequence of words in $\mathsf{dom}(f)$ converging to $x\in\Sigma^{\omega}$, such that $\left(f(x_{n})\right)_{n\in\mathbb{N}}$ is not convergent. Such a sequence is called a bad sequence at $x$ for $f$.

Let $\left(x_{n}\right)_{n\in\mathbb{N}}$ and $\left(x_{n}^{\prime}\right)_{n\in\mathbb{N}}$ be two sequences in $\mathsf{dom}(f)$ both converging to $x\in\Sigma^{\omega}$, such that either $\left(f(x_{n})\right)_{n\in\mathbb{N}}$ is not convergent, $\left(f(x_{n}^{\prime})\right)_{n\in\mathbb{N}}$ is not convergent, or $\lim_{n}f(x_{n})\neq\lim_{n}f(x_{n}^{\prime})$. Such a pair of sequences is called a bad pair of sequences at $x$ for $f$.

A pair of sequences is synchronised if it is of the form: $\left(\left(uv^{n}wz^{\omega}\right)_{n},\left(uv^{n}w^{\prime}z^{\prime\omega}\right)_{n}\right)$

Proposition 5**.**

A function is not continuous if and only if it has a bad pair at some point of its domain. A function is not uniformly continuous if and only if it has a bad pair.

Proof 4.2**.**

The case of continuous functions is obtained just by definition. For uniform continuity, consider a function $f$ with a bad pair $(\left(x_{n}\right)_{n\in\mathbb{N}},\left(x_{n}^{\prime}\right)_{n\in\mathbb{N}})$, and let us show that it is not uniformly continuous. We can assume that both $\left(f(x_{n})\right)_{n\in\mathbb{N}}$ and $\left(f(x_{n}^{\prime})\right)_{n\in\mathbb{N}}$ converge. Otherwise we can extract subsequences that converge, by compactness of $\Gamma^{\omega}$. Moreover, since the pair is bad, one can assume that they converge to different limits $y\neq y^{\prime}$. Let $i$ be such that $y[i]\neq y^{\prime}[i]$. For any $j$, one can find $N$ such that for all $n\geq N$, $|x_{n}\wedge x^{\prime}_{n}|\geq j$ since both sequences converge to $x$. Since $\left(f(x_{n})\right)_{n\in\mathbb{N}}$ converges to $y$, we can ensure that $N$ is large enough so that for all $n\geq N$, $|f(x_{n})\wedge y|\geq i$. We can also ensure that for $n\geq N$, $|f(x_{n}^{\prime})\wedge y^{\prime}|\geq i$ holds. Let $n\geq N$, we have both $|x_{n}\wedge x^{\prime}_{n}|\geq j$ and $|f(x_{n})\wedge f(x_{n}^{\prime})|<i$, which means that $f$ is not uniformly continuous.

Let $f$ be a function which is not uniformly continuous, we want to exhibit a bad pair of $f$. According to the definition, there exists $i$ such that for all $j$ there exist $x_{j},x_{j}^{\prime}$ with $|x_{j}\wedge x^{\prime}_{j}|\geq j$ but $|f(x_{j})\wedge f(x_{j}^{\prime})|<i$. By compactness of $\Sigma^{\omega}$, there exists a subsequence of $\left(x_{j}\right)_{j\in\mathbb{N}}$ which is convergent. Let $\left(x_{\tau(j)}\right)_{j\in\mathbb{N}}$, with $\tau\colon\mathbb{N}\rightarrow\mathbb{N}$ increasing, denote such a subsequence. Then we have for all $j$ that $|x_{\tau(j)}\wedge x_{\tau(j)}^{\prime}|\geq\tau(j)\geq j$ and $|f(x_{\tau(j)})\wedge f(x_{\tau(j)}^{\prime})|<i$. Therefore up to renaming the sequences, we can assume that for all $j$, $|x_{j}\wedge x_{j}^{\prime}|\geq j$ and $|f(x_{j})\wedge f(x_{j}^{\prime})|<i$, with $\left(x_{j}\right)_{j\in\mathbb{N}}$ being convergent. By repeating the process of extracting subsequences, we can assume that $\left(x_{j}^{\prime}\right)_{j\in\mathbb{N}}$, $\left(f(x_{j})\right)_{j\in\mathbb{N}}$, $\left(f(x_{j}^{\prime})\right)_{j\in\mathbb{N}}$ are also convergent. Since for any $j$, $|x_{j}\wedge x_{j}^{\prime}|\geq j$, the two sequences converge to the same limit. In the end we obtain that $(\left(x_{j}\right)_{j\in\mathbb{N}},\left(x_{j}^{\prime}\right)_{j\in\mathbb{N}})$ is a bad pair for $f$ at $\lim_{j}x_{j}=\lim_{j}x_{j}^{\prime}$.

Note that in case $\mathsf{dom}(f)$ is not compact, then we may not have a subsequence of $\left(x_{j}\right)_{j\in\mathbb{N}}$ which converges in $\mathsf{dom}(f)$. However, the definition of bad pairs does not require convergence in the domain; it only asks for convergence to some $x$, which need not be in $\mathsf{dom}(f)$.

The main result of this section is the following lemma which says that one can restrict to considering only synchronised bad pairs. In the following sections this characterisation will be used to decide continuity/uniform continuity.

Lemma 6** (Characterisation).**

A reg-preserving function is not continuous if and only if it has a synchronised bad pair at some point of its domain. A reg-preserving function is not uniformly continuous if and only if it has a synchronised bad pair.

Proof 4.3**.**

This lemma extends Proposition 5. It shows that, in the case of reg-preserving functions, one can restrict to considering synchronised pairs, which are much easier to deal with. The only if direction is a simple consequence of Proposition 5. For the other direction, we first show that for a reg-preserving function $f$, if there is a bad pair at some $x$, then there is one at some regular $z$, i.e. $z=uv^{\omega}$ for some finite words $u,v$. Moreover, for the case of non-uniform continuity, we show that $z$ can be chosen so that $x\in\mathsf{dom}(f)\Leftrightarrow z\in\mathsf{dom}(f)$. In a second step, since we have two sequences converging to a regular $z$, we show how to replace the bad pair by a bad pair of regular sequences, still using the fact that $f$ is reg-preserving. Finally, we prove that we can synchronise these two regular sequences and end up with a synchronised bad pair at $z$.

Let $f\colon\Sigma^{\omega}\rightarrow\Gamma^{\omega}$ be a reg-preserving function which is not uniformly continuous. Then according to Proposition 5, it has a bad pair $(\left(x_{n}\right)_{n\in\mathbb{N}},\left(x_{n}^{\prime}\right)_{n\in\mathbb{N}})$ at some point $x$. If $f$ is not continuous then we can assume that $x\in\mathsf{dom}(f)$. Our goal is to exhibit a synchronised bad pair at a point $z$, such that if $x\in\mathsf{dom}(f)$ then $z\in\mathsf{dom}(f)$.

By compactness of $\Gamma^{\omega}$, we can extract subsequences such that both $\left(f(x_{n})\right)_{n\in\mathbb{N}}$ and $\left(f(x_{n}^{\prime})\right)_{n\in\mathbb{N}}$ converge. Moreover, since the pair is bad, one can assume that they converge to different limits $y\neq y^{\prime}$. Let $i$ be such that $y[i]\neq y[i^{\prime}]$ and let $B_{y}=\left\{z\mid\ |y\wedge z|\geq i\right\}={\uparrow}y[{\colon}i]$ and $B_{y^{\prime}}=\left\{z\mid\ |y^{\prime}\wedge z|\geq i\right\}={\uparrow}y^{\prime}[{\colon}i]$. By definition we have $B_{y}\cap B_{y^{\prime}}=\emptyset$, and moreover both sets $B_{y},B_{y^{\prime}}$ are regular. Up to extracting subsequences, we can assume that for all $n$, $x_{n}\in f^{-1}(B_{y})$ and $x_{n}^{\prime}\in f^{-1}(B_{y^{\prime}})$. This means that $x\in\overline{f^{-1}(B_{y})}\cap\overline{f^{-1}(B_{y^{\prime}})}$. Since $f$ is reg-preserving, and from Proposition 4.1, the set $\overline{f^{-1}(B_{y})}\cap\overline{f^{-1}(B_{y^{\prime}})}$ is regular, and non-empty. Hence there exists a regular word $z\in\overline{f^{-1}(B_{y})}\cap\overline{f^{-1}(B_{y^{\prime}})}$. Moreover, since $\mathsf{dom}(f)$ is also regular, we can choose $z$ so that $x\in\mathsf{dom}(f)\Leftrightarrow z\in\mathsf{dom}(f)$. Since $z\in\overline{f^{-1}(B_{y})}$, there is a sequence $\left(z_{n}\right)_{n\in\mathbb{N}}$ of words in $f^{-1}(B_{y})$ which converges to $z$. Furthermore, since $f^{-1}(B_{y})$ is regular and since $z$ is a regular word, we can assume, from Proposition 4.3, that the sequence $\left(z_{n}\right)_{n\in\mathbb{N}}$ is regular. Similarly, there is a regular sequence $\left(z_{n}^{\prime}\right)_{n\in\mathbb{N}}$ in $f^{-1}(B_{y^{\prime}})$ which converges to $z$.

If either sequence $\left(f(z_{n})\right)_{n\in\mathbb{N}}$ or $\left(f(z_{n}^{\prime})\right)_{n\in\mathbb{N}}$ is not convergent then we are done, because one of the pairs $(\left(z_{n}\right)_{n\in\mathbb{N}},\left(z_{n}\right)_{n\in\mathbb{N}})$ or $(\left(z_{n}^{\prime}\right)_{n\in\mathbb{N}},\left(z_{n}^{\prime}\right)_{n\in\mathbb{N}})$ is bad and of course synchronised. If both sequences are convergent, then $\lim_{n}f(z_{n})\in B_{y}$ and $\lim_{n}f(z_{n}^{\prime})\in B_{y^{\prime}}$ (because $B_{y}$ and $B_{y^{\prime}}$ are both closed), which means that $|\lim_{n}f(z_{n})\wedge\lim_{n}f(z_{n}^{\prime})|\leq i$, hence the pair $\left(\left(f(z_{n})\right)_{n\in\mathbb{N}},\left(f(z_{n}^{\prime})\right)_{n\in\mathbb{N}}\right)$ is bad.

We only have left to show that we can synchronise the sequences. Let $z_{n}=uv^{n}wt^{\omega}$ and let $z^{\prime}_{n}=u^{\prime}v^{\prime n}w^{\prime}t^{\prime\omega}$

Let us first assume that $z^{\prime}_{n}$ is constant equal to $z$. Let $z^{\prime}=u^{-1}z$, we have that $v^{n}z^{\prime}=z^{\prime}$ and $uv^{n}z^{\prime}=z$ for any $n$. Thus the pair $\left(\left(z_{n}\right)_{n\in\mathbb{N}},\left(z\right)_{n\in\mathbb{N}}\right)$ is a synchronised bad pair.

Let us now assume that neither sequence is constant, which means that $|v|,|v^{\prime}|>0$. Without loss of generality, let us assume that $|u|\geq|u^{\prime}|$, let $k\in\mathbb{N}$, let $p<|v^{\prime}|$ be such that $|u^{\prime}|+k|v^{\prime}|+p=|u|$, let $v^{\prime\prime}=v^{\prime}[p+1\colon|v^{\prime}|]v^{\prime}[1\colon p]$ and let $w^{\prime\prime}=v^{\prime}[p+1\colon|v^{\prime}|]w^{\prime}$. Then we can write $z^{\prime\prime}_{n}=z^{\prime}_{n+k+1}=u^{\prime}(v^{\prime})^{k}v^{\prime}[1\colon p]\cdot(v^{\prime\prime})^{n}\cdot w^{\prime\prime}t^{\prime\omega}=uv^{\prime\prime n}w^{\prime\prime}t^{\prime\omega}$.

Note that $v^{\omega}=v^{\prime\prime\omega}$, which means that $v^{|v^{\prime\prime}|}=v^{\prime\prime|v|}$. Let $y_{n}=z_{|v^{\prime\prime}|n}{=}uv^{|v^{\prime\prime}|n}wt^{\omega}$ and let $y^{\prime\prime}_{n}=z^{\prime\prime}_{|v|n}{=}u{v^{\prime\prime}}^{|v|n}w^{\prime}t^{\prime\omega}$. Then the pair $\left(\left(y_{n}\right)_{n\in\mathbb{N}},\left(y^{\prime\prime}_{n}\right)_{n\in\mathbb{N}}\right)$ is a synchronised bad pair at $z$.

5. Deciding Continuity and Uniform Continuity

We first show how to decide (uniform) continuity for rational and then for regular functions.

5.1. Rational case

We exhibit structural patterns which are shown to be satisfied by a one-way Büchi transducer if and only if the rational function it defines is not continuous (resp. not uniformly continuous). We express those patterns in the pattern logic defined in [FMR18, Sec. 6], which is based on existential run quantifiers of the form $\exists\pi\colon p\xrightarrow{u|v}q$ where $\pi$ is a run variable, $p,q$ are state variables and $u,v$ are word variables. Intuitively, there exists a run $\pi$ from state $p$ to state $q$ on input $u$, producing output $v$. A one-way transducer is called trim if each of its states appears in some accepting run. Any one-way Büchi transducer can be trimmed in polynomial time. The structural patterns for trim transducers are given in Figures 2 and 3. The predicate $\textsf{init}(p)$ expresses that $p$ is initial while $\textsf{acc}(p)$ expresses that it is accepting. The predicate mismatch expresses the existence of a mismatch between two words, as defined in Section 2.

Lemma 7**.**

A trim one-way Büchi transducer defines a non-continuous (resp. non-uniformly continuous) function if and only if it satisfies the formula $\phi_{\text{cont}}$ of Figure 2 (resp. the formula $\phi_{\text{u-cont}}$ of Figure 3).

Proof 5.1**.**

Showing that the patterns of Figure 2 and Figure 3 induce non-continuity and non-uniform continuity, respectively, is quite simple. Indeed, the first pattern $\phi_{\text{cont}}$ is a witness that $\left(uv^{n}wz\right)_{n\in\mathbb{N}}$ is a bad sequence at a point $uv^{\omega}$ of its domain, for $z$ a word with a final run from $r_{2}$, which entails non-continuity by Proposition 5 (if a sequence $s$ is bad then $(s,s)$ is bad). Similarly, the pattern $\phi_{\text{u-cont}}$ witnesses that the pair $\left(\left(uv^{n}wz\right)_{n\in\mathbb{N}},\left(uv^{n}w^{\prime}z^{\prime}\right)_{n\in\mathbb{N}}\right)$ is synchronised and bad (with $z,z^{\prime}$ words that have a final run from $r_{1},r_{2}$, respectively), which entails non-uniform continuity.

For the other direction, we again use Lemma 6. From a synchronised bad pair, we can find a pair of runs with a synchronised loop, such that iterating the loop does not affect the existing mismatch between the outputs of the two runs, which is in essence what the pattern formulas of Figure 2 and Figure 3 state. Let us consider the continuous case formally. The uniformly continuous case is similar. Let $f$ be a function realised by a trim transducer $T$.

Let us first show that if the pattern of $\phi_{\text{cont}}$ appears, then we can exhibit a bad pair at a point of the domain. Let us assume $\phi_{\text{cont}}$ holds. Then the word $uv^{\omega}$ is in the domain of the function realised by the transducer since it has an accepting run. Let $zt^{\omega}$ be a word accepted from state $r_{2}$, which exists by trimness, and let us consider the pair $\left(\left(uv^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{n}wzt^{\omega}\right)_{n\in\mathbb{N}}\right)$. We have $f(uv^{\omega})=u_{1}v_{1}^{\omega}$ and $u_{2}\lim_{n}f(uv^{n}wzt^{\omega})$. If $\mathsf{mismatch}(u_{1},u_{2})$ then the pair is bad, otherwise, we must have $v_{2}=\epsilon$ and thus $u_{2}w_{2}\lim_{n}f(uv^{n}wzt^{\omega})$. Since $\mathsf{mismatch}(u_{1},u_{2}w_{2})$ we again have that the pair is bad.

Let us assume that the function $f$ is not continuous at some point $x\in\mathsf{dom}(f)$. Then according to Lemma 6, there is a synchronised bad pair $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{n}w^{\prime}z^{\prime\omega}\right)_{n\in\mathbb{N}}\right)$ converging to some point of $\mathsf{dom}(f)$.

Our goal is to exhibit a pattern as in $\phi_{\text{cont}}$. If $v$ is empty, then the sequences are constant which contradicts the functionality of $T$. So both the sequences converge to $uv^{\omega}$, but their output sequences either do not converge or if converges, then not to $f(uv^{\omega})$. Because of the mismatch, either $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair or $\left(\left(uv^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{n}w^{\prime}z^{\prime\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair (or both). Without loss of generality, let $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$ be a bad pair.

Let us consider an accepting run $\rho$ of $T$ over $uv^{\omega}$. Since the run is accepting, there is an accepting state $q_{1}$ visited infinitely often. Let $l\in\left\{1,\ldots,|v|\right\}$ be such that, the state reached after reading $uv^{n}v[1{\colon}l]$ in the run $\rho$ is $q_{1}$ for infinitely many $n$s. Let $v^{\prime}=v[l+1\colon|v|]v[1\colon l]$, let $u^{\prime}=uv[1{\colon}l]$ and let $w^{\prime}=v[l+1\colon|v|]$, we have that $\left(\left(u^{\prime}v^{\prime n}w^{\prime}z^{\omega}\right)_{n\in\mathbb{N}},\left(u^{\prime}v^{\prime\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair. To simplify notations, we write this pair again as $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$. We have gained that on the run over $uv^{\omega}$, the accepting state $q_{1}$ is reached infinitely often after reading $v$ factors. Now let $k,l$ be integers such that ${p_{1}}\xrightarrow{uv^{k}}q_{1}\xrightarrow{v^{l}}q_{1}$, with $p_{1}$ an initial state. We consider $l$ different sequences, for $r\in\left\{0,\ldots,l-1\right\}$ we define the sequence $s_{r}=\left(uv^{ln+r}wz^{\omega}\right)_{n\in\mathbb{N}}$. Since $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair, there must be a value $r$ such that $\left(\left((uv^{k})(v^{l})^{n}(v^{r}w)z^{\omega}\right)_{n\in\mathbb{N}},\left((uv^{k})(v^{l})^{\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair. To simplify notations, again, we rename this pair $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$, and we know that ${p_{1}}\xrightarrow{u}q_{1}\xrightarrow{v}q_{1}$, with $p_{1}$ initial and $q_{1}$ accepting.

For any $m$ larger than the number of states $|Q|$ of $T$, let us consider the run of $T$ over $uv^{m}wz^{\omega}$. Let $i_{m},j_{m},k_{m}$ be such that we have the accepting run ${p_{m}}\xrightarrow{uv^{i_{m}}}q_{m}\xrightarrow{v^{j_{m}}}q_{m}\xrightarrow{v^{k_{m}}wz^{\omega}}$, with $i_{m}+j_{m}+k_{m}=m$ and $0<j_{m}\leq|Q|$. And let $r_{m}=i_{m}+k_{m}\mod j_{m}$. Let us consider for some $m$, the sequence $\left((uv^{r_{m}})(v^{j_{m}})^{n}(wz)^{\omega}\right)_{n\in\mathbb{N}}$. By the presence of these loops, each of these sequences has a convergent image. There is actually a finite number of such sequences, since $j_{m}$ and $r_{m}$ take bounded values. Since the original pair is bad, this means that there must exist $m$ such that the sequence $\left(f((uv^{r_{m}})(v^{j_{m}})^{n}(wz)^{\omega})\right)_{n\in\mathbb{N}}$ does not converge to $f(uv^{\omega})$. Let $u^{\prime}=uv^{i_{m}}$, $v^{\prime}=v^{j_{m}}$ and $w^{\prime}=v^{k_{m}}w$, then $\left(\left(u^{\prime}v^{\prime n}w^{\prime}z^{\omega}\right)_{n\in\mathbb{N}},\left(u^{\prime}v^{\prime\omega}\right)_{n\in\mathbb{N}}\right)$ is a bad pair. Once again we rename the pair $\left(\left(uv^{n}wz^{\omega}\right)_{n\in\mathbb{N}},\left(uv^{\omega}\right)_{n\in\mathbb{N}}\right)$ and now we have both ${p_{1}}\xrightarrow{u}q_{1}\xrightarrow{v}q_{1}$ and ${p_{2}}\xrightarrow{u}q_{2}\xrightarrow{v}q_{2}$, such that $p_{1},p_{2}$ are initial, $q_{1}$ is accepting and $wz^{\omega}$ has a final run from $q_{2}$.

Now we have established the shape of the pattern, we only have left to show the mismatch properties.

[TABLE]

Let us first assume that $v_{2}\neq\epsilon$. Then $\lim_{n}f(uv^{n}wz^{\omega})=u_{2}v_{2}^{\omega}$. Since the pair is bad, there exists $k$ such that $\mathsf{mismatch}(u_{1}v_{1}^{k},u_{2}v_{2}^{k})$. Hence, up to taking $u^{\prime}=uv^{k}$, we have established the pattern:

[TABLE]

Let us now assume that $v_{2}=\epsilon$. Then $\lim_{n}f(uv^{n}wz^{\omega})=u_{2}y_{2}$. Then there is a prefix $w_{2}$ of $y_{2}$ and an integer $k$ such that $\mathsf{mismatch}(u_{1}v_{1}^{k},u_{2}w_{2})$. Hence, up to taking $u^{\prime}=uv^{k}$, and $w^{\prime}$ a sufficiently long prefix of $wz^{\omega}$ we have established the pattern:

[TABLE]

which concludes the proof.

Theorem 8**.**

Deciding if a one way Büchi transducer defines a continuous (resp. uniformly continuous) function can be done in NLogSpace.

Proof 5.2**.**

Let $T$ be a one way Büchi transducer defining a function $f$. From Lemma 7, if $T$ is trim, non-continuity of $f$ is equivalent to $T$ satisfying the formula $\phi_{cont}$ of Figure 2. This formula is expressed in the syntax of the pattern logic from [FMR18], where it is proved that model-checking pattern formulas against transducers can be done in NLogSpace [FMR18, Thm. 6]. This yields the result.

If $T$ is not trim, then we modify the formula $\phi_{cont}$ to additionally express that there must be some accepting run from $r_{2}$ on some input. Equivalently, we express that there exists a run from $r_{2}$ to some accepting state $s$, and a run looping in $s$, in the following way: we just add the quantifiers $\exists\pi_{3}\colon r_{2}\xrightarrow{\alpha\mid\beta}s\ \exists\pi_{4}\colon s\xrightarrow{\gamma\mid\tau}s$ to $\phi_{cont}$ and the constraint $\textsf{acc}(s)$ which requires $s$ to be accepting.

The proof for non-uniform continuity, using formula $\phi_{\text{u-cont}}$ is similar.

5.2. Regular case

As for the rational case, we first define a pattern which is satisfied by a 2DFTpla if and only if it defines a non-continuous function. Then we show how to check for the existence of this pattern. It is however more intricate than in the rational setting. First, we get rid of the look-ahead by working on words annotated with look-ahead information. We now make this notion formal.

5.2.1. Look-ahead removal and annotated words

Let $f$ be realized by a 2DFTpla $\mathcal{T}$ over alphabet $\Sigma$ with look-ahead automaton $P$. Let $Q_{P}$ be the states of $P$. We define $\widetilde{\mathcal{T}}$, a 2DBT over $\Sigma\times Q_{P}$ which, informally, simulates $\mathcal{T}$ over words annotated with look-ahead states, and which accepts only words with a correct look-ahead annotation with respect to $P$. Formally, for an annotated word $u\in(\Sigma\times Q_{P})^{\infty}$, we denote by $\pi_{\Sigma}(u)\in\Sigma^{\infty}$ its projection on $\Sigma$. An annotated word $x\in(\Sigma\times Q_{P})^{\omega}$ is well-labelled if $\pi_{Q_{P}}(u)$ is the accepting run of $P$ over $u$.

As $P$ is prophetic, for all words $u\in\mathsf{dom}(f)$, there exists a unique well-annotated word, denoted $\tilde{u}$, which satisfies $\pi_{\Sigma}(\tilde{u})=u$. We now let $\tilde{f}$ be the function defined, for all $u\in\mathsf{dom}(f)$, by $\tilde{f}(\tilde{u})=f(u)$. The function $\tilde{f}$ is easily seen to be definable by a 2DBT which simulates $\mathcal{T}$ over the $\Sigma$-component of the input word and simulates $P$ over the $Q_{P}$-component of the input word to check that the annotation is correct.

Proposition 9**.**

One can construct, in linear-time, a 2DBT denoted $\widetilde{T}$ which realises the function $\tilde{f}$.

5.2.2. Transition monoid of 2DBT

In our pattern, we will be using the notion of transition monoid of a 2DBT, as the transition monoid of its underlying two-way automaton (obtained by ignoring the output words on transitions).

Let $T$ be a 2DBT, we define its transition monoid $M_{T}$ in the usual way (see e.g. [BGMP18] for details), but we also add information telling us if a word produces empty output or not. The set $M_{T}$ contains functions $Q\times\left\{L,R\right\}\rightarrow Q\times\left\{L,R\right\}\times\left\{0,1\right\}$. Informally, the transition morphism of $T$, $\phi_{T}\colon\Sigma^{*}\rightarrow M_{T}$ sends a word $u$ to the function mapping e.g. $(p,L)$ to $(q,R,1)$ if there exists a run of $T$ on $u$ which enters $u$ from the left in state $p$, stays within the inner positions of $u$ until it exits $u$ from the right in state $q$, and $T$ has produced a non-empty output. This run is called a left-to-right traversal (LR-traversal for short). Left-to-left (LL-), right-to-right (RR-) and right-to-left (RL-) traversals are defined similarly. For instance a run from $p$ to $q$ is an LL-traversal on $u$, if it enters $u$ from the left in state $p$, stays within the inner positions of $u$, until it exists $u$ from the left in state $q$. If this run did not produce any output, then $\phi_{T}(u)$ contains the function mapping $(p,L)$ to $(q,L,0)$.

The transition monoid of a two-way automaton is defined similarly, except that the information on whether there is a production of non-empty output or not is not required, i.e. it is a set of functions of type $Q\times\left\{L,R\right\}\rightarrow Q\times\left\{L,R\right\}$.

5.2.3. Critical Pattern

Let $\mathcal{T}$ be a 2DFTpla and $\widetilde{T}$ be its associated 2DBT running over annotated words (see Section 5.2.1). Let $\rho=(q_{0},i_{0}=0)\stackrel{{\scriptstyle b_{i_{0}}/\gamma_{1}}}{{\longrightarrow}}(q_{1},i_{1})\stackrel{{\scriptstyle b_{i_{1}}/\gamma_{2}}}{{\longrightarrow}}\cdots(q_{n},i_{n}=l)$ be an initial run of $\widetilde{T}$ over a finite word $uvw$. We say that the factor $v$ is non-producing in $\rho$ if all the transitions occurring within $v$ output $\epsilon$. Otherwise $v$ is producing. Formally, if in all the transitions $(q_{j},i_{j})\stackrel{{\scriptstyle b_{i_{j}}/\gamma_{j}}}{{\longrightarrow}}(q_{j+1},i_{j+1})$ in run $\rho$ such that $|u|\leq i_{j}<|uv|$ and $\gamma_{j}=\epsilon$, then $v$ is non-producing.

We define the notion of critical pattern for the 2DBT $\widetilde{T}$. We say that $\widetilde{T}$ admits a critical pattern if there are words $u,v\in\Sigma^{*}$, $u_{1},v_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2}\in(\Sigma\times Q_{P})^{*}$ such that

1. (1)

$\pi_{\Sigma}(u_{1})=\pi_{\Sigma}(u_{2})=u$, $\pi_{\Sigma}(v_{1})=\pi_{\Sigma}(v_{2})=v$, 2. (2)

$v_{1}$ and $v_{2}$ are idempotent444$\phi_{\widetilde{T}}(v_{i})=\phi_{\widetilde{T}}(v_{i}v_{i})$ for $i\in\left\{1,2\right\}$ with respect to the transition monoid of $\widetilde{T}$, 3. (3)

there exist two accepting runs of $\widetilde{T}$ on $u_{1}v_{1}w_{1}z_{1}^{\omega}$ and $u_{2}v_{2}w_{2}z_{2}^{\omega}$ which can be respectively decomposed into $\rho_{1}\lambda_{1}$ and $\rho_{2}\lambda_{2}$ such that for all $i=1,2$, 4. (4)

$\rho_{i}$ is over $u_{i}v_{i}w_{i}$ and does not end in $v_{i}$, 5. (5)

$v_{i}$ is not producing in $\rho_{i}$, 6. (6)

there is a mismatch between $\mathsf{out}(\rho_{1})$ and $\mathsf{out}(\rho_{2})$.

We give the following characterisation of continuity and uniform continuity. Note that the patterns are similar to the one-way case.

Proposition 10**.**

Let $T$ be a 2DFTpla realising a function $f$. Then the following holds:

1. (1)

$f$* is not uniformly continuous (resp. continuous).* 2. (2)

the 2DBT $\tilde{T}$ admits a critical pattern $u_{1},u_{2},v_{1},v_{2},w_{1},z_{1},w_{2},z_{2},\rho_{1},\lambda_{1},$ $\rho_{2},\lambda_{2}$ (resp. and $\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$)

Proof 5.3**.**

We will show that the existence of a critical pattern is equivalent to the existence of a synchronised bad pair. From Proposition 5 this will conclude the proof.

Let us first assume that we have a critical pattern $u_{1},u_{2},v_{1},v_{2},w_{1},z_{1},w_{2},z_{2},\rho_{1},\lambda_{1},\rho_{2},\lambda_{2}$. Our goal is to prove that $\left(\left(\pi_{\Sigma}(u_{1}v_{1}^{n}w_{1}z_{1}^{\omega})\right)_{n},\left(\pi_{\Sigma}(u_{2}v_{2}^{n}w_{2}z_{2}^{\omega})\right)_{n}\right)$ is a bad pair. We define $\rho_{1}^{n},\rho_{2}^{n}$ the runs obtained from $\rho_{1},\rho_{2}$, just by iterating the respective $v_{1},v_{2}$ factors $n$ times. Since $v_{1},v_{2}$ are idempotents, reading $v_{i}$ or $v_{i}^{n}$ does not change the shape of the run $\rho_{i}$, nor the order of the outputs occurring outside of $v_{i}$. Moreover, since $v_{i}$ is non-producing in both runs, the outputs over $v_{i}$ and $v_{i}^{n}$ are also the same. Hence we get $\mathsf{out}(\rho_{1})=\mathsf{out}(\rho_{1}^{n})$ and $\mathsf{out}(\rho_{2})=\mathsf{out}(\rho_{2}^{n})$. Thus the runs $\rho_{1}^{n}\lambda_{1}^{n}$ and $\rho_{2}^{n}\lambda_{2}^{n}$ produce outputs which mismatch at a position smaller than $\max(|\rho_{1}|,|\rho_{2}|)$ and the pair $\left(\left(\pi_{\Sigma}(u_{1}v_{1}^{n}w_{1}z_{1}^{\omega})\right)_{n},\left(\pi_{\Sigma}(u_{2}v_{2}^{n}w_{2}z_{2}^{\omega})\right)_{n}\right)$ is indeed bad.

Conversely, let us assume that $\left(\left(uv^{n}x_{1}y_{1}^{\omega}\right)_{n},\left(uv^{n}x_{2}y_{2}^{\omega}\right)_{n}\right)$ is a bad pair. Up to extracting subsequences, we can assume that $v,y_{1},y_{2}$ are idempotent both for $T$ and its look-ahead automaton. Thus we can obtain, up to taking a larger word $u$, a synchronised bad pair of the form $\left(\left(\pi_{\Sigma}(u_{1}v_{1}^{n}w_{1}z_{1}^{\omega})\right)_{n},\left(\pi_{\Sigma}(u_{2}v_{2}^{n}w_{2}z_{2}^{\omega})\right)_{n}\right)$ with $\pi_{\Sigma}(u_{1})=\pi_{\Sigma}(u_{2})=u$ and $\pi_{\Sigma}(v_{1})=\pi_{\Sigma}(v_{2})=v$. We also write $\pi_{\Sigma}(w_{i})=x_{i}$ and $\pi_{\Sigma}(z_{i})=y_{i}$ for $i\in\left\{1,2\right\}$. Since the pair is bad there exists $i$ such that for any $m$, there exists $n\geq m$ with $|f(uv^{n}x_{1}y_{1}^{\omega})\wedge f(uv^{n}x_{2}y_{2}^{\omega})|\leq i$. Let $n$ be larger than $2i+2$ with $|f(uv^{n}x_{1}y_{1}^{\omega})\wedge f(uv^{n}x_{2}y_{2}^{\omega})|=j\leq i$. Let $\rho_{1}$ (resp. $\rho_{2}$) be the prefix of the run over $u_{1}v_{1}^{n}w_{1}z_{1}^{\omega}$ (resp. $u_{2}v_{2}^{n}w_{2}z_{2}^{\omega}$) which stops after producing the $j$th output. We make the following claim with respect to the sequence $u_{1}v_{1}^{i+1}v_{1}^{k}v_{1}^{i+1}w_{1}z_{1}^{\omega}$:

Claim 11**.**

Any transition of $\rho_{1}$ occurring within the factor $v_{1}^{k}$ must produce empty outputs and $\rho_{1}$ ends outside of this factor.

If we assume that the claim is true, then it is similarly true for $\rho_{2}$. Then we obtain a critical pattern $u_{1}v_{1}^{i+1},u_{2}v_{2}^{i+1},v_{1}^{k},v_{2}^{k},v_{1}^{i+1}w_{1},z_{1},v_{1}^{i+1}w_{2},z_{2},\rho_{1},\lambda_{1},\rho_{2},\lambda_{2}$.

We only have left to show that the claim holds.

Proof 5.4** (Proof of Claim 11).**

Let us assume towards a contradiction that a transition occurring within $v_{1}^{k}$ in $\rho_{1}$ has non-empty output. Let $\rho_{1}^{\prime}$ the shortest prefix of the run $\lambda$ over $u_{1}v_{1}^{i+1}v_{1}^{k}v_{1}^{i+1}w_{1}z1^{\omega}$ which extends $\rho_{1}$ and ends outside of the $v_{1}^{k}$ factor. Note that if $\rho_{1}$ already ends outside of this factor, $\rho_{1}^{\prime}=\rho_{1}$. Let $\rho$ be a factor of $\rho_{1}^{\prime}$ which contains such a producing transition and which starts and ends at a boundary of the $v_{1}^{k}$ factor without leaving it.

Since $\tilde{T}$ is deterministic and since $v_{1}$ is idempotent, all $v_{1}$ factors (except possibly for the first and last ones) must also produce such a non-empty output in $\lambda$. These outputs must occur in $\lambda$ either in increasing or decreasing order with respect to the order of the input word. If they occur in increasing order, the first ${i+1}$ $v_{1}$ factors produce non-empty outputs within $\rho_{1}$, which contradicts the assumption that $|\mathsf{out}(\rho_{1})|\leq i$. Similarly if the outputs occur in decreasing order then the last ${i+1}$ $v_{1}$ factors produce non-empty outputs within $\rho_{1}$, which also yields a contradiction, hence we obtain that the claim must hold.

This proves 10.

5.2.4. Deciding uniform continuity and continuity for regular

functions

We now show how to decide, in PSpace, whether a given 2DFTpla defines a uniform continuous function by checking whether its associated 2DBT over annoted words admits a critical pattern. Deciding continuity is based on the same ideas and shown in the last paragraph of this section. We reduce the problem to checking the emptiness of a non-deterministic two-way Parikh automaton [Iba14]. A two-way Parikh automaton (2PA) $\mathcal{P}$ of dimension $d$ is a two-way automaton, running on finite words, extended with vectors of integers (including [math]) of dimension $d$. Each dimension can be seen as a counter which can only be incremented. A run on a finite word is accepting if it reaches some accepting state and the (pairwise) sum of the vectors met along the transitions belong to some given semi-linear set represented as some existential Presburger formula555We recall that existential Presburger formulas are existentially quantified first-order formulas over the predicate $t_{1}\leq t_{2}$ where $t_{i}$ are terms over the constants $0,1$ and the addition $+$.. The emptiness problem for 2PA is undecidable but decidable in PSpace for bounded-visit 2PA [FGM19]. A 2PA is bounded visit if there exists some $k$ such that in any accepting run of $\mathcal{P}$, any input position is visited at most $k$ times by that run. The 2PA we construct will be of polynomial size and bounded-visit, entailing PSpace decidability of uniform continuity for 2DFTpla, following Proposition 9.

Lemma 12**.**

Given a 2DFTpla $T$, one can construct in polynomial time a bounded-visit 2PA $\mathcal{P}_{T}$ (of polynomial size) such that $L(\mathcal{P}_{T})\neq\emptyset$ if and only if $\widetilde{T}$ admits a critical pattern.

Before proving the lemma, let us state our main result.

Theorem 13**.**

Deciding whether a regular function given as a deterministic two-way transducer with prophetic Büchi look-ahead is uniformly continuous is PSpace-Complete. Hardness also holds for continuity.

Proof 5.5**.**

The upper-bound is a direct consequence of Proposition 9, Lemma 12, and the PSpace upper-bound of [FGM19] for the non-emptiness of bounded-visit two-way Parikh automata.

*The lower-bound is easily obtained by reducing the problem of checking the non-emptiness of the language of a deterministic two-way automaton over finite words, which is known to be PSpace-hard666This is a folklore result, easily obtained by reducing the PSpace-hard problem of checking the non-emptiness of the intersection of the languages of $n$ DFA, each pass of the two-way automaton over the whole input simulates one pass of each DFA.. Given a deterministic two-way automaton $A$ on finite words over some alphabet $\Sigma$ containing at least two letters $a$ and $b$, we construct a 2DFTpla $T$ defining the following function $f$. It is defined on all $\omega$-words $u$ in $(\Sigma\cup\{\#\})^{\omega}$ by $f(u)=a^{\omega}$ if $u=v\#w$ for some $v\in L(A)$ and $w$ contains infinitely many $a$, otherwise by $f(u)=b^{\omega}$. Clearly, if $L(A)$ is empty, then $f$ is the constant function mapping any word to $b^{\omega}$ and is therefore uniformly continuous (and continuous). Conversely, if there exists some $v\in L(A)$, then we claim that $f$ is not continuous (and hence not uniformly continuous). Indeed, consider the family of words $u_{n}=v\#a^{n}\#^{\omega}$ for all $n\geq 0$ and some $a\in\Sigma$. Clearly, $f(u_{n})=b^{\omega}$ for all $n$ as $u_{n}$ contains finitely many $a$. However $f(\lim_{n\rightarrow\infty}u_{n})=f(v\#a^{\omega})=a^{\omega}$, which is different from $\lim_{n\rightarrow\infty}f(u_{n})=b^{\omega}$. Finally, it remains to show how to construct $T$ from $A$. The idea is to use a look-ahead to check whether the input is of the form $v\#w$ where $v\in\Sigma^{*}$ and $w$ contains infinitely many $a$. If that is the case, then $T$ simulates $A$ on $v$ (using $\#$ as an endmarker). At the end of this simulation, if $A$ reaches an accepting state, then $T$ reads $w$ and keeps on producing $a$. On the other hand, if $A$ reaches a non-accepting state, then $T$ keeps on producing $b$ on the $w$ part. If the look-ahead has failed (meaning that the input is not of the above form), then $T$ keeps on producing $b$ while reading its input in a one-way fashion. *

We now proceed to the proof of Lemma 12.

Encoding of the set of critical patterns as a language

We show how to encode the set of critical patterns as the language of a 2PA. To that end, let us see how a critical pattern can be encoded as a word. The 2PA will have to check properties $(1)-(6)$ of the definition of a critical pattern. The first condition is about projections. To check that $u_{1},u_{2}$ project on the same $\Sigma$-word, as well as $v_{1},v_{2}$, we just encode them as words over the alphabet $\Sigma\times Q_{P}\times Q_{P}$. Let us make this more formal. Let $\#$ be a fresh symbol. For any two alphabets $A,B$ and any two words $w_{1}\in A^{*}$ and $w_{2}\in B^{*}$ of same length, we let $w_{1}\otimes w_{2}\in(A\times B)^{*}$ be their convolution, defined by $(w_{1}\otimes w_{2})[i]=(w_{1}[i],w_{2}[i])$ for any position $i$ of $w_{1}$.

We now define a language $\text{Crit}_{\mathcal{T}}\leavevmode\nobreak\ {\subseteq}\leavevmode\nobreak\ \vdash((\Sigma\times Q_{P}^{2})^{*}\#)^{2}((\Sigma\times Q_{P})^{*}\#)^{4}\dashv$ which consists of words of the form $w\leavevmode\nobreak\ {=}\leavevmode\nobreak\ \vdash(u\otimes a_{1}\otimes a_{2})\#(v\otimes b_{1}\otimes b_{2})\#w_{1}\#z_{1}\#w_{2}\#z_{2}\#\dashv$ where, if $u_{i}=u\otimes a_{i}$ and $v_{i}=u\otimes b_{i}$, then $u_{1},v_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2}$ is a critical pattern.

The following proposition is immediate

Proposition 14**.**

$\mathcal{T}$* admits a critical pattern if and only if $\text{Crit}_{\mathcal{T}}\neq\emptyset$.*

Note that this encoding makes sure condition $(1)$ of the definition of critical pattern is ensured, but the other properties will have to be checked by the $2\textsf{PA}$.

Checking idempotency with a succinct two-way automaton

The 2PA has to check condition $(2)$ of the critical patterns, i.e. idempotency with respect the transition monoid of the 2DBT $\widetilde{T}$. We show more generally, given a deterministic two-way automaton $A$, how a two-way automaton of polynomial size can recognise idempotent words with respect to the transition monoid of $A$. The proof of this result is not needed to understand the proof of the main lemma (Lemma 17), namely that the set $\text{Crit}_{\mathcal{T}}$ is recognisable by a 2PA, and can be skipped in a first reading.

Lemma 15**.**

For any deterministic two-way automaton $A$ (resp. deterministic two-way Büchi transducer $T$), one can construct in polynomial time a (bounded-visit) deterministic two-way automaton $I_{A}$ which recognises the set of words $\#u\#$ such that $u$ is idempotent with respect to $A$, and $\#$ is a fresh symbol.

Proof 5.6**.**

We prove the result for automata. Its adaptation to transducers is trivial, as the transition monoid of a transducer is the same as the transition monoid of its underlying automaton obtained by ignoring the outputs, without the information on whether some non-empty output is produced or not by a traversal. The following construction, done for automata, can be trivially adapted to account for this information.

Let $Q$ be the set of states of $A$. Without loss of generality, we can assume that $Q=\{1,\dots,n\}$. Let $(i,j)\in Q^{2}$. We explain how a two-way automaton $A_{i,j}^{LR}$ can check whether $(i,j)$ is is left-to-right traversal of $u$: it needs to start from the left of $u$ in state $i$, and simulates $A$ until it reaches a boundary of $u$: if it is the left boundary, it rejects, if it the right boundary, it accepts. Now, let us explain how a two-way automaton $B_{i,j}^{L,R}$ can check whether $(i,j)$ is a left-to-right traversal of $A$ over $uu$, by reading only $\#u\#$. Intuitively, the main idea is to simulate $A$ and when $A$ wants to go to the right of $u$ following some transition $t$, then $B_{i,j}^{L,R}$ comes back to the left of $u$ and applies $t$ and proceeds with its simulation of $A$. More precisely, $B_{i,j}^{L,R}$ has two modes: $M_{1}$ and $M_{2}$. It stays in mode $M_{1}$ as long as $A$ does not cross the right boundary of $u$ or crosses the left boundary (in which case it stops its computation in a non-accepting state). As soon as it crosses the right boundary, using some transition $t$, $B_{i,j}^{L,R}$ moves to mode $M_{2}$, comes back to the left of $u$, and applies $t$. It then simulates $A$ until it reaches the right boundary in state $j$ in which case it stops its computation and accepts, or it reaches the left boundary in which case it stops its computation and rejects.

Note that in the above constructions, $A_{i,j}^{LR}$ and $B_{i,j}^{LR}$ are both deterministic, since $A$ is deterministic. Therefore, they have bounded crossing. Moreover, they have a polynomial number of states. We construct in a similar way automata for each type of traversals (LR, RL, LL, RR) and each pair $(i,j)$.

Then, clearly, $u$ is idempotent if and only if the following holds

[TABLE]

Since the automata are deterministic, they can be complemented in polynomial time. Moreover, intersection of two-way automata can be done in linear time by serial composition: the first automaton is simulated and if it eventually accepts, then the other automaton is simulated and must accept as well. Using these results, one can construct in polynomial time a deterministic two-way automaton implementing the conjunction above, concluding the proof.

Checking acceptance of lasso words by a succinct two-way

automaton over finite words

We prove a useful technical lemma, which intuitively says that it is possible to construct a two-way automaton of polynomial size accepting words of the form $u\#v$ such that $uv^{\omega}$ is accepted by a given Büchi two-way automaton $A$ and $v$ is idempotent with respect to the transition monoid of $A$. The statement of the lemma is slightly more general. The proof of this lemma is not needed to understand the proof of the main lemma, namely that the set $\text{Crit}_{\mathcal{T}}$ is recognisable by a 2PA, and can be skipped in a first reading.

A marked word over an alphabet $\Sigma$ is an $\omega$-word over $\Sigma\times\{0,1\}$ which contains exactly one occurrence of $1$. Given $i\geq 1$ and $x\in\Sigma^{\omega}$, we denote by $x\triangleright i$ the marked word such that for all $j\geq 1$, $(x\triangleright i)[j]=(x[j],0)$ if $j\neq i$ and $(x\triangleright i)[j]=(x[j],1)$ otherwise.

Lemma 16**.**

Let $A$ be a non-deterministic (bounded-visit) two-way automaton over an alphabet $\Sigma$, $\#\not\in\Sigma$ and $q$ be a state of $A$. Let $L_{q}$ be the language of words $({\vdash}u\#v{\dashv})\triangleright i$ such that $u,v\in\Sigma^{*}$, $2\leq i\leq|u|+1$, $v$ is idempotent with respect to the transition monoid of $A$, and there exists an accepting run of $A$ on $uv^{\omega}$ starting in configuration $(q,i)$. Then, $L_{q}$ is recognisable by a non-deterministic bounded-visit two-way automaton of polynomial size (in $A$).

Proof 5.7**.**

We define a two-way automaton $P$ recognising $L_{q}$. The symbol $\#$ is needed to identify the left boundary of $v$. First, $P$ checks that the input is valid, i.e. it is of the form $({\vdash}u\#v{\dashv})\triangleright i$ such that $2\leq i\leq|u|+1$ and $v$ is idempotent with respect to the transition monoid of $A$. To check idempotency, we rely on the construction of Lemma 15.

If the validity checking succeeds, $P$ comes back to the initial position of its input and check the existence of an accepting run as required by the statement of the lemma. Since this accepting run is on $uv^{\omega}$ and $P$ can only read one occurrence of $v$, we first give a characterisation of such an accepting run which will turn useful to check its existence while accessing only one iteration of $v$. This characterisation intuitively says that there is an accepting loop on some finite iteration $v^{\kappa}$ accessible from the marked position $i$ in state $q$. More precisely, it can be seen that any accepting run $r$ of $A$ on $uv^{\omega}$ starting in configuration $(q,i)$ can be decomposed as:

[TABLE]

where:

1. (1)

$n$* is smaller than the number of states of $A$* 2. (2)

$\rho_{0}$* is a run on $u$ from configuration $(q,i)$ to some configuration $(q_{1},|u|+1)$* 3. (3)

for all $1\leq j\leq n$, $L_{j}$ is a left-to-left traversal on $v^{\omega}$ starting in some configuration $(q_{j},|u|+1)$ and ending in some configuration $(p_{j},|u|)$ 4. (4)

for all $1\leq j\leq n$, $R_{j}$ is a right-to-right traversal on $u$ starting in configuration $(p_{j},|u|)$ and ending in some configuration $(q_{j},|u|+1)$ 5. (5)

$\rho_{1}$* is a finite run visiting only positions of $v^{\omega}$ from configuration $(q_{n},|u|+1)$ to some configuration $(p,j_{1})$ such that $j_{1}=|u|+|v|.m+1$ for some $m$ (i.e. $j_{1}$ is the initial position of some iteration of $v$)* 6. (6)

$\ell$* is a finite run visiting only positions of $v^{\omega}$ from configuration $(p,j_{1})$ to some configuration $(p,j_{2})$ such that $j_{2}=j_{1}+|v|m$ for some $m\geq 1$ (i.e. $j_{2}$ is the initial position of some iteration of $v$, and is at the right of $j_{1}$)*

In the above characterisation, note that $L_{j},R_{j}$ are either LL- or RR-traversal starting at the right boundary of $u$. Since $r$ is accepting, it visits the whole infinite input $uv^{\omega}$ and therefore there cannot be more such traversals than the number of states. Otherwise, this boundary would be visited twice in the same state by $A$, and therefore, it would be visited infinitely many times, contradicting that the whole input is read. This justifies why we can take $n$ smaller than the number of states.

This characterisation is not directly exploitable by $P$. We make the following observation: since $v$ is idempotent, $L_{j}$ is a left-to-left traversal on $vv$ for all $1\leq j\leq n$. Indeed, suppose that is not the case, it means that $L_{j}$ visits all positions of $v^{2}\sigma$ at least once, where $\sigma$ is the first symbol of $v$. Let $s_{1}$ be the state of $L_{j}$ the first time it reaches the end of $v$, and $s_{2}$ be the state of $L_{j}$ the first time it reaches the end of $vv$. In other words, there is a left-to-right traversal from $q_{j}$ to $s_{1}$ on $v$ and a left-to-right traversal from $q_{j}$ to $s_{2}$ on $vv$. Since $v$ is idempotent, we get that $s_{1}=s_{2}$. This contradicts that $L_{j}$ is a left-to-right traversal, since $A$ then loops on $s_{1}=s_{2}$ and moves forever to the right when initially starting to read $v^{\omega}$ on state $q_{j}$. This means that to check the existence of a left-to-left traversal on $v^{\omega}$, one only needs to consider two iterations of $v$.

We now proceed to the construction of $P$. The automaton $P$ guesses a decomposition as in the above characterisation by simulating $A$. The main difficulty is that it reads only one occurrence of $v$ while $A$ must be simulated on $uv^{\omega}$. Let us first explain how the decomposition can be guessed. First, $P$ accesses the marked position $i$ and start simulating $A$ from state $q$ (ignoring the marking in $\{0,1\}$ since $A$ is over alphabet $\Sigma$). If eventually $A$ reaches the right boundary of $u$ in some state $q_{1}$, $P$ guesses some state $p_{1}$ and checks whether there exists a left-to-left traversal $L_{1}$ of $A$, from $q_{1}$ to some $p_{1}$, on $v^{\omega}$ (we explain later how this verification can be done by $P$). If it is the case, $P$ again simulates $A$ on $u$ and if eventually $A$ reaches the right boundary of $u$ in some state $q_{2}$, once again, $P$ checks whether there exists a left-to-left traversal of $v^{\omega}$ from $q_{2}$ to some $p_{2}$, and so on for at most $n$ times. Non-deterministically, when $P$ reaches the right boundary of $u$, it can decide to check for the existence of an accessible accepting loop in $v^{\omega}$, i.e. runs $\rho_{1}$ and $\ell$ as in the above characterisation (we also explain later how this verification can be done by $P$). If such a loop is found, $P$ accepts.

Let us now explain how the two verifications involved in the latter simulation can be done by $P$, namely: checking the existence of a left-to-left traversal on $v^{\omega}$ from some state, say $s$, and checking the existence of an accessible accepting loop. The main difficulty is that $P$ has access to only one occurrence of $v$, but it can use two-wayness to overcome this problem. If $A$ needs to cross the right boundary of $v$ from the left (i.e. access the next iteration of $v$), $P$ just rewinds its reading head to the first position of $v$, and if $A$ needs to cross the left boundary of $v$ from the right (i.e. access the previous iteration of $v$), then $P$ moves its reading head to the last position of $v$. We call this simulation a simulation modulo. We use this idea of simulation modulo to check the existence of LL-traversals as well as $\rho_{1}$ and $\ell$.

For LL-traversals, as explained before, one only needs to check the existence of an LL-traversal on $vv$. $P$ therefore performs a simulation of $A$ modulo and uses a bit of information to check whether it is in the first or second occurrence of $v$.

To check the existence of $\rho_{1}$, we can use similar arguments as before, based on the fact that $v$ is idempotent, to prove that $\rho_{1}$ only visits the two first iterations of $v$. This is due to the fact that $\rho_{1}$ can be decomposed into a sequence of traversals on some powers of $v$ but each of those traversal is a traversal on $v$ by idempotency. For example, $\rho_{1}$ might be an LR-traversal on $v^{\kappa_{1}}$ followed by a LL-traversal on $v^{\kappa_{2}}$, followed by a RR-traversal on $v^{\kappa_{3}}$, up to reaching configuration $(p,j_{1})$. However by idempotency, each of these traversals are actually traversals on $v$, so, $\kappa_{j}=1$ for all $j$. Hence, only two iterations of $v$ are needed (two and not one, because, for instance, an LR-traversal on $v$ can be followed by a LL-traversal on $v$, and hence two iterations are needed). Since two iterations of $v$ are needed, $P$ can check the existence of $\rho_{1}$ using some simulation modulo and one bit of information.

Finally, it remains for $P$ to check for the existence of a loop visiting an accepting state. Using idempotency of $v$ and similar arguments as before, it can be shown that such a loop can be found only on three iterations of $v$, i.e. on $v^{3}$. So, once again, $P$ can perform a simulation modulo, and use two bits of information to check whether it is on the first, second or third copy of $v$.

Note that since $A$ is bounded-visit, and since $P$ only performs simulations of $A$ on up to three iterations of $v$, it is bounded visit as well.

Construction of the 2PA

We now have all the ingredients to construct a 2PA whose language is non-empty if and only if $\mathcal{T}$ admits a critical pattern. More precisely, we show the following:

Lemma 17**.**

The language $\text{Crit}_{\mathcal{T}}$ is recognisable by a 2PA $C$ of polynomial size (in $\mathcal{T}$).

Proof 5.8**.**

We do not give a formal construction of $C$, which would be unnecessarily too technical. Instead, we explain how $C$ can check the six conditions $(1)-(6)$ of the definition of a critical pattern when reading valid encodings. The dimension of $C$ is $2$ (i.e. its vectors are in $\mathbb{N}^{2}$ or equivalently, it has two incrementing counters). We say that the counters are unchanged by a transition if the vector on that transition is $(0,0)$.

First $C$ checks, by doing a left-to-right pass on the whole input $w$, whether $w$ is a valid encoding, i.e. whether $w\in{\vdash}((\Sigma\times Q_{P}^{2})^{*}\#)^{2}((\Sigma\times Q_{P})^{*}\#)^{4}{\dashv}$. If this is the case, then $C$ comes back to the beginning of $u$ and proceed by checking other properties, otherwise it rejects. Note that this first verification only needs a constant number of states. During this phase, counters are unchanged.

Let us now assume that $C$ has validated the type of its input $w$, which is then of the form $w={\vdash}(u\otimes a_{1}\otimes a_{2})\#(v\otimes b_{1}\otimes b_{2})\#w_{1}\#z_{1}\#w_{2}\#z_{2}\#{\dashv}$. Let $u_{i}=u\otimes a_{i}$ and $v_{i}=v\otimes v_{i}$. Note that $C$ can navigate between each $\#$-free factors of $w$ by just keeping in its state whether it is in the first, second, up to sixth factor. This information can be updated when the separator $\#$ is met and is polynomial. The second observation is that condition $(1)$ ($u_{1}$ and $u_{2}$ projects on the same $\Sigma$-word, as well as $v_{1}$ and $v_{2}$) is necessarily satisfied by definition of the encoding.

Let us explain how $C$ checks condition $(2)$ about idempotency of $v_{1}$ and $v_{2}$. We rely on the construction of Lemma 15 applied to the 2DBT $\widetilde{\mathcal{T}}$ where outputs are ignored (therefore, it is a deterministic two-way automaton). If this second phase accepts, $C$ proceeds to checking conditions $(3)-(6)$. Otherwise it rejects. Again, during this verification, counters are unchanged.

We now turn to conditions $(3)-(6)$. The 2PA $C$ first constructs a finite run $\rho_{1}$ on $u_{1}v_{1}w_{1}$ which does not end in $v_{1}$. Since $\rho_{1}$ is existentially quantified in the definition of critical patterns, this is where non-determinism of $C$ is needed. To do so, $C$ simulates $\widetilde{\mathcal{T}}$ on $u_{1}v_{1}w_{1}$. More precisely, it reads $\vdash(u\otimes a_{1}\otimes a_{2})\#(v\otimes b_{1}\otimes b_{2})\#w_{1}\#$ but ignores the third components $a_{2}$ and $b_{2}$ as well as the $\#$ symbols. During this simulation, outputs of $\mathcal{T}$ are also ignored. If $\mathcal{T}$ wants to cross the left boundary of $w_{1}$, then $C$ rejects, otherwise condition $(4)$ is not satisfied. If $\mathcal{T}$ is in $v_{1}$ but produces a non-empty output, then $C$ rejects as well, ensuring condition $(5)$. Non-deterministically, $C$ decides to stop the simulation, but only if $\mathcal{T}$ is not in $v_{1}$ (otherwise, this would violate condition $(4)$). If it does not stop the simulation, then $C$ will never accept its input. Stopping the simulation means that $C$ has constructed a run $\rho_{1}$ which satisfies conditions $(4)$ and $(5)$ (for $i=1$). We call this simulation phase $S_{1}$. To construct a run $\rho_{2}$ on $u_{2}v_{2}w_{2}$, $C$ proceeds similarly as in $S_{1}$. We call this simulation $S_{2}$. Note that both simulation requires only a polynomial number of states.

It remains to explain $(i)$ how to check condition $(6)$ and $(ii)$ how to check condition $(3)$, i.e. whether $\rho_{i}$ can be extended into accepting runs over $u_{i}v_{i}w_{i}z_{i}^{\omega}$, for $i=1,2$.

The two counters are used to check condition $(6)$, i.e. to check the existence of a mismatch between the outputs of $\rho_{1}$ and $\rho_{2}$. To do so, the simulation $S_{i}$, $i=1,2$, is again divided into two modes: in the first mode, whenever $\mathcal{T}$ produces some output word $\alpha$, the $i$th counter of $C$ is incremented by $|\alpha|$, using the vector $(|\alpha|,0)$ for $i=1$, and $(0,|\alpha|)$ for $i=2$. So, the $i$th counter counts the length of the outputs produced so far by $\mathcal{T}$ on $u_{i}v_{i}w_{i}$. Non-deterministically, it eventually decides to stop counting this length, and increments the counter $c_{i}$ one last time by some $0\leq\ell\leq|\alpha|$. It then keeps in memory the $c_{i}$th letter produced by $\mathcal{T}$, say, $\tau_{i}\in\Gamma$. After this non-deterministic guess, which corresponds to existentially quantify an output position, the $i$th counter is left unchanged during the whole computation of $C$. The automaton $C$ will accept only if $c_{1}=c_{2}$ and $d_{1}\neq d_{2}$, ensuring the existence of a mismatch between $\mathsf{out}(\rho_{1})$ and $\mathsf{out}(\rho_{2})$. Again, this needs only a polynomial number of states: simulation $S_{i}$ is divided into two modes (before and after the non-deterministic guess), so, $C$ only needs to remember in which mode it is.

To conclude, it remains to show how condition $(3)$ can be checked, i.e. how $C$ can check that $\rho_{i}$ can be extended into an accepting run over $u_{i}v_{i}w_{i}z_{i}^{\omega}$. This is a direct application of Lemma 16.

Finally, Lemma 12 is a direct consequence of Lemma 17 and Proposition 14.

Deciding continuity for regular functions

We prove the following theorem:

Theorem 18**.**

Deciding whether a regular function given as a deterministic two-way transducer with prophetic Büchi look-ahead is continuous is PSpace-c.

Proof 5.9**.**

The lower bound has been established in Theorem 13. For the upper-bound, let $\mathcal{T}$ be a 2DFTpla defining a regular function $f$, with set of look-ahead states $Q_{P}$. According to Proposition 9, one needs to check whether $\widetilde{\mathcal{T}}$ admits a critical pattern $u_{1},v_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2}$ such that $\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$. We have seen in the proof of Theorem 13 how to construct a 2PA $P$ of polynomial size which accepts the set of (encodings of) critical patterns. Additionally here, $P$ needs to check whether $\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$. The difficulty lies in that $\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$ is not equivalent to $u_{1}v_{1}^{\omega}\in\mathsf{dom}(\tilde{f})$, because $u_{1}v_{1}^{\omega}$ may not be a good annotated word (see Section 5.2.1). So, it is not correct to check whether $u_{1}v_{1}^{\omega}\in\mathsf{dom}(\tilde{f})$.

To overcome this difficulty, we modify the notion of critical pattern into strong critical pattern, which also includes some good annotation of $\pi_{\Sigma}(u_{1}v_{1}^{\omega})$. A strong critical pattern is a tuple of words $(u^{\prime}_{1},v^{\prime}_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2})$ such that $u^{\prime}_{1},v^{\prime}_{1}\in(\Sigma\times Q_{P}\times Q_{P})^{*}$, $(\pi_{1,2}(u^{\prime}_{1}),\pi_{1,2}(v^{\prime}_{1}),w_{1},z_{1},u_{2},v_{2},w_{2},z_{2})$ is a critical pattern and $\pi_{1,3}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})\in\mathsf{dom}(\tilde{f})$, where $\pi_{1,2}$ is a morphism which only keeps the first and second alphabet components while $\pi_{1,3}$ only keeps the first and third components. We show that $f$ is continuous if and only if $\mathcal{T}$ admits a strong critical pattern. If $\mathcal{T}$ admits a strong critical pattern $(u^{\prime}_{1},v^{\prime}_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2})$, then for $u_{1}=\pi_{1,2}(u^{\prime}_{1})$ and $v_{1}=\pi_{1,2}(v^{\prime}_{1})$, we have that $(u_{1},v_{1},w_{1},z_{1},u_{2},v_{2},w_{2},z_{2})$ is a critical pattern. Moreover, $\pi_{1,3}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})\in\mathsf{dom}(\tilde{f})$, which implies that $\pi_{\Sigma}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})=\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$. Hence $f$ is continuous.

Conversely, if $f$ is continuous, $\widetilde{\mathcal{T}}$ admits a critical pattern $pat=(u_{1},v_{1},w_{1},z_{1},u_{2},v_{2}$, $w_{2},z_{2})$ such that $\pi_{\Sigma}(u_{1}v_{1}^{\omega})\in\mathsf{dom}(f)$. Since the look-ahead automaton is prophetic, its accepting run on $\pi_{\Sigma}(u_{1}v_{1}^{\omega})$ is of the form $r=r_{1}r_{2}^{\omega}$ such that $r_{1}$ is a run on $\pi_{\Sigma}(u_{1}v_{1}^{k_{1}})$ for some $k_{1}\geq 0$ and $r_{2}$ is a run on $\pi_{\Sigma}(v_{1}^{k_{2}})$ for some $k_{2}\geq 1$. We then let $u^{\prime}_{1}=(u_{1}v_{1}^{k_{1}})\otimes r_{1}$ and $v^{\prime}_{1}=(v_{1}^{k_{2}})\otimes r_{2}$. We also let $u^{\prime}_{2}=u_{2}v_{2}^{k_{1}}$ and $v^{\prime}_{2}=v_{2}^{k_{2}}$. We claim that $(u^{\prime}_{1},v^{\prime}_{1},w_{1},z_{1},u^{\prime}_{2},v^{\prime}_{2},w_{2},z_{2})$ is a strong critical pattern. Clearly, $\pi_{1,3}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})\in\mathsf{dom}(\tilde{f})$, because the annotation of $\pi_{1,3}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})$ is $r_{1}r_{2}^{\omega}$ which is an accepting run of the look-ahead automaton. It remains to show that $pat^{\prime}=(\pi_{1,2}(u^{\prime}_{1})=u_{1}v_{1}^{k_{1}},\pi_{1,2}(v^{\prime}_{1})=v_{1}^{k_{2}},w_{1},z_{1},u^{\prime}_{2}=u_{2}v_{2}^{k_{1}},v^{\prime}_{2}=v_{2}^{k_{2}},w_{2},z_{2})$ is a critical pattern for $\widetilde{\mathcal{T}}$. It is immediate as $v_{1}$ and $v_{2}$ are idempotent and non-producing, so, iterating them does not change the existence of accepting runs whose outputs mismatch.

We have established that $f$ is continuous if and only if $\widetilde{\mathcal{T}}$ admits a strong critical pattern. As shown in Lemma 17, the set of (encodings of) critical patterns is recognisable by a bounded-visit 2PA of polynomial size. We need here to slightly modify the 2PA constructed in Lemma 17 so that it also checks whether $\pi_{1,3}(u^{\prime}_{1}(v^{\prime}_{1})^{\omega})$ is in the domain of $\mathcal{T}$. Based on Lemma 16, we can construct a bounded-visit two-way automaton of polynomial size checking the latter property. When this automaton has successfully checked the latter property, it is then sequentially composed with a 2PA as in Lemma 17 checking whether the input (where the third components of the alphabets are ignored) forms a critical pattern. The resulting composition is a bounded-visit 2PA of polynomial size, whose emptiness can be checked in PSpace, as shown in [FGM19].

6. Conclusion

In this paper, we have studied two notions of computability for rational and regular functions, shown their correspondences to continuity notions which we proved to be decidable in NLogSpace and PSpace respectively. The notion of uniform computability asks for the existence of a modulus of continuity, which tells how far one has to go in the input to produce a certain amount of output. It would be interesting to give a tight upper bound on modulus of continuity for regular functions, and we conjecture that it is always a linear (affine) function in that case.

Another interesting direction is to find a transducer model which captures exactly the computable, and uniformly computable, rational and regular functions. For rational functions, the deterministic (one-way) transducers are not sufficient, already for uniform computability, as witnessed by the rational function which maps any word of the form $a^{n}b^{\omega}$ to itself, and any word $a^{n}c^{\omega}$ to $a^{2n}c^{\omega}$. For regular functions, we conjecture that 2DFT characterise the computable ones, but we have not been able to show it yet.

Finally, much of our work deals with reg-preserving functions in general. An interesting line of research would be to investigate continuity and uniform continuity for different classes of functions which have this property. One natural candidate is the class of polyregular functions introduced in [Boj18] which enjoy several different characterisations and many nice properties, including being effectively reg-preserving. This means that continuity and computability also coincide, however deciding continuity seems challenging.

Appendix A Proofs from Section 2

Proof A.1** (Proof of Theorem 1).**

In [AFT12], authors show that a function is regular iff it is definable by $2\textsf{DMT}\textsubscript{{la}}$. We show that a function is $2\textsf{DMT}\textsubscript{{la}}$ definable iff it is $2\textsf{DFT}\textsubscript{{pla}}$ definable. Recall that $2\textsf{DMT}\textsubscript{{la}}$ is defined as $(\mathcal{T},A,B)$ where $\mathcal{T}$ is a two-way deterministic transducer with Muller acceptance, $A$ is a regular look-ahead automaton, given by a Muller automaton and $B$ is a regular look-behind given by a finite state automaton.

Given a 2DFTpla $(\mathcal{A},P)$, where $\mathcal{A}=(Q,\Sigma,\Gamma,\delta_{\mathcal{A}},q_{0})$ and $P=(Q_{P},\Sigma,\delta_{P},Q_{0},F)$, we construct a 2DMTla $(\mathcal{T},A,B)$ as follows: For every state $p\in Q_{P}$, we construct an equivalent Muller automaton $A_{p}$ with initial state $s_{p}$ s.t. $\mathcal{L}(P,p)=\mathcal{L}(A_{p})$. The Muller look-ahead automaton $A$ used in the 2DMTla $(\mathcal{T},A,B)$ is the disjoint union of the Muller automata $A_{p}$ for all $p\in Q_{P}$. $\mathcal{T}=(Q,\Sigma,\Gamma,\delta_{\mathcal{T}},q_{0},2^{Q}\backslash\emptyset)$, and $\delta_{\mathcal{T}}$ is obtained by modifying the transition function $\delta_{\mathcal{A}}(q,a,p)=(q^{\prime},\gamma,d)$ as $\delta_{\mathcal{T}}(q,a,s_{p})=(q^{\prime},\gamma,d)$. Since the language accepted by two distinct states of a prophetic automaton are disjoint, the language accepted by $A_{p}$ and $A_{p}^{\prime}$ are disjoint for $p\neq p^{\prime}$. The look-behind automaton $B$ accepts all of $\Sigma^{*}$. It is easy to see that $(\mathcal{T},A,B)$ is deterministic : on any position $i$ of the input word $a_{1}a_{2}\dots$, and any state $q\in Q$, there is a unique $A_{p}$ accepting $a_{i+1}a_{i+2}\dots$. The domain of $(\mathcal{T},A,B)$ is the same as that of $(\mathcal{A},P)$, since the accepting states of $A$ are the union of the accepting states of all the $A_{p},p\in Q_{P}$. Since all the transitions in $\delta_{\mathcal{T}}$ have the same outputs as in $\delta_{\mathcal{A}}$ for each $(q,a,p)$, the function computed by $(\mathcal{A},P)$ is the same as that computed by $(\mathcal{T},A,B)$.

For the other direction, given a 2DMTla, it is easy to remove the look-behind by a product construction [DGN18]. Assume we start with such a modified 2DMTla $(\mathcal{T},A)$ with no look-behind. Let $\mathcal{T}=(Q_{\mathcal{T}},\Sigma,\Gamma,\delta_{\mathcal{T}},s_{\mathcal{T}},\mathcal{F}_{\mathcal{T}})$ and $A=(Q_{A},\Sigma,\delta_{A},s_{A},\mathcal{F}_{A})$ where $\mathcal{F}_{\mathcal{T}},\mathcal{F}_{A}$ respectively are the Muller sets corresponding to $\mathcal{T}$ and $A$. We describe how to obtain a corresponding 2DFTpla $(\mathcal{A},P)$ with $P$, a prophetic Büchi look-ahead automaton. $\mathcal{A}$ is described as $(Q_{\mathcal{T}},\Sigma,\Gamma,\delta,p_{0})$. The prophetic look-ahead automaton is described as follows. Corresponding to each state $q\in Q_{A}$, let $P_{q}$ be a prophetic automaton such that $\mathcal{L}(A,q)=\mathcal{L}(P_{q})$ (this is possible since prophetic automata capture $\omega$-regular languages [CPP08]). Since $\mathcal{A}$ has no accepting condition, we also consider a prophetic look-ahead automaton to capture $\mathsf{dom}(\mathcal{T})$. The Muller acceptance of $\mathcal{T}$ can be translated to a Büchi acceptance condition, and let $P_{\mathsf{dom}(\mathcal{T})}$ represent the prophetic automaton such that $\mathcal{L}(P_{\mathsf{dom}(\mathcal{T})})=\mathsf{dom}(\mathcal{T})$. Thanks to the fact that prophetic automata are closed under synchronized product, the prophetic automaton $P$ we need, is the product of $P_{q}$ for all $q\in Q_{A}$ and $P_{\mathsf{dom}(\mathcal{T})}$. Assuming an enumeration $q_{1},\dots,q_{n}$ of $Q_{A}$, the states of $P$ are $|Q_{A}|+1$ tuples where the first $|Q_{A}|$ entries correspond to states of $P_{q_{1}},\dots,P_{q_{n}}$, and the last entry is a state of $P_{\mathsf{dom}(\mathcal{T})}$. Using this prophetic automaton $P$ and transitions $\delta_{\mathcal{T}}$, we obtain the transitions $\delta$ of $\mathcal{A}$ as follows. Consider a transition $\delta_{\mathcal{T}}(p,a,q_{i})=(q^{\prime},\gamma,d)$. Correspondingly in $\mathcal{A}$, we have $\delta(p,a,\kappa)=(q^{\prime},\gamma,d)$ where $\kappa$ is a $|Q_{A}|+1$ tuple of states such that the $i$th entry of $\kappa$ is an initial state of $P_{q_{i}}$. From the initial state $s_{\mathcal{T}}$, on reading $\vdash$, if we have $\delta_{\mathcal{T}}(p_{0},\vdash,q_{i})=(q^{\prime},\gamma,d)$, then $\delta(p_{0},\vdash,\kappa)=(q^{\prime},\gamma,d)$ such that the $i$th entry of $\kappa$ is an initial state of $P_{q_{i}}$ and the last entry of $\kappa$ is an initial state of $P_{\mathsf{dom}(\mathcal{T})}$.

To see why $(\mathcal{A},P)$ is deterministic. For each state $q\in Q_{\mathcal{T}}$, for each position $i$ in the input word $a_{1}a_{2}\dots a_{i}\dots$, there is a unique state $p\in Q_{A}$ such that $a_{i+1}a_{i+2}\dots$ is accepted by $A$. By our construction, the language accepted from each $p\in Q_{A}$ is captured by the prophetic automaton $P_{p}$; by the property of the prophetic automaton $P$, we know that for any $q_{1},q_{2}\in Q_{A}$ with $q_{1}\neq q_{2}$, $L(P_{q_{1}})\cap L(P_{q_{2}})=\emptyset$. Thus, in $(\mathcal{A},P)$, for each state $q$ of $\mathcal{A}$, there is a unique state $p\in P$ such that the suffix is accepted by $L(P)$; further, from the initial state of $\mathcal{A}$, from $\vdash$, there is a unique state $p\in P$ which accepts $\mathsf{dom}((\mathcal{T},A))$. Hence $\mathsf{dom}((\mathcal{A},P))$ is exactly same as $\mathsf{dom}((\mathcal{T},A))$. For each $\delta_{\mathcal{T}}(q,a,q_{i})=(q^{\prime},\gamma,d)$, we have the transition $\delta(q,a,\kappa)=(q^{\prime},\gamma,d)$ with the $i$th entry of $\kappa$ equal to the initial state of $P_{q_{i}}$, which preserves the outputs on checking that the suffix of the input from the present position is in $L(P_{q_{i}})$. Notice that the entries $j\neq i$ of $\kappa$ are decided uniquely, since there is a unique state in each $P_{q}$ from where each word has an accepting run. Hence, $(\mathcal{A},P)$ and $(\mathcal{T},A)$ capture the same function.

Remark 19**.**

Example function $g$ given in Section 2, after Theorem 1 cannot be realised without look-ahead, not even if we allow non-determinism.