Expregular Functions

A (string-to-string) MSO set interpretation $\mathrm{\Phi }$ from ${\mathrm{\Sigma }}^{\ast }$ to ${\mathrm{\Gamma }}^{\ast }$(over a finite set $F$), where $\mathrm{\Sigma }$ and $\mathrm{\Gamma }$ are finite alphabets, is given by MSO formulas ${\varphi }_{\mathrm{conf}}(X^{(F)})$, and for each $\gamma \in \mathrm{\Gamma }$, a formula ${\varphi }_{\gamma }(X^{(F)})$, where $X^{(F)}$ and $Y^{(F)}$ are $F$-variables. For each $\mathrm{\Sigma }$-string $w$, this defines a -structure $\mathrm{\Phi }(w)$ whose universe is the set of colourings $A^{(F)}$ of the positions of $w$ with $F$ such that $w\vDash {\varphi }_{\mathrm{conf}}(A^{(F)})$ and where is interpreted as and for each $\gamma \in \mathrm{\Gamma }$, the associated unary predicate is interpreted as ${\varphi }_{\gamma }$. We assume that for each $\mathrm{\Sigma }$-string $w$, $\mathrm{\Phi }(w)$ defines a $\mathrm{\Gamma }$-string, which means that is a total order, and the unary predicates associated to the $\gamma \in \mathrm{\Gamma }$ partition the positions.

Given an MSO set interpretation $\mathrm{\Phi }$, $F$-colourings of the input string that satisfy ${\varphi }_{\mathrm{conf}}$ are called configurations; these correspond to positions in the output string (ordered by ). We say that a function is expregular if it is computed by an MSO set interpretation.

We stress the fact that defines the order over the configurations, and not the successor relation. While being irrelevant for regular functions (the configurations are essentially input positions and therefore the order can be defined as the transitive closure of the successor relation), this distinction becomes crucial for polyregular functions (see [5]) as well as expregular functions. Here are some examples.

A string-to-string yield-Hennie machine $\mathscr{H}$ from ${\mathrm{\Sigma }}^{\ast }$ to ${\mathrm{\Gamma }}^{\ast }$ is a branching $1$-tape bounded visit Turing machine. It consists of:

• $\mathrm{■}$

  a finite set of internal states $Q$ with an initial state $q_0\in Q$;

• $\mathrm{■}$

  a finite tape alphabet $\mathrm{\Theta }$ which contains $\mathrm{\Sigma }\cup \{⊳,⊲\}$; and

• $\mathrm{■}$

  a transition function $\delta :Q\times \mathrm{\Theta }\to {(\mathrm{\Gamma }\cup Q\times \mathrm{\Theta }\times \{\leftarrow ,\circlearrowright ,\to \})}^{\ast }$,

such that $\delta (\mathrm{\_},⊳)\in {(\mathrm{\Gamma }\cup Q\times \{⊳\}\times \{\circlearrowright ,\to \})}^{\ast }$ and $\delta (\mathrm{\_},⊲)\in {(\mathrm{\Gamma }\cup Q\times \{⊲\}\times \{\leftarrow ,\circlearrowright \})}^{\ast }$.

To every input string $w\in {\mathrm{\Sigma }}^{\ast }$, we associate a labelled ordered tree called the run over $w$, which is defined top-down as follows:

• $\mathrm{■}$

  the root of the tree is labelled by $(q_0,\underset{¯}{⊳}w⊲)$;

• $\mathrm{■}$

  for all nodes labelled $(q,u)$ where $q$ is a state and $u$ a pointed $\mathrm{\Theta }$-string whose pointed letter is $\theta$ and such that $\delta (q,\theta )={\delta }_1\mathrm{\dots }{\delta }_k$, the node has exactly $k$ children, and for all $i\in \{1,\mathrm{\dots },k\}$, if ${\delta }_i=\gamma$, the $i$th child is labelled $\gamma$, and if ${\delta }_i=(q_i^{\prime },{\theta }_i^{\prime },{\mathrm{dir}}_i)\in Q\times \mathrm{\Theta }\times \{\leftarrow ,\circlearrowright ,\to \}$, then the $i$’th child is labelled $(q_i^{\prime },u_i^{\prime })$ where $u_i^{\prime }$ is the obtained from $u$ by replacing the pointed letter by ${\theta }_i^{\prime }$ and moving the point according to ${\mathrm{dir}}_i$.

Note that in the run over $w$, all pointed strings have the same size as $⊳w⊲$, and therefore we may talk of the position of the mark in a uniform manner. We assume the bounded visit property: there exists some integer $k$ such that for every input string $w$, on every branch of the run over $w$ and for every position $i$, there are at most $k$ labels where the pointer is at position $i$. This implies that the depth of the run over $w$ is bounded by $k(|w|+2)$ hence the run has $2^{O(|w|)}$ nodes. The semantics of $\mathscr{H}$ is the function ${\tau }_{\mathscr{H}}:{\mathrm{\Sigma }}^{\ast }\to {\mathrm{\Gamma }}^{\ast }$ which assigns to $w$ the yield of its run, i.e. the string obtained by concatenating all labels of leaves in $\mathrm{\Gamma }$ along a traversal of the leaves in the natural order.

Here are some examples.

An Ariadne transducer $𝒜$ from ${\mathrm{\Sigma }}^{\ast }$ to ${\mathrm{\Gamma }}^{\ast }$ consists of:

• $\mathrm{■}$

  a partially ordered set of states $Q$, with an initial state $q_0\in Q$;

• $\mathrm{■}$

  a local stack bound $k\in \mathbb{N}$ – we write $Q^{⩽k}=\{u\in Q^{\ast }\mid |u|⩽k\}$;

• $\mathrm{■}$

  a partial transition function of the following type:

  $$\delta :(\mathrm{\Sigma }\cup \{⊳,⊲\})\times Q^{⩽k}\rightharpoonup {\mathrm{\Gamma }}^{\ast }\times (\{{\mathrm{𝚙𝚞𝚜𝚑}}_{\to },{\mathrm{𝚙𝚞𝚜𝚑}}_{\circlearrowright },{\mathrm{𝚙𝚞𝚜𝚑}}_{\leftarrow }\}\times Q\cup \{\mathrm{𝚙𝚘𝚙}\}\times \mathrm{Update}(Q)),$$

  where $\mathrm{Update}(Q)$ is the set of partial functions $f:Q\rightharpoonup Q$ which are inflationary (i.e. $f(q)>q$ if it is defined).

Consider an input $\mathrm{\Sigma }$-string $w$. A stack of $𝒜$ over $w$ is a sequence $s\in {(Q\times \{0,\mathrm{\dots },|w|+1\})}^{\ast }$. Given a non-empty stack $s$, we define the top and the untop of $s$ with $\mathrm{top}(s)=(p,i)$ such that $s=\mathrm{untop}(s)\cdot (p,i)$. We say that $p$ is the top state of $s$ and $i$ is its top position. Given a position $i\in \{0,\mathrm{\dots },|w|+1\}$, we denote by ${s|}_i\in Q^{\ast }$ the local view of $s$ at $i$, which is the sequence of top states of prefixes of $s$ with top position $i$ (in increasing prefix order).

The initial stack over $w$ is $(q_0,0)$. Let $s$ be a stack over $w$ with top position $i$, let $\sigma$ be the $i$-th letter of $⊳w⊲$ and let ${s|}_i=p_1\mathrm{\dots }{p}_{\mathrm{\ell }}$ be the corresponding local view. Suppose that $(u,\mathrm{𝖺𝖼𝗍𝗂𝗈𝗇})=\delta (\sigma ,p_1\mathrm{\dots }{p}_{\mathrm{\ell }})$ is defined, which implies $\mathrm{\ell }⩽k$. We define the successor stack $s^{\prime }$ of $s$ over $w$ as follows:

• $\mathrm{■}$

  if $\mathrm{𝖺𝖼𝗍𝗂𝗈𝗇}=({\mathrm{𝚙𝚞𝚜𝚑}}_{\to },q)$ and $i+1\le |w|+1$, then $s^{\prime }=s\cdot (q,i+1)$;

• $\mathrm{■}$

  if $\mathrm{𝖺𝖼𝗍𝗂𝗈𝗇}=({\mathrm{𝚙𝚞𝚜𝚑}}_{\circlearrowright },q)$ then $s^{\prime }=s\cdot (q,i)$;

• $\mathrm{■}$

  if $\mathrm{𝖺𝖼𝗍𝗂𝗈𝗇}=({\mathrm{𝚙𝚞𝚜𝚑}}_{\leftarrow },q)$ and $i-1\ge 0$, then $s^{\prime }=s\cdot (q,i-1)$;

• $\mathrm{■}$

  if $\mathrm{𝖺𝖼𝗍𝗂𝗈𝗇}=(\mathrm{𝚙𝚘𝚙},f)$ and $\mathrm{untop}(s)=r\cdot (p,j)\ne \epsilon$, then $s^{\prime }=r\cdot (f(p),j)$;

• $\mathrm{■}$

  otherwise, $s^{\prime }$ is undefined.

Whenever $s^{\prime }$ is defined, the word $u$ is called the production of the stack $s$ over $w$.

The run of $𝒜$ over $w$ is the sequence of stacks $s_1,\mathrm{\dots },s_n$ such that $s_1$ is the initial stack, $s_{m+1}$ is the successor stack of $s_m$ for all , and $s_n$ has no successor. Stacks are preordered lexicographically (by using the partial order over $Q$ and ignoring the positions). Note that the transition steps imply that $s^{\prime }>s$ whenever the successor stack $s^{\prime }$ of $s$ is defined, and hence a run cannot contain the same stack twice. Note furthermore that runs are of size at most ${|Q|}^{|w|k}$ which is exponential in $|w|$. The production of $𝒜$ over $w$ is the concatenation $u_1\mathrm{\cdots }{u}_n$ of productions of $s_1,\mathrm{\dots },s_n$. The semantics of $𝒜$ is the function ${\tau }_{𝒜}:{\mathrm{\Sigma }}^{\ast }\to {\mathrm{\Gamma }}^{\ast }$ which maps a word to the production of $𝒜$ over it.

Here are some examples.

For $i$ a position of the input, let $\overrightarrow{i}$ be the set of positions $⩽i$, and $\overleftarrow{i}$ the set of positions $⩾i$. We call sets of the form $\overrightarrow{i}$ or $\overleftarrow{i}$ splits⁵⁵5Technically, one requires that the complement of a split be a split, and hence that the full set of positions is not allowed to be a split.. Given a split $s$, we let $\overline{s}$ denote its complement, which is also a split. Recall that positions in the output string correspond to configurations (i.e. $F$-colourings $A$ of $w$ such that $w\vDash {\varphi }_{\mathrm{conf}}(A)$), ordered by . Consider an interval $I$ of configurations.

We define what it is for $I$ to be $d$-simple at $s$ (for $d⩾0$) recursively. The interval $I$ is $0$-simple at $s$ if all the configurations $A\in I$ are equal when restricted to $s$. For the general case, an interval $I$ is $d$-simple at $s$ if there is a set $P\subseteq I$ such that (1) all the configurations in $P$ are equal when restricted to $s$, and (2) all sub-intervals of $I$ that do not intersect $P$ are $(d-1)$-simple at $\overline{s}$. Call simplicity of $I$ at $s$ the least $d$ such that $I$ is $d$-simple at $s$.

A first crucial argument in the proof is that the above phenomenon is always true: for all string-to-string MSO set interpretation, there exists $d_0$ such that for all input strings, all splits $s$, and all interval $I$ of configurations, $I$ is $d$-simple at $s$. This proof relies on the facts that the MSO set interpretation defines a total order (and not only successor), and that when comparing two configurations it is sufficient to consider boundedly many MSO-types over $s$ and $\overline{s}$ (compositionality).

Consider an interval of positions of the output string $I$ together with a split $s$, which corresponds to a potential node of the run of the yield-Hennie machine that we are trying to construct. Now that the notion of simplicity is established, we should define the children of the node corresponding to $I$ and $s$. More precisely, we want to decompose $I$ into a union of a bounded number of children intervals $I_1,\mathrm{\dots },I_{\mathrm{\ell }}$, so that each interval $I_j$ comes together with a split $s_j$ which is obtained from $s$ by moving the cut-position either to the left of to the right.

The crucial feature of this decomposition should be that the bounded-visit property is satisfied, i.e. each position is seen a bounded number of times on each branch. In terms of simplicity, this naturally translates to the condition that if $I^0\to I^1\to \mathrm{\dots }\to I^n$ defines a sequence of intervals such that for some splits $s^0,\mathrm{\dots },s^n$, it holds for every that $(I^{k+1},s^{k+1})$ is a child of $(I^k,s^k)$, and moreover $s^0$ and $s^n$ have the same cut-position, then the simplicity of $I^n$ at $s^n$ should be strictly lower than the simplicity of $I^0$ at $s^0$.

Defining such a decomposition requires an understanding of how simplicities evolve when moving between two successive splits (e.g. from $\overrightarrow{i}$ to $\overrightarrow{i+1}$, or from $\overrightarrow{i}$ to $\overleftarrow{i}$).

In a yield-Hennie machine, every node contains a pointed string which corresponds to a colouring $C$ of the input together with a position $i$. Following the above approach, the obvious choice is for $i$ to encode the current split $s$ (together with a bit of information corresponding to its direction that can be added to $C$), and for $C$ to encode the interval $I=[A,B]$, by writing the two configurations $A$ and $B$. Unfortunately there is a major issue with this approach: when moving from a node to one of its children, the yield-Hennie machine can update the current colouring $C$ only at the pointed position $i$. However if $C$ is written as a pair of configurations $A,B$, there is no guarantee that its children can be obtained by such local updates of the colourings defining the configurations. Overcoming this issue requires introducing some additional infrastructure that we describe now.

Defining an encoding of $(I,s)$ as a colouring of the input string in a way that can be updated locally when moving from $(I,s)$ to its children is achieved by combining two ideas.

• $\mathrm{■}$

  Definable basis of intervals: we construct families of intervals $B_s$, one for each split $s$, with the properties that

  1. (a)

     every interval which is $d$-simple at $s$ can be covered by a bounded union of $d$-simple at $s$ intervals from $B_s$;

  2. (b)

     every configuration belongs to a bounded number of intervals from $B_s$; and

  3. (c)

     given (the natural encodings of) $I$ and $s$, membership of $I$ in $B_s$ is MSO definable.

  From now on, we fix such a definable basis ${(B_s)}_{s\text{ split}}$.

• $\mathrm{■}$

  Funnels: we represent a node corresponding to interval $I$ and split $s$ by a sequence $I_0,s_0,\mathrm{\dots },I_n,s_n$ of intervals and splits, which we call a funnel, such that⁶⁶6We also have a condition on the simplicities which will guarantee the bounded visit property, but we omit it in this overview.

  • –

    $I_0$ is the interval of all positions and $s_0=\overrightarrow{0}$;

  • –

    the $I_k$’s are basis intervals i.e. $I_k\in B_{s_k}$;

  • –

    the splits $s_0,s_1,\mathrm{\dots },s_n$ are consecutive;

  • –

    $s_n$ is $s$ and $I$ is the intersection of the $I_k$’s;

  • –

    for every $k$, $(I_{k+1},s_{k+1})$ is a child of $({\bigcap }_{m\le k}{I}_k,s_k)$ as defined above.s

  Intuitively, instead of storing $(I,s)$, we remember the full path from the root node to $(I,s)$, except that it is stored using basis intervals, and $I$ is obtained as an intersection of these intervals.

Of course it is not at all clear how this circumvents the problem highlighted above; for this we should explain how funnels are encoded as colourings of the input string.

To encode a funnel $F=I_0,s_0,\mathrm{\dots },I_n,s_n$ we proceed as follows. Let $j_0,\mathrm{\dots },j_{n-1}$ be such that for every $k$, it holds that $F_{\le k+1}=I_0,s_0,\mathrm{\dots },I_{k+1},s_{k+1}$ is the $j_k$-th child of $F_{\le k}$. Since the splits are consecutive and satisfy the bounded visit property, the sequence $s_0,\mathrm{\dots },s_n$ can be encoded as a colouring of the input using an adequate notion of tilings. To encode the funnel $F$, we integrate the labels $j_0,\mathrm{\dots },j_{n-1}$ (these are bounded integers) in the above tiling. Note that this encoding is indeed locally updatable: the encoding of the $j$-th child of $F$ is obtained from the encoding of $F$ by adding one step (labelled by $j$) at the current position.

The crucial idea is that given an encoding $T$ of a funnel as above, there exist a formula that recovers the output $I={\bigcap }_k{I}_k$ of the funnel as follows. First we guess a configuration $A$ in $I$, and guess a labelled tiling (corresponding to the same sequence of splits) with labels $p_0,\mathrm{\dots },p_n$, such that for every $k$, $I_k$ is the $p_k$-th interval from $B_{s_k}$ containing $A$ (here we rely on property b of definable bases). Then we verify local consistency of these guesses, and recover $I$ as the intersection of the $I_k$’s.

We are now ready for the final construction. Here the important insight is that in the previous items, the proofs are phrased in terms of definability. In particular, given an encoding of a funnel, the encoding of the next funnel is definable. Therefore to define the transitions from a given node (i.e. , a funnel), it suffices to have access to the MSO-type (defined just below) of sufficiently large quantifier rank of the current labelling of the tape (which encodes the funnel). In a nutshell, this is achieved⁷⁷7This trick is stolen from [14, Lemma 4]. by labelling the tape with one half of the type, and storing the other half in the current state (where the directions of the halves depend on the direction of the current split).