Transducers on Compressed Strings

Bojańczyk, Mikołaj; Lohrey, Markus

doi:10.4230/LIPIcs.ICALP.2026.170

Transducers on Compressed Strings

Mikołaj Bojańczyk

University of Warsaw, Poland Markus Lohrey

University of Siegen, Germany

Abstract

We study string-to-string functions which are compatible with compression in the following sense: given a compressed representation of an input string, one can compute in polynomial time a compressed representation of the output string. As the compression formalism, we use straight-line programs (i.e. context-free grammars that produce only one string). As the functions, we use finite state transducers, with a focus on the regular and polyregular functions. We show that all regular functions are compatible with compression, but this is no longer true for the polyregular functions. We identify a subclass of the polyregular functions – the so-called rectangular polyregular functions – which is compatible with compression, and we characterise this subclass in terms of a functional programming language.

Keywords and phrases:

polyregular functions, grammar compression

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Funding:

Mikołaj Bojańczyk: Mikołaj Bojańczyk was supported by the Polish National Science Centre (NCN) grant “Polynomial finite state computation” (2022/46/A/ST6/00072).

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Automata extensions

DOI:

10.4230/LIPIcs.ICALP.2026.170

Event:

53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The starting point for this work stems from the paradigm of algorithmics on compressed data. Its principal idea is to process data that is given in compressed form without first decompressing it and then operating on the uncompressed data. There are three main applications for algorithms of this kind (see [26] for a survey).

$\blacksquare$

In many applications one has to combine compression and querying. A typical example is a genome database where DNA sequences are stored in compressed form and searched for specific patterns (e.g. genes). This leads to so-called compressed text indices [13, 17].
$\blacksquare$

A compressed representation of the input data might reveal certain regularities, which could be used to speed up an algorithm. This principle is known as acceleration by compression. An example can be found in [24], where Viterbi’s algorithms for decoding hidden Markov chains is sped up using compression.
$\blacksquare$

Large and often highly compressible data may appear as intermediate data structures in algorithms. In such a situation, one may try to store a compressed representation of these intermediate data structures and to process this representation. This may lead to more efficient algorithms. One example, which arises in group theory, is the compressed word problem: checking if two compressed representations describe the same group element, see the surveys [2, 27].

We begin our investigation of algorithmics on compressed data by clarifying two aspects: (i) what compressed representation of data is used and (ii) what are the processing steps carried out on the compressed data?

Grammar-based string compression

Let us first address question (i), which is about the compression format. In this paper we consider strings (words) that are compressed using context-free grammars: a grammar compression of a string $w\in A^{*}$ is a context-free grammar which generates the string $w$ and no other strings (we will also shortly speak of a compression of $w$ ). Syntactically, this can be ensured by only considering context-free grammars that are acyclic (there is no nonterminal $X$ and a non-empty derivation $X\Rightarrow^{+}u$ such that $X$ appears in $u$ ) and where every nonterminal is on the left-hand side of exactly one production. An equivalent representation is a straight-line program, which is a sequence of instructions of the form $x:=a$ and $x:=y\cdot z$ for variables $x, y, z$ and a terminal symbol $a$ . The following straight-line program generates the string $a a a a$ :

⬇

1 x := a

2 y := x

\cdot

x

3 z := y

\cdot

y

The variables can be seen as non-terminals, and the variable $z$ in the last line can be seen as the starting non-terminal. Note that a straight-line program corresponds to a context-free grammar in Chomsky normal form. We define the size of a straight-line program as the number of instructions (or, equivalently, the number of non-terminals in the corresponding Chomsky normal form grammar). A straight-line program can achieve exponential compression, but not more: every program of size $n$ generates a string of length at most $2^{n}$ . It is well known that every string of length $n$ over an alphabet of size $\sigma$ can be generated by a straight-line program of size $\mathcal{O}(n/\log_{\sigma}n)$ ; see [4, Proposition 3.1] where straight-line programs are called word chains.

Although computing a minimal straight-line program for a given string is not possible in polynomial time unless P = NP [12, Theorem 1], there exist several compressors that achieve a good approximation of a smallest straight-line program [12, 20, 32]. Straight-line programs have been intensively used in algorithmics on compressed data. Algorithmic problems that can be solved in polynomial time on grammar compressed strings are for instance checking equality [19, 28, 30], pattern matching [22, 21], and membership in regular languages [31]; see the survey [26] for further details. On the negative side, testing membership of a grammar compressed string in a context-free language (and even a fixed visibly pushdown language) is a PSPACE-complete problem [25, Theorem 9].

String-to-string functions

We now come to the second question (ii): What are the processing steps carried out on the compressed data? We will use string-to-string functions, which are functions $f:A^{*}\to B^{*}$ where $A$ and $B$ are finite alphabets. Among such functions, we will be interested in those that can be evaluated in polynomial time using compressed representations, as described in the following definition.

Definition 1.

A string-to-string function $f:A^{*}\to B^{*}$ is called compatible with compression if there is a deterministic polynomial time algorithm which does this:

$\blacksquare$

Input: a compression of a string $w\in A^{*}$ .
$\blacksquare$

Output: a compression of the string $f(w)\in B^{*}$ .

Let us begin with some examples of functions that are compatible – or not – with compression. In the examples, we use straight-line programs rather than grammars.

Example 2 (duplication).

The string duplication function $w\mapsto ww$ is compatible with compression. The corresponding operation on straight-line programs is to append one more line x := y $\cdot$ y, where y was the last variable used in the input program. $\lrcorner$

Example 3 (reversal).

String reversal is also compatible with compression. The corresponding operation on straight-line programs is to reverse the order of concatenation in every line. $\lrcorner$

Example 4 (squaring).

Consider the squaring function illustrated as follows:

\displaystyle 123\quad\mapsto\quad 123123123.

This function is compatible with compression. To implement squaring on straight-line programs, we write the code of the program twice, with the second copy using the output of the first copy instead of the character constants. $\lrcorner$

Example 5 (exponential outputs).

This is a non-example, i.e. a function that is not compatible with compression. Assume that the input and output alphabets have one letter only, and consider the function

a^{n}\quad\mapsto\quad a^{2^{n}}.

(1)

This function is not compatible with compression. The reason is that we can produce $a^{2^{k}}$ by a straight-line program of size $k$ . The function (1) maps $a^{2^{k}}$ to $a^{2^{2^{k}}}$ which requires a straight-line program of size $2^{k}$ . Such a straight-line program cannot be constructed in polynomial time from a straight-line program of size $k$ . $\lrcorner$

Characterizing the class of all string-to-string functions that are compatible with compression might be a very difficult task. In this paper, we are interested in string-to-string functions that can be computed by finite-state transducer models. As explained in Example 5, a transducer computing a function that is compatible with compression cannot produce outputs of exponential size, which excludes many important transducer models (at least in their full generality), such as copyful streaming string transducers [18, Section 2.1] or the even more general model of macro tree transducers (in the string-to-string case) [16, Section 3.1]. For this reason, we will only consider transducer models that produce outputs of polynomial size. The largest known class of string-to-string transducers with polynomial size outputs are the polyregular functions [7], and thus all transducers in this paper will be special cases of the polyregular functions. We will consider three such classes:

\displaystyle\text{rational functions}\;\subseteq\;\text{regular functions}\;% \subseteq\;\text{polyregular functions.}

Rational functions are computed by nondeterministic one-way transducers, whereas regular functions are computed by deterministic two-way transducers. Finally, polyregular functions are computed by deterministic two-way transducers with pebbles. The regular and polyregular functions have many equivalent characterizations [7]; in this paper we will use characterizations based on closure properties of string-to-string functions.

Let us now outline the main contributions of this paper.

$\blacksquare$

In Section 2, we identify which of the above transducer models are compatible with compression. We first prove that the rational functions are compatible with compression and then extend this result to the regular functions using a characterization of the latter class based on closure properties. This cannot be further extended to cover all polyregular functions, since we can give an example of a polyregular function that is not compatible with compression. We then identify a sufficient condition for compatibility; the corresponding class is called the rectangular polyregular functions, and it lies strictly between the regular functions and the polyregular functions. We do not know if rectangularity is also a necessary condition, we leave this as an open problem.
$\blacksquare$

In Section 3, we give evidence that the rectangular polyregular functions are an interesting class of transducers, whose relevance extends beyond the connections with compression. We do this by presenting an equivalent programming language, which can be seen as the least programming language that can capture all regular functions, and which is equipped with $\lambda$ -abstraction and application.

2 Transducers compatible with compression

In this section we define the function classes mentioned in the introduction (rational functions, regular functions, polyregular functions) and study their compatibility with respect to compression.

2.1 Rational functions

We begin with the class of rational functions, which was introduced by Eilenberg [14, Chapter IX] and has been studied extensively since then. Among several equivalent definitions, we use one that is based on nfa with output.

Let us begin with the definition of a rational relation, and then we will identify the rational functions as the special case of rational relations which are functions. A rational relation is described by an nfa with output. This is the same as an nfa, except that there is an additional labelling which assigns output strings (possibly empty) to: (a) initial states; (b) transitions; and (c) final states. Here is a picture of an nfa with output:

Thanks to the labellings with output strings, each accepting run can be seen as producing an output string, which is defined by concatenating the output strings assigned to the initial state, the transitions taken, and the final state. The semantics of the automaton is a binary relation between input and output strings, which assigns to each input string all possible outputs produced by accepting runs. A relation that is obtained this way is called a rational relation. A rational function is the special case of a rational relation which is a function, i.e. for every input string there is exactly one output string. ¹¹1We restrict our attention to total functions. While one could also consider partial functions computed by transducers, this would not introduce any new aspects with respect to compatibility with compression. The following result extends [5, Theorem 1], which only covers the class of sequential functions (a subclass of the rational functions):

Theorem 6.

Rational functions are compatible with compression.

Proof.

It is well known that context-free languages are preserved under images of rational relations [3, Chapter V]. This means that for every context-free language $L\subseteq A^{*}$ and every rational relation $R\subseteq A^{*}\times B^{*}$ , the image

\displaystyle\{w\in B^{*}\ |\begin{tabular}[]{l}$(v,w)\in R$ for some $v\in L$% \end{tabular}\}

is also context-free. The proof is a simple product construction, in particular the size of the output grammar is polynomial in the sizes of the input grammar and the automaton defining the rational relation. If the input grammar generates exactly one string, and the rational relation is in fact a function, then the output grammar will also generate exactly one string. $\hfill\blacktriangleleft$

2.2 The map combinator

Before moving to more expressive regular functions, we prove a closure property for functions that are compatible with compression. This will be useful in the rest of the paper, which will use an approach to transducer classes which emphasises closure properties.

The first closure property, which is immediate from the definition, is that functions compatible with compression are closed under function composition. Another closure property concerns the map operation. The general idea is that a function $f$ is lifted from strings to lists of strings, where it is applied to every list item separately. Since – for now – we are working with strings only, we need to represent lists using a separator symbol, as in the following lemma.

Lemma 7.

Consider a string-to-string function

\displaystyle f:A^{*}\to B^{*},

and let $|$ be a fresh separator symbol that is neither in $A$ nor $B$ . If $f$ is compatible with compression, then so is its map lifting, which is defined to be the function

\displaystyle w_{1}|\cdots|w_{n}\quad\mapsto\quad f(w_{1})|\cdots|f(w_{n})% \qquad\text{for $w_{1},\ldots,w_{n}\in A^{*}$}.

Proof.

The input string for the map lifting uses separators. We begin by improving the compression of the input string so that the structure of the grammar is consistent with the separators. This is done using the following normal form: the nonterminals (except for the starting one) can be partitioned into two groups, called inner (depicted in blue below) and outer (depicted in red), such that every rule in the grammar has one of the following forms, where the string ${\color[rgb]{0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor% }{rgb}{0.921875,0.33984375,0.33984375}v}$ only consists of outer (red) nonterminals and ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}u}$ only consists of inner (blue) nonterminals and symbols from $A$ :

\displaystyle S\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}Y}{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}Z}\qquad{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}X}\to{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}v}\qquad{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}X}\to|{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}Y}\qquad{\color[% rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}X}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}u},

Observe that the partition, if it exists, is unique: the inner nonterminals are those which cannot derive a string containing the separator symbol (they correspond to parts of list items), and the outer ones are those which do (they correspond to sequences of list items).

Claim 8.

Every compression over the alphabet $A\cup\{|\}$ can be converted in polynomial time into an equivalent compression which is in normal form.

Proof.

For a string $w$ that uses at least one separator, define three parts, as in the following picture:

Observe that the last separator is not in any of the parts, and the remaining separators are in the middle part. For a string with exactly one occurrence of $|$ the middle part is missing, whereas a string with no $|$ at all only has a start.

Given a grammar that is not necessarily in normal form, we compute a new grammar in normal form, such that for every nonterminal $X$ in the original grammar, there are three corresponding nonterminals in the new grammar, which generate its start, middle and finish, respectively. The construction is a straightforward induction, it can be implemented in polynomial time, and the output grammar has linear size in the size of the input grammar. For instance, if the original grammar has the production $X\to YZ$ and ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Y_{s}}$ , ${\color[rgb]{0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor% }{rgb}{0.921875,0.33984375,0.33984375}Y_{m}}$ , ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Y_{f}}$ are the nonterminals for the start/middle/finish part of $Y$ (so, we assume that $Y$ produces at least two separators), and similarly for $Z$ , then we introduce the following rules: ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}X_{s}}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named% ]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}u}$ if ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Y_{s}}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named% ]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}u}$ , ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}X_{f}}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named% ]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}v}$ if ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Z_{f}}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named% ]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}v}$ , ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}U}\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}Y_{f}Z_{s}}$ , ${\color[rgb]{0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor% }{rgb}{0.921875,0.33984375,0.33984375}V}\to|{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}U}$ , and ${\color[rgb]{0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor% }{rgb}{0.921875,0.33984375,0.33984375}X_{m}}\to{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}Y_{m}VZ_{m}}$ .

From the new grammar, we easily get a grammar in normal form that generates the same string as the original grammar, by suitably choosing the production for the starting nonterminal. $\hfill\vartriangleleft$ Once we have normalized the input compression, we can easily prove the lemma. The input string can be seen as a list of strings over the alphabet $A^{*}$ , separated by the symbol $|$ . In the compression, each list item will be found as the value of an inner nonterminal ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Y}$ in rules of the form

\displaystyle S\to{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}Y}{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}Z}\qquad{\color[rgb]{% 0.921875,0.33984375,0.33984375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.921875,0.33984375,0.33984375}X}\to|{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}Y},

and it will be found nowhere else. Therefore, we can modify the grammar by replacing every occurrence of ${\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}Y}$ with the corresponding compression of the output string, which is obtained by the assumption that $f$ is compatible with compression. This gives the desired compression of the output string of the map lifting. $\hfill\blacktriangleleft$

2.3 Regular functions

Having proved that the rational string-to-string functions are compatible with compression, we now move to the next class of functions, namely the regular string-to-string functions. The latter class of functions can be defined using several different models, such as two-way automata with output [33], mso transductions [15], or streaming string transducers [1]. Instead of presenting any of these machine models, we use a characterization of the regular functions that uses concepts that have already been introduced in this paper. For the reader who is unfamiliar with regular functions, the following theorem, see [11, Theorem 18], can be taken as the definition of regular functions²²2Let us explain in more detail the relation of Theorem 9 and [11, Theorem 18]. The latter result is in fact stronger, because it allows certain kinds of infinite alphabets, and has fewer closure properties than those mentioned in items 1-4 of Theorem 9. The difficult implication in Theorem 9 is that the regular functions are contained in the smallest class with the listed closure properties 1–4. Therefore, [11, Theorem 18] implies Theorem 9..

Theorem 9.

The class of regular functions is the smallest class of string-to-string functions which:

1.

contains all rational functions;
2.

contains the duplication and reverse functions from Examples 2 and 3;
3.

is closed under composition of functions;
4.

is closed under the map combinator from Lemma 7.

Thanks to the above characterization and the results proved so far, we can immediately deduce compatibility with compression for regular functions.

Theorem 10.

Regular string-to-string functions are compatible with compression.

Proof.

The rational functions are compatible with compression by Theorem 6. The duplication and reversal functions are compatible with compression by Example 2 and 3. The class of functions compatible with compression is closed under composition essentially by definition, and it is closed under the map combinator by Lemma 7. Therefore, by Theorem 9, all regular functions are compatible with compression. $\hfill\blacktriangleleft$ Observe that the proof of the above theorem would continue to work if we would extend the basic functions from item 2 by adding the squaring function from Example 4, or any other function compatible with compression. This observation will be useful in the next section.

2.4 Polyregular functions

Having shown that the rational and regular functions are compatible with compression, we now turn to a more expressive class of functions, namely the polyregular functions. We will show that this class is not compatible with compression, and we will isolate a fragment that is.

Similarly to the rational and regular functions discussed in the previous section, the class of polyregular functions admits many characterizations, see the survey [7] for at least five such characterizations. For the purposes of this paper, it will be most convenient to work with a characterization using combinators, similar to the one from Theorem 9. The idea is to extend the description from Theorem 9 with one more basic function, which is explained in the following example.

Example 11 (marked squaring).

The marked squaring function is like the square function from Example 4, except that each copy of the input string is annotated with an underlined position, with the $i$ -th copy having the $i$ -th position underlined. Here is an example:

\displaystyle 1234\quad\mapsto\quad\underline{1}2341\underline{2}3412% \underline{3}4123\underline{4}

Formally speaking, the output alphabet consists of two copies of the input alphabet, one with and one without underlining. $\lrcorner$

The polyregular functions are then obtained from the regular ones by adding marked squaring to the basic functions, as in the following definition; see [6, Definition 1.2 and Theorem 1.6]³³3In [6, Definition 1.2 and Theorem 1.6] the class of polyregular functions is defined in an equivalent way as the smallest class of functions that is closed under composition and that contains all rational functions, marked squaring and map reverse (i.e., map applied to reverse). Equivalence of this definition with Definition 12 can be shown in the same way as Lemma 19 below..

Definition 12.

The class of polyregular functions is the smallest class of string-to-string functions which:

1.

contains all rational functions;
2.

contains the duplication, reverse and marked squaring functions from Examples 2, 3 and 11;
3.

is closed under composition of functions;
4.

is closed under the map combinator from Lemma 7.

According to the above definition, the polyregular functions extend the regular ones by adding marked squaring. Therefore, to show that the polyregular functions are compatible with compression, it would be enough to show this compatibility for the new function. Unfortunately, this is not the case.

Lemma 13.

Marked squaring is not compatible with compression.

Proof.

Similarly to Example 5, the problem is not in computing the output compression, but simply in the fact that it does not exist in polynomial size. Consider the input string

\displaystyle v_{n}=a^{2^{n}}b.

This string has a compression of size $\mathcal{O}(n)$ . Let $w_{n}$ be the marked squaring of $v_{n}$ . We will show that any compression of $w_{n}$ must have size at least $2^{n}$ . The reason is that $w_{n}$ contains an infix of the form $ba^{i}\underline{a}$ for every $i\in\{1,\ldots,{2^{n}}\}$ . On the other hand, the number of such infixes is limited by the size of any compression, as shown in the following claim (which is similar to the so-called $m k$ -lemma from [12, Lemma 3]).

Claim 14.

Let $a, b, c$ be distinct letters. If a string $w$ has a compression of size $m$ , then

\displaystyle|\{i\ |\begin{tabular}[]{l}$w$ contains an infix of the form $ab^% {i}c$\end{tabular}\}|\leq m.

Proof.

Consider a variable x in a straight-line program, which is defined by the rule x := y $\cdot$ z, where each of y and z is either a previously defined variable, or a letter, or the empty string $\varepsilon$ . Define the contribution of variable x to be

\displaystyle\{i\ |\begin{tabular}[]{l}$ab^{i}c$ is an infix of {x}, but is % not an infix of {y} or {z}\end{tabular}\}.

The key observation is that this contribution contains at most one number $i$ . This will imply the claim, since the set in the claim is the union of all contributions of variables in the program. To see why the variable contributes at most one number, observe that the infix $ab^{i}c$ is either contained in y, or contained in z, or it crossed the boundary between y and z. In the first two cases, it is not counted in the contribution of x. In the last case, there is exactly one value of $i$ for which this can happen, namely the number of $b$ ’s between the last $a$ in y and the first $c$ in z. $\hfill\vartriangleleft$ Claim 14 together with the fact that $w_{n}$ contains all infixes $ba^{i}\underline{a}$ for every $1\leq i\leq 2^{n}$ immediately yields the lemma. $\hfill\blacktriangleleft$

2.5 Rectangular polyregular functions

As we have seen above, marked squaring is a polyregular function that is not compatible with compression. A natural idea to overcome this problem is to consider the weaker notion of squaring from Example 4,

\displaystyle 123\quad\mapsto\quad 123123123,

which does not have the underlines, and which is compatible with compression. We can, however, do a bit better.

Example 15 (rectangle).

The essential idea behind this function is that it takes a lexicographic product of two input strings, as illustrated in the following example:

\displaystyle(123,abcd)\quad\mapsto\quad 1abcd2abcd3abcd.

(2)

This can be seen as a generalization of squaring, since squaring is obtained by taking both input strings to be the same and then removing the letters from the first string. Since for the moment we want to work with functions that input strings (and not pairs of strings), we will view the rectangle function as a string-to-string function in the following way. There are two disjoint alphabets $A$ and $B$ , and the function has type

\displaystyle(A+B)^{*}\to(A+B)^{*}.

If the input is not of the form $A^{*}B^{*}$ , then the output is the empty string. Otherwise, the input is split into two strings, and then we apply the rectangle operation as above. (An alternative definition, which would not change the results below, would be to untangle the input string over alphabet $A+B$ into two strings, by projecting onto the respective alphabets. We choose the previous definition to underline the fact that we are only interested in inputs where the two parts are clearly separated.)

Let us show that the rectangle function is compatible with compression. Suppose that we are given a compression of some string over alphabet $A+B$ . We can first check in polynomial time if this string is in $A^{*}B^{*}$ ; this can be done because membership in a regular language can be checked in polynomial time for compressed inputs [31]. Next, we extract in polynomial time compressions for the two parts of the input string, one in $A^{*}$ and one in $B^{*}$ ; this can be done by removing the nonterminals from the unused part of the alphabet. Finally, in the compression for the first string from $A^{*}$ , we insert a copy of the compression for the second string from $B^{*}$ after each terminal symbol. $\lrcorner$

As we have mentioned after Theorem 10, adding any function compatible with compression to the basic functions in the theorem will lead to a class that is compatible with compression. We believe – with some justification presented in Section 3 – that the particular choice of the rectangle function is worthwhile, hence the following definition.

Definition 16 (rectangular polyregular functions).

Define the class of rectangular polyregular functions in the same way as the polyregular functions from Definition 12, except that marked squaring is replaced by the rectangle function from Example 15.

By design, this subclass is compatible with compression, as stated in the following theorem, which is proved using the same argument as for regular functions in Theorem 10.

Theorem 17.

Rectangular polyregular functions are compatible with compression.

Since the rectangle function is polyregular, it follows that the rectangular polyregular functions are a subclass of the polyregular functions. One corollary of Theorem 17 is that the rectangular polyregular functions are a proper subclass of the polyregular functions, since the latter are not necessarily compatible with compression, as shown by Lemma 13. This is stated in the following theorem, which also relates the classes to another known subclass of the polyregular functions, namely the comparison-free polyregular functions from [29] (this model will be explained in the proof of the theorem). The comparison-free polyregular functions are the model most closely related with the rectangular ones, and can be seen as an inspiration for their definition.

Theorem 18.

Comparison-free polyregular $\subsetneq$ rectangular polyregular $\subsetneq$ polyregular.

Proof.

We have already argued for the second inclusion and its strictness. Let us now define the class of comparison-free polyregular functions, and argue for the first inclusion. One of the definitions of this class, see [29, Theorem 6.1], is the same as in Definition 16, except that the map combinator is not included⁴⁴4Strictly speaking, [29, Theorem 6.1] does not use the rectangle function, but a similar one called comparison-free squaring. It is not hard to see that each of these two functions can be defined using the other. . This proves the first inclusion. This inclusion is also strict, since the comparison-free polyregular functions are not closed under map, see [29, Corollary 8.5]. $\hfill\blacktriangleleft$ By [29, Theorem 6.1], the class of comparison-free polyregular functions contains the class of regular functions. Hence, we also have the inclusion regular $\subsetneq$ rectangular polyregular.

The second separation in the above theorem, i.e. the separation between rectangular and general polyregular functions, was proved using compression arguments. We believe that this is an interesting and clean technique, and much simpler than the intricate pumping arguments used for other separations, such as the first one in the above theorem. We believe that this lends further credence to the usefulness of compression techniques in the study of string-to-string functions.

A normal form.

We conclude this section with a slightly different characterization of rectangular polyregular functions, which relies only on composition in the closure properties and does not use the map combinator. In the definition of the rectangular polyregular functions from Definition 16, map and function composition could be applied in alternation, e.g. we could apply map, followed by composition, followed by map, etc. The following lemma shows that such alternation is not necessary, since it is enough to compose functions, each of which is either rational, or map reverse, or map rectangle. Here, map reverse refers to the function obtained by applying the map combinator to the reverse function, and similarly for map rectangle. In other words, map can be pushed inside composition and is not nested.

Lemma 19.

Every rectangular polyregular function can be obtained as a composition of functions, each of which is either: (a) rational; or (b) map reverse; or (c) map rectangle.

Proof.

It is enough to show that the class of functions in the statement of the lemma has the closure properties from Definition 16. This class contains all rational functions, and it is closed under composition. It also contains reverse and rectangle, since these are subsumed by map reverse and map rectangle in the case where the separator symbol is not used. Moreover, we can also recover duplication, which can be obtained as follows:

\displaystyle w\quad\stackrel{{\scriptstyle\text{rational}}}{{\mapsto}}\quad 1% 2w\quad\stackrel{{\scriptstyle\text{rectangle}}}{{\mapsto}}\quad 1w2w\qquad% \stackrel{{\scriptstyle\text{rational}}}{{\mapsto}}\quad ww.

It remains to show that the class is closed under applying map. Map commutes with composition ( $\mathop{map}(f\circ g)=\mathop{map}(f)\circ\mathop{map}(g)$ ), and therefore it is enough to show that map can be applied to the atomic functions (a), (b) and (c) from the lemma. In other words, it is easy to see that map can be pushed inside composition, but it remains to be argued that it does not need to be applied twice. The class of rational functions is closed under applying map, and therefore we only need to show that applying map twice to reverse or rectangle yields a function as in the statement of the lemma. We only do this for the case of the rectangle, and we leave the case of reverse to the reader.

Suppose then that we apply map twice to the rectangle function. In this case, there are two separators: one for the outer map (which we denote using a vertical bar) and one for the inner map (which we denote using a comma). Here is an example

\displaystyle a01,bc234|de56|fg78,hij9\quad\mapsto\quad a01,b234c234|d56e56|f7% 8g78,h9i9j9.

This is implemented by using a map rectangle where both kinds of separators are treated in the same way. Formally speaking, we need to introduce a third separator (say $\#$ ), which is appended to both kinds of separators using a rational function, as in the following example:

\displaystyle a01,bc234|de56|fg78,hij9\quad\mapsto\quad a01,\#bc234|\#de56|\#% fg78,\#hij9.

Next, we apply map rectangle with the new separator, which yields

\displaystyle a01,\#b234|c234|\#d56|e56|\#f78,g78,\#h9i9j9.

From this we obtain the correct output by removing every comma or $|$ that does not directly follow a $\#$ and finally removing every $\#$ . This is a regular function. $\hfill\blacktriangleleft$

3 A functional programming language

We think that the rectangular polyregular functions are interesting in their own right, and not just some random subclass of the polyregular functions that is compatible with compression. In particular, one could ask if the converse implication of Theorem 17 also holds: if a polyregular function is compatible with compression, then it is rectangular polyregular. We are not aware of any counterexample to the converse implication, but proving it seems difficult, and we leave it for future work.

In this section, we give other evidence for the importance of rectangular polyregular functions, by presenting a functional programming language which is equivalent to them. This functional programming language is based on a similar one that was given for the general polyregular functions in [7, Section 4.1]. Before giving a formal definition, we present some example programs.

Example 20 (duplication, squaring and rectangle).

Let us begin with a program in a Haskell-like language that implements the duplication function from Example 2 (we use blue superscripts to indicate the types of variables and auxiliary functions; occasionally we will also omit these types):

\displaystyle\lambda x^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{*}}}.\ \mathtt{concat}^{{\color[rgb% ]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}A^{**}\to A^{*}}}[x,x].

Here, the function $\mathtt{concat}$ concatenates a list of lists into a single list. Next, we write a program that implements the squaring function from Example 4.

\displaystyle\lambda x^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{*}}}.\ \mathtt{concat}^{{\color[rgb% ]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}A^{**}\to A^{*}}}(\mathtt{map}^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }(A\to A^{*})\to A^{*}\to A^{**}}}\ (\lambda y^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A}}.\ x)\ x)

The subprogram $\mathtt{map}\ (\lambda y.\ x)\ x$ applies the function $\lambda y.\ x$ to each list element of $x$ , which means that each letter in the list $x$ will be replaced by the list $x$ itself. For example, if the input to this subprogram is $[1,2,3]$ , then its output will be the nested list $[[1,2,3],[1,2,3],[1,2,3]]$ . The nesting is then removed by the $\mathtt{concat}$ function. Using the similar program

\lambda x^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}% {rgb}{0,0.6796875,0.9375}A^{*}}}.\ \lambda y^{{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{*}}}.\ \mathtt{% concat}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.6796875,0.9375}A^{**}\to A^{*}}}(\mathtt{map}^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }(A\to A^{*})\to A^{*}\to A^{**}}}\ (\lambda z^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A}}.\ \mathtt{concat}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{**}\to A^{*}}}[[z],y])\ x),

(3)

we can implement a variant of the rectangle function from Example 15, in which the input consists of two strings. Here, the subprogram $\mathtt{map}\ (\lambda z.\ \mathtt{concat}[[z],y])\ x$ applies the function $\lambda z.\ \mathtt{concat}[[z],y]$ to each list element of $x$ , which means that every list item $z$ in $x$ is replaced by $\mathtt{concat}[[z],y]$ . For instance, for $x=[a,b]$ and $y=[1,2,3]$ we obtain

[\mathtt{concat}[[a],[1,2,3]],\mathtt{concat}[[b],[1,2,3]]]=[[a,1,2,3],[b,1,2,% 3]].

The outermost application of $\mathtt{concat}$ in (3) flattens this nested list into $[a,1,2,3,b,1,2,3]$ . $\lrcorner$

We now give a formal definition of the programming language in detail. It is called the polyregular $\lambda$ -calculus, and its purpose is to define exactly the polyregular functions.

3.1 Syntax

The polyregular $\lambda$ -calculus is a variant of the simply typed $\lambda$ -calculus, and therefore its programs are a certain kind of $\lambda$ -terms. We will use the word programs for these terms, or programs of the polyregular $\lambda$ -calculus in case there is some ambiguity about the kind of programs in consideration. The programs use variables, which are taken from an infinite set of variables. Both programs and variables have associated types, which are unique, i.e. the same variable or program cannot be associated with two different types (as in Church typing). We indicate the types using blue superscripts. The types are built using the following type constructors:

\displaystyle\underbrace{1}_{\text{a set with one element}}\qquad\underbrace{A% \times B}_{\text{product}}\qquad\underbrace{A+B}_{\text{disjoint union}}\qquad% \underbrace{A^{*}}_{\text{lists}}\qquad\underbrace{A\to B}_{\text{functions}}

Here is the inductive definition of the syntax of the programs.

3.1.1 Variables, application and abstraction

We begin with the basic elements of the $\lambda$ -calculus: each variable $x$ is a program, and we can construct programs using application and $\lambda$ -abstraction:

\displaystyle\frac{M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A\to B}}\quad N^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A}}}{(M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.6796875,0.9375}A\to B}}N^{{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}})^{{\color[rgb]% {0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}B}}}\text{\ (application)}\qquad\frac{\overbrace{x^{{\color% [rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}A}}}^{\text{variable}}\quad M^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }B}}}{(\lambda x^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}}.\ M^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }B}})^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb% }{0,0.6796875,0.9375}A\to B}}}\text{\ ($\lambda$-abstraction)}

The descriptions above should be read as usual in the $\lambda$ -calculus, with premises above the line and the conclusion below it.

3.1.2 Data constructors and destructors

Next, the programming language has features to access the data types for pairs, co-pairs, lists, and the atomic unit type $1$ . For the unit type, there is a program of this type, which generates the unique value in this type; this program is denoted by $()$ . For the remaining type constructors, there are data constructors described as follows:

	$\displaystyle\frac{M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}}\quad N^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }B}}}{(M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0.6796875,0.9375}A}},N^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}B}})^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A\times B}}}\text{\ (pair)}$	$\displaystyle\quad\frac{M_{1}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}}\quad\cdots\quad M_{n}^{{% \color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0.6796875,0.9375}A}}}{[M_{1}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}},\ldots,M_{n}^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A}}]^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb% }{0,0.6796875,0.9375}A^{*}}}}\text{\ (list)}$
	$\displaystyle\frac{M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}}}{(\mathtt{Left}^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }A\to A+B}}M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A}})^{{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A+B}}}\text{\ (% left co-pair)}$	$\displaystyle\quad\frac{M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0.6796875,0.9375}B}}}{(\mathtt{Right}^{{\color[rgb]{% 0,0.6796875,0.9375}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375% }B\to A+B}}M^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0.6796875,0.9375}B}})^{{\color[rgb]{0,0.6796875,0.9375}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A+B}}}\text{\ (% right co-pair)}$

In the rule list, the program $[]$ is also allowed, representing the empty list. Observe that in the data constructors for co-pairs, the other type $B$ (respectively, $A$ ) is part of the syntax, since it cannot be inferred from the argument $M$ .

We also have atomic programs for deconstructing data:

	$\displaystyle\mathtt{fst}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A\times B\to A}}$
	$\displaystyle\mathtt{snd}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A\times B\to B}}$
	$\displaystyle\mathtt{uncons}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{}\to 1+A\times A^{}}}$
	$\displaystyle\mathtt{either}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}(A\to C)\to(B\to C)\to(A+B)\to C}}$

Here, $\mathtt{fst}$ and $\mathtt{snd}$ are the destructors for the pair constructor, $\mathtt{uncons}$ is the destructor for lists and $\mathtt{either}$ is the destructor for the co-pair constructors $\mathtt{Left}$ and $\mathtt{Right}$ .

The above list of programs is not finite, since each program represents a family of programs, which is parameterized by the choice of types $A, B, C$ .

3.1.3 List processing

The polyregular $\lambda$ -calculus does not have any mechanisms for recursion, iteration, or even a fold function⁵⁵5The omission of the fold function is discussed at length in [8].. For this reason, computation on lists of unbounded length must be done using dedicated atomic programs. These are listed below (again, the list is infinite, since each program is parameterized by a choice of types $A, B$ ):

	$\displaystyle\mathtt{reverse}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{}\to A^{}}}$
	$\displaystyle\mathtt{concat}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{*}\to A^{}}}$
	$\displaystyle\mathtt{map}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0.6796875,0.9375}(A\to B)\to A^{}\to B^{}}}$
	$\displaystyle\mathtt{split}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{}\to(A^{}\times A^{})^{}}}$
	$\displaystyle\mathtt{block}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}(A+B)^{}\to A^{}\times(B% \times A^{})^{}}}\qquad$

3.1.4 Rational functions

For all finite types $A$ and $B$ and every rational function $A^{*}\to B^{*}$ , we have a corresponding atomic program⁶⁶6In fact, for expressive completeness, it is enough to have only very special rational functions that evaluate the group operation in a finite group, see [7, Figure 1]. This is because all other rational functions can be derived using the group operation and the part of the programming language from Sections 3.1.1–3.1.3. However, for simplicity of exposition, we use the more powerful construction that allows all rational functions, which does not affect the expressive power of the programming language. It is worth pointing out that if we do not explicitly add the rational functions, and keep only items from Sections 3.1.1–3.1.3, then we still get a reasonable class of functions, called the first-order polyregular functions [6, Theorem 4.4]..

3.2 Semantics

The only part of the polyregular $\lambda$ -calculus that is not completely standard is the two functions $\mathtt{split}$ and $\mathtt{block}$ , so we begin by explaining those. The function $\mathtt{split}$ is used to split a list into all possible (prefix, suffix) pairs, sorted by increasing prefixes, as explained in this example

[1,2,3]\quad\mapsto\quad[([],[1,2,3]),([1],[2,3]),([1,2],[3]),([1,2,3],[])].

(4)

The function $\mathtt{block}$ inputs a list which has elements of two kinds, and collects into blocks the consecutive elements of the first kind, as explained in the following example, in which $A$ is letters and $B$ is digits:

[a,b,1,c,d,e,2,3,f]\quad\mapsto\quad([a,b],[(1,[c,d,e]),(2,[]),(3,[f])]).

(5)

Having defined these two functions, the rest of the semantics is defined in the standard way. In fact, the programming language can be seen as a fragment of Haskell. Nevertheless, we give a brief explanation of the semantics to make this paper relatively self-contained, and also because the semantics are much simpler than those of a full-fledged programming language such as Haskell. Each type $A$ comes with a semantic domain, written by $[\![A]\!]$ , which is meant to describe the values of programs that have this type. The semantic domain is defined naively by induction on the type structure, with the type constructors having the expected meaning. In particular, $[\![A\to B]\!]$ is defined to be all (total) functions from $[\![A]\!]$ to $[\![B]\!]$ , which is appropriate to our language since it can only define always-terminating functions. If a program has free variables of types $A_{1},\ldots,A_{n}$ , and the program itself has type $A$ , then its semantics will be a function

\displaystyle\underbrace{[\![A_{1}]\!]\times\cdots\times[\![A_{n}]\!]}_{\text{% values of the free variables}}\quad\to\quad\underbrace{[\![A]\!]}_{\text{value% of the program}},

which is defined by induction on the structure of the program in the expected way. If the program is closed, i.e. it has no free variables, then its semantics will be in $[\![A]\!]$ . This completes the definition of the polyregular $\lambda$ -calculus.

3.3 String-to-string functions

We are mainly interested in closed programs that define string-to-string functions, as we now explain. Every finite alphabet can be represented as a type, e.g. $1+1+1$ can be seen as representing an alphabet with three letters⁷⁷7The choice of representation is not important, since if we have two finite types of the same cardinality, then the bijection between them can be realised using a program. Here, a finite type is one whose semantics is a finite set, which is the same as saying that the list constructor is not used.. Therefore, by abuse of notation, we will identify finite alphabets and finite types. Under this identification, our programming language defines exactly the polyregular functions.

Theorem 21 ([7, Theorem 4.1]).

Let $A$ and $B$ be finite alphabets. Then

\displaystyle f:A^{*}\to B^{*}

is polyregular if and only if it can be defined in the polyregular $\lambda$ -calculus.

The purpose of this section is to identify the subclass which corresponds to the rectangular polyregular functions. This is done in the following theorem, which identifies the $\mathtt{split}$ function as the only obstruction.

Theorem 22.

Let $A$ and $B$ be finite alphabets. Then

\displaystyle f:A^{*}\to B^{*}

is rectangular polyregular if and only if it can be defined in the polyregular $\lambda$ -calculus without using $\mathtt{split}$ .

Proof.

We will use the name split-free program for programs of the polyregular $\lambda$ -calculus that do not use the split function. We begin with the easier inclusion, namely

\displaystyle\text{rectangular polyregular}\;\subseteq\;\text{split-free % programs}.

The split-free programs contain all rational functions by definition, and they are easily seen to be closed under composition, as witnessed by the program $\lambda w.\ M\ (N\ w).$ Also, they are closed under map and reverse, since both of these are included as atomic programs. Duplication and rectangle were treated in Example 20. This completes the proof of the first inclusion.

The rest of this proof is devoted to the converse inclusion, namely

\displaystyle\text{split-free programs}\;\subseteq\;\text{rectangular % polyregular}.

This proof is much longer, and it follows the same lines as the proof of the corresponding inclusion for the (not necessarily rectangular) polyregular functions in [7, Theorem 4.1]. The general idea is to write down a program as a string, and to then evaluate it by using string rewriting. If done carefully, the evaluation can be done by a rectangular polyregular function.

String representation of programs.

We begin by explaining how programs are represented as strings. This is the usual representation, which we have already used above when writing example programs. In this representation, we assume that the variable names and the atomic programs are single letters. In particular, the alphabet is infinite, since there are infinitely many variables and infinitely many atomic programs. (There are infinitely many atomic programs since the type annotation is important. For example, different letters will be used for $\mathtt{concat}$ depending on the type $A$ that is involved.) If we pick some convention on writing parentheses, then the string representation can be made unique, so that each program has a unique string representation.

A problem with the string representation that was described above is that the alphabet is infinite. This will be a problem if we want to manipulate string representations using rectangular polyregular functions, which work on finite alphabets. For this reason, we will assume that there is a fixed finite set of variables and atomic programs that can be used, and we will only work with programs that are subject to this restriction.

Another problem is that programs with deep syntax trees will be difficult to handle in their string representation. The syntax of the polyregular $\lambda$ -calculus is defined inductively, and therefore each program has a corresponding syntax tree, in which nodes are labelled by term constructors. Here is a picture of such a syntax tree for a program which applies $\mathtt{concat}$ to a doubly nested list of type $1^{**}$ :

The height of a syntax tree is defined to be the maximal number of edges on a root-to-leaf path (in the above picture, the height is three), and the height of a program is defined to be the height of its syntax tree. It turns out that a polyregular function cannot deal with trees of unbounded height, since it is essentially a finite automaton, and finite automata on strings cannot handle trees of unbounded height. For this reason, we will impose a bound on the height of programs.

The assumptions discussed above are summarised in the following definition.

Definition 23.

Define a resource bound to be a triple consisting of

(a)

a finite set of variables,
(b)

a finite set of atomic programs and
(c)

a height bound in $\{1,2,\ldots\}$ .

We say that a program is consistent with a resource bound if its variables are contained in the set from item (a), its atomic programs are contained in the set from item (b), and its height is at most the number from item (c). If we fix a resource bound, then programs consistent with this resource bound can be written as strings over a finite alphabet (for this, the height bound is unimportant). Furthermore, the set of strings that are representations of programs is a regular language over this alphabet (for this, the height bound is important).

	$\displaystyle(\lambda x.M)\ N$	$\displaystyle\ \leadsto\ M[x:=N]$
	$\displaystyle\mathtt{fst}(M,N)$	$\displaystyle\ \leadsto\ M$
	$\displaystyle\mathtt{snd}(M,N)$	$\displaystyle\ \leadsto\ N$
	$\displaystyle\mathtt{uncons}[]$	$\displaystyle\ \leadsto\ \mathtt{Left}()$
	$\displaystyle\mathtt{uncons}[M_{1},\ldots,M_{n}]\text{ for $n\geq 1$}$	$\displaystyle\ \leadsto\ \mathtt{Right}(M_{1},[M_{2},\ldots,M_{n}])$
	$\displaystyle\mathtt{either}\ M_{1}\ M_{2}\ (\mathtt{Left}\ N)$	$\displaystyle\ \leadsto\ M_{1}\ N$
	$\displaystyle\mathtt{either}\ M_{1}\ M_{2}\ (\mathtt{Right}\ N)$	$\displaystyle\ \leadsto\ M_{2}\ N$
	$\displaystyle\mathtt{reverse}[M_{1},\ldots,M_{n}]$	$\displaystyle\ \leadsto\ [M_{n},\ldots,M_{1}]$
	$\displaystyle\mathtt{concat}[[M^{1}_{1},\ldots,M^{1}_{n_{1}}],\ldots,[M^{k}_{1% },\ldots,M^{k}_{n_{k}}]]$	$\displaystyle\ \leadsto\ [M^{1}_{1},\ldots,M^{k}_{n_{k}}]$
	$\displaystyle\mathtt{map}\ M\ [N_{1},\ldots,N_{n}]$	$\displaystyle\ \leadsto\ [M\ N_{1},\ldots,M\ N_{n}]$
	$\displaystyle\mathtt{split}\ [M_{1},\ldots,M_{n}]$	$\displaystyle\ \leadsto\ \text{result as in \eqref{def-split}}$
	$\displaystyle\mathtt{block}\ [M_{1},\ldots,M_{n}]$	$\displaystyle\ \leadsto\ \text{result as in \eqref{def-block}}$
	$\displaystyle f[M_{1},\ldots,M_{n}]$	$\displaystyle\ \leadsto\ \text{output of the rational function $f$}$

Figure 1: Reduction rules. The last rule is for an atomic program

f

that is a rational function. In the last rule, we assume that the list elements

M_{1},\ldots,M_{n}

, which have some finite type, are already been evaluated, i.e. they are built only using the data constructors for the finite types, which are

()

, pairing and co-pairing.

Reduction.

So far, we have explained how a program can be written as a string over a finite alphabet. We now explain how programs can be evaluated under this representation. When defining the semantics of the polyregular $\lambda$ -calculus, we used a denotational approach, defined by induction on the syntax. In this proof, we use an approach based on rewriting, where a program is executed by applying syntactic reduction rules. Arguably the most important rule is $\beta$ -reduction, which substitutes an argument for a variable (we omit the blue superscripts with types to improve readability):

\displaystyle(\lambda x.M)\ N\;\leadsto\;M[x:=N].

(6)

The complete list of reduction rules is shown in Figure 1. It is easy to see that applying a reduction rule changes neither the type nor the semantics of a program. A program is in normal form if no reduction rules can be applied to it. The normal form is unique, up to renaming of bound variables [34, Corollary 1.4.9]. If a closed program represents a string, i.e. its type is $A^{*}$ for some finite type, then its normal form is necessarily a list of elements of $A$ . Therefore, for closed programs that have such a type $A^{*}$ , normal forms and their string representations are essentially the same thing.

The key lemma in the proof is the following, which shows that a rectangular polyregular function can perform term substitution, as used in the $\beta$ -reduction rule from (6). In the proof of the lemma, we use the rectangle function from Example 15.

Lemma 24.

Fix a resource bound ${\mathcal{R}}$ . There is a rectangular polyregular function which does the following, with programs represented as strings:

$\blacksquare$

Input: a program of the form $(\lambda x.M)\ N$ , which is consistent with ${\mathcal{R}}$ ;
$\blacksquare$

Output: the program $M[x:=N]$ .

Proof.

Thanks to the resource bound, there are finitely many possible choices for the variable $x$ , and therefore we can think of this variable as being fixed.

Since there is a fixed bound on the height of the input program, a rational function can use a stack of bounded height to label each position in the string representation with the distance of this position from the root of the syntax tree. Using this stack, we can also identify the closing bracket $)$ that is just before $N$ , by matching it with the opening bracket at the beginning of the term. This way, we can isolate the part of the input which represents the program $N$ .

Next, we use the rectangle function to insert a copy of the string representation of the program $N$ after every letter in the string representation of the program $M$ . Then, we can use a rational function to keep only the copies which are necessary, i.e. those that immediately follow an occurrence of the variable $x$ . $\hfill\blacktriangleleft$ The above lemma is the only place where our proof differs from the one in [7]. Essentially, the content of the above lemma is the observation that a weaker mechanism than the full polyregular functions, namely the rectangle function, is sufficient to implement term substitution.

A reduction strategy.

The rest of this proof follows the same lines as the one in [7, Theorem 4.1]. Define a redex in a program to be a node in its syntax tree to which a reduction rule can be applied. A redex can also be seen as an infix of the string representation of the program. Here is an example of a program with some (in fact, all) redexes underlined:

\displaystyle[\underbrace{(\lambda x.x)[]}_{\text{a redex for $\lambda$-% abstraction}},[],[],\underbrace{\mathtt{map}(\lambda x.x)[[],[],[]]}_{\text{a % redex for $\mathtt{map}$}},\underbrace{\mathtt{fst}([],())}_{\text{a redex for% $\mathtt{fst}$}}].

Usually in the $\lambda$ -calculus, one chooses a reduction strategy which picks some redex, reduces it, and then repeats this process. However, in the current proof, we will need to use a more general notion of reduction strategy, which allows reducing several redexes in parallel. This will allow us to reduce a program to normal form in constant time, once resource bounds are fixed. Define a parallel reduction strategy to be a function which assigns to each term a subset of its redexes, such that the redexes are pairwise non-overlapping (i.e. the corresponding infixes in the string representation do not overlap). The result of applying such a strategy to a program is obtained by reducing all the selected redexes in parallel, which can be done since the redexes are assumed to be non-overlapping. The following lemma shows that, once the resource bounds are fixed, there is a parallel reduction strategy which leads to the normal form in a bounded number of steps.

Lemma 25 ([6, Lemma 8.6]).

Fix a resource bound ${\mathcal{R}}$ . There exist

1.

a parallel reduction strategy and
2.

a time bound $k\in\{1,2,\ldots\}$

such that for every program consistent with the resource bound, applying the reduction strategy $k$ times leads to a term in normal form. Furthermore, the reduction strategy can be implemented by a rational function, with the redexes marked in the output using begin/end markers.

The above lemma was proved in [6] for the (not necessarily rectangular ) polyregular $\lambda$ -calculus, but it remains valid for any fragment of this language, such as the split-free fragment that we are considering here.

We now put the above results together to conclude that split-free programs can be evaluated using rectangular polyregular functions, as stated in the following corollary.

Corollary 26.

Fix a resource bound ${\mathcal{R}}$ . There is a rectangular polyregular function which does the following, with programs represented as strings:

$\blacksquare$

Input: a split-free program $M$ consistent with ${\mathcal{R}}$ ;
$\blacksquare$

Output: a program in normal form obtained from $M$ by applying reductions.

Proof.

Fix the $k$ and the parallel reduction strategy from Lemma 25; these only depend on the resource bound and not on the input program. Then the given split-free program $M$ can be reduced to normal form by repeating the following process $k$ times:

(1)

mark a pairwise non-overlapping set of redexes in $M$ using the rational function from the parallel reduction strategy;
(2)

reduce the marked redexes in parallel ⁸⁸8Note that during this process the height of the syntax trees may increase (for instance, due to $\lambda$ -abstraction), and, hence, the resource bound may not be preserved. This is not a problem. It is only important that the initial input program $M$ is consistent with the resource bound ${\mathcal{R}}$ . Then Lemma 25 guarantees that $k$ repetitions of the parallel reduction strategy yield a normal form, even if thereby the height of the syntax tree increases..

Since the rectangular polyregular functions are closed under composition and contain the rational ones, it remains to prove that part (2) of the process can be implemented using a rectangular polyregular function.

We first argue that a single redex can be reduced by a rectangular polyregular function. For redexes corresponding to $\lambda$ -abstraction, this was proved in Lemma 24. Let us now consider the remaining kinds of redexes, which correspond to the reduction rules in Figure 1, except for $\mathtt{split}$ , which has been removed in the rectangular fragment that we are considering. Consider first the reduction rule for $\mathtt{map}$ , which is

\displaystyle\mathtt{map}\ M\ [N_{1},\ldots,N_{n}]\quad\leadsto\quad[M\ N_{1},% \ldots,M\ N_{n}].

This reduction rule can be evaluated similarly to the proof of Lemma 24, by using the rectangle function to copy the program $M$ into each of the $n$ list elements. The reduction rule for reverse can be implemented by a regular function, and the remaining reduction rules are even rational. This completes the proof that a single redex can be reduced by a rectangular polyregular function.

Our reduction strategies are parallel, which means that multiple redexes need to be reduced in one step. However, since these redexes are non-overlapping, the parallel execution corresponds to using the map combinator from Section 2.2. Since this combinator is part of the definition of the rectangular polyregular functions, we can complete the proof of (2), and therefore also the proof of the corollary. $\hfill\blacktriangleleft$ Using the above corollary, we complete the proof of the inclusion

\displaystyle\text{split-free programs}\;\subseteq\;\text{rectangular % polyregular}.

Fix a split-free program $M$ of type $A^{*}\to B^{*}$ . The output string is computed as follows: (a) given an input string in $A^{*}$ , replace it by a term of the form $M N$ , where $N$ is a program that represents the input string; (b) reduce the term $M N$ to normal form; (c) extract the output string from the normal form. Each of these steps can be computed by a rectangular polyregular function, which completes the proof of the inclusion. Indeed, (b) is a rectangular polyregular function by Corollary 26, while steps (a) and (c) can even be implemented using rational functions, since there is very little difference between strings over a finite alphabet $A$ and the string representations of the corresponding programs of type $A^{*}$ that are in normal form. $\hfill\blacktriangleleft$

3.4 Programs with combinators instead of $\lambda$ -abstraction

We finish this section with another characterisation of the rectangular polyregular functions. This is a variant of a characterisation of the polyregular functions, see [6, Section 4], which is similar to the polyregular $\lambda$ -calculus, but uses a programming language that is based on combinators instead of $\lambda$ -abstraction. A nice feature of this characterisation is that it highlights the role of the strength function

	$\displaystyle\mathtt{strength}:A\times B^{*}$	$\displaystyle\to(A\times B)^{*}$		(7)
	$\displaystyle(a,[b_{1},\ldots,b_{n}])$	$\displaystyle\mapsto[(a,b_{1}),\ldots,(a,b_{n})],$

which is an important function that arises in category theory, especially in the context of monads.

In the programming language discussed now, we will not have higher-order functions. We will only authorise functions of type $A\to B$ , where both input and output types are arrow-free, i.e. they are constructed using only the unit, product, disjoint union and list type constructors. In type theory, such functions are said to have first-order function type, but we avoid this terminology here, since it may be confused with first-order logic, which also plays a role in the study of polyregular functions.

The idea behind the programming language is to start with a set of atomic functions, which have types of the form $A\to B$ with arrow-free $A$ and $B$ , and then to close this set under certain combinators, namely

	$\displaystyle\frac{f_{1}:A_{1}\to B\quad f_{2}:A_{2}\to B}{f_{1}+f_{2}:A_{1}+A% _{2}\to B}\text{\ (co-product)}\qquad$	$\displaystyle\frac{f:A\to B_{1}\quad g:A\to B_{2}}{(f,g):A\to B_{1}\times B_{2% }}\text{\ (product)}$
	$\displaystyle\frac{f:A\to B\quad g:B\to C}{g\circ f:A\to C}\text{\ (% composition)}\qquad$	$\displaystyle\frac{f:A\to B}{\mathtt{map}\ f:A^{}\to B^{}}\text{\ (map)}.$

Depending on the choice of the initial set of atomic functions, one can obtain various classes of string-to-string functions. In [9, Section 6], one can find a choice that leads to the so-called regular functions, which are a well known transducer class. If one adds the function $\mathtt{split}$ (formally speaking, the variant of this function for all possible arrow-free types $A$ ), then one gets exactly the polyregular functions. As we show below, replacing $\mathtt{split}$ by strength leads to the rectangular polyregular functions.

Theorem 27.

Let $A$ and $B$ be finite alphabets. A string-to-string function

\displaystyle f:A^{*}\to B^{*}

is rectangular polyregular if and only if it belongs to the least class of functions which:

1.

is closed under the combinators for co-product, product, composition and map;
2.

contains the atomic functions for the regular functions, as in [9, Section 6];
3.

contains, for all arrow-free types $A$ and $B$ , the strength function explained in (7).

Proof.

It is enough to show that the class of functions from this theorem sits between the two equal classes from Theorem 22:

\displaystyle\text{rectangular polyregular}\;\subseteq\;\text{functions from % this theorem}\;\subseteq\;\text{split-free programs}.

The second inclusion is essentially immediate, since all functions from items 2 and 3 in this theorem can easily be defined using split-free programs, and split-free programs have the closure properties from item 1. (For item 2, one needs to consult the list of atomic functions in [9], but we assure the reader that this is a simple check.) Consider now the first inclusion. Since the functions from this theorem are closed under composition, it is enough to show that they contain the atomic functions from Lemma 19, namely the rational functions, map reverse and map rectangle. As shown in [9, Theorem 6.1], even without using the strength function, one can derive all regular string-to-string functions, which contain both rational functions and map reverse. We are left with map rectangle, which is easily derived using the strength function and map. $\hfill\blacktriangleleft$

4 Conclusions

We have studied string-to-string transducers which are compatible with compression, i.e. they can be evaluated in polynomial time from compressed inputs. A necessary condition is having outputs of polynomial size, and therefore we have focused on the polyregular functions.

1.

Are the rectangular polyregular functions exactly the polyregular functions that are compatible with compression?
2.

Can one decide if a given polyregular function is rectangular?
3.

Can the rectangular polyregular functions be characterised in terms of logic? Such a characterisation exists for the general polyregular functions; these are exactly the mso interpretations [10, Theorem 7]. For the rectangular ones a promising idea is to consider the interpretations based on [29, Conjecture 10.1]: Starting with a word $w$ represented in the usual way as a structure, one first takes a $k$ -fold product of this structure with itself, and then applies a $1$ -dimensional MSO-interpretation that produces the output word. Conjecture 10.1 from [29] was originally made for the weaker class of comparison-free polyregular functions, but it has been refuted [23, Theorem 4.6]. However, it might still be appropriate for the rectangular polyregular functions.
4.

Can the rectangular polyregular functions be characterised in terms of an imperative programming language, such as the for-transducers from [7, Section 1]?

It is a tantalising possibility that the answers to all these questions are positive.

References

[1] Rajeev Alur and Pavol Cerný. Expressiveness of streaming string transducers. In Kamal Lodaya and Meena Mahajan, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, volume 8 of LIPIcs, pages 1–12. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2010. doi:10.4230/LIPIcs.FSTTCS.2010.1.
[2] Frédérique Bassino, Ilya Kapovich, Markus Lohrey, Alexei Miasnikov, Cyril Nicaud, Andrey Nikolaev, Igor Rivin, Vladimir Shpilrain, Alexander Ushakov, and Pascal Weil. Compression techniques in group theory. In Complexity and Randomness in Group Theory, chapter 4. De Gruyter, 2020. doi:10.1515/9783110667028-004.
[3] Jean Berstel. Transductions and context-free languages. Springer-Verlag, 2013. doi:10.1007/978-3-663-09367-1.
[4] Jean Berstel and Srecko Brlek. On the length of word chains. Information Processing Letters, 26(1):23–28, 1987. doi:10.1016/0020-0190(87)90031-7.
[5] Alberto Bertoni, Christian Choffrut, and Roberto Radicioni. Literal shuffle of compressed words. In Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, volume 273 of IFIP, pages 87–100. Springer, 2008. doi:10.1007/978-0-387-09680-3_6.
[6] Mikołaj Bojańczyk. Polyregular functions, 2018. arXiv:1810.08760.
[7] Mikołaj Bojańczyk. Transducers of polynomial growth. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22. ACM, 2022. doi:10.1145/3531130.3533326.
[8] Mikołaj Bojańczyk. Folding interpretations. In Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175796.
[9] Mikołaj Bojańczyk, Laure Daviaud, and Shankara Narayanan Krishna. Regular and First-Order List Functions. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 125–134. ACM, 2018. doi:10.1145/3209108.3209163.
[10] Mikolaj Bojanczyk, Sandra Kiefer, and Nathan Lhote. String-to-string interpretations with polynomial-size output. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, volume 132 of LIPIcs, pages 106:1–106:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.ICALP.2019.106.
[11] Mikołaj Bojańczyk and Rafał Stefański. Single-use automata and transducers for infinite alphabets. In Proceedings of the 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, volume 168 of LIPIcs, pages 113:1–113:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.ICALP.2020.113.
[12] Moses Charikar, Eric Lehman, Ding Liu, Rina Panigrahy, Manoj Prabhakaran, Amit Sahai, and Abhi Shelat. The smallest grammar problem. IEEE Transactions on Information Theory, 51(7):2554–2576, 2005. doi:10.1109/TIT.2005.850116.
[13] Francisco Claude, Gonzalo Navarro, and Alejandro Pacheco. Grammar-compressed indexes with logarithmic search time. Journal of Computer and System Sciences, 118:53–74, 2021. doi:10.1016/j.jcss.2020.12.001.
[14] Samuel Eilenberg. Automata, Languages, and Machines. Vol. A. Academic Press [A subsidiary of Harcourt Brace Jovanovich, Publishers], New York, 1974.
[15] Joost Engelfriet and Hendrik Jan Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic, 2(2):216–254, 2001. doi:10.1145/371316.371512.
[16] Joost Engelfriet and Heiko Vogler. Macro tree transducers. Journal of Computer and System Sciences, 31(1):71–146, 1985. doi:10.1016/0022-0000(85)90066-2.
[17] Paolo Ferragina and Giovanni Manzini. Indexing compressed text. Journal of the ACM, 52(4):552–581, 2005. doi:10.1145/1082036.1082039.
[18] Emmanuel Filiot and Pierre-Alain Reynier. Copyful streaming string transducers. In Proceedings of the 11th International Workshop on Reachability Problems, RP 2017, volume 10506 of Lecture Notes in Computer Science, pages 75–86. Springer, 2017. doi:10.1007/978-3-319-67089-8_6.
[19] Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polynomial-time algorithm for deciding equivalence of normed context-free processes. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, FOCS 1994, pages 623–631. IEEE Computer Society, 1994. doi:10.1109/SFCS.1994.365729.
[20] Artur Jeż. Approximation of grammar-based compression via recompression. Theoretical Computer Science, 592:115–134, 2015. doi:10.1016/J.TCS.2015.05.027.
[21] Artur Jeż. Faster fully compressed pattern matching by recompression. ACM Transactions on Algorithms, 11(3):20:1–20:43, 2015. doi:10.1145/2631920.
[22] Marek Karpinski, Wojciech Rytter, and Ayumi Shinohara. Pattern-matching for strings with short descriptions. In Proceedings of the 6th Annual Symposium on Combinatorial Pattern Matching, CPM 95, volume 937 of Lecture Notes in Computer Science, pages 205–214. Springer, 1995. doi:10.1007/3-540-60044-2_44.
[23] Sandra Kiefer, Lê Thành Dũng Nguyên, and Cécilia Pradic. Refutations of pebble minimization via output languages, 2023. arXiv:2301.09234.
[24] Yury Lifshits, Shay Mozes, Oren Weimann, and Michal Ziv-Ukelson. Speeding up HMM decoding and training by exploiting sequence repetitions. Algorithmica, 54(3):379–399, 2009. doi:10.1007/S00453-007-9128-0.
[25] Markus Lohrey. Leaf languages and string compression. Information and Computation, 209(6):951–965, 2011. doi:10.1016/J.IC.2011.01.009.
[26] Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241–299, 2012. doi:10.1515/GCC-2012-0016.
[27] Markus Lohrey. The Compressed Word Problem for Groups. SpringerBriefs in Mathematics. Springer, 2014. doi:10.1007/978-1-4939-0748-9.
[28] Kurt Mehlhorn, R. Sundar, and Christian Uhrig. Maintaining dynamic sequences under equality-tests in polylogarithmic time. In Proceedings of the 5th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 1994, pages 213–222. ACM/SIAM, 1994. URL: http://dl.acm.org/citation.cfm?id=314464.314496.
[29] Lê Thành Dung Nguyên, Camille Noûs, and Pierre Pradic. Comparison-free polyregular functions. In Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, volume 198 of LIPIcs, pages 139:1–139:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.ICALP.2021.139.
[30] Wojciech Plandowski. Testing equivalence of morphisms on context-free languages. In Proceedings of the 2nd Annual European Symposium on Algorithms, ESA 1994, volume 855 of Lecture Notes in Computer Science, pages 460–470. Springer, 1994. doi:10.1007/BFB0049431.
[31] Wojciech Plandowski and Wojciech Rytter. Complexity of language recognition problems for compressed words. In Juhani Karhumäki, Hermann A. Maurer, Gheorghe Paun, and Grzegorz Rozenberg, editors, Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 262–272. Springer, 1999. doi:10.1007/978-3-642-60207-8_23.
[32] Wojciech Rytter. Application of Lempel-Ziv factorization to the approximation of grammar-based compression. Theoretical Computer Science, 302(1–3):211–222, 2003. doi:10.1016/S0304-3975(02)00777-6.
[33] John C. Shepherdson. The reduction of two-way automata to one-way automata. IBM Journal of Research and Development, 3(2):198–200, April 1959. doi:10.1147/RD.32.0198.
[34] Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/149.

[bib.bib1] [1] Rajeev Alur and Pavol Cerný. Expressiveness of streaming string transducers. In Kamal Lodaya and Meena Mahajan, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, volume 8 of LIPIcs, pages 1–12. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2010. doi:10.4230/LIPIcs.FSTTCS.2010.1.

[bib.bib2] [2] Frédérique Bassino, Ilya Kapovich, Markus Lohrey, Alexei Miasnikov, Cyril Nicaud, Andrey Nikolaev, Igor Rivin, Vladimir Shpilrain, Alexander Ushakov, and Pascal Weil. Compression techniques in group theory. In Complexity and Randomness in Group Theory, chapter 4. De Gruyter, 2020. doi:10.1515/9783110667028-004.

[bib.bib3] [3] Jean Berstel. Transductions and context-free languages. Springer-Verlag, 2013. doi:10.1007/978-3-663-09367-1.

[bib.bib4] [4] Jean Berstel and Srecko Brlek. On the length of word chains. Information Processing Letters, 26(1):23–28, 1987. doi:10.1016/0020-0190(87)90031-7.

[bib.bib5] [5] Alberto Bertoni, Christian Choffrut, and Roberto Radicioni. Literal shuffle of compressed words. In Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, volume 273 of IFIP, pages 87–100. Springer, 2008. doi:10.1007/978-0-387-09680-3_6.

[bib.bib6] [6] Mikołaj Bojańczyk. Polyregular functions, 2018. arXiv:1810.08760.

[bib.bib7] [7] Mikołaj Bojańczyk. Transducers of polynomial growth. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22. ACM, 2022. doi:10.1145/3531130.3533326.

[bib.bib8] [8] Mikołaj Bojańczyk. Folding interpretations. In Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175796.

[bib.bib9] [9] Mikołaj Bojańczyk, Laure Daviaud, and Shankara Narayanan Krishna. Regular and First-Order List Functions. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 125–134. ACM, 2018. doi:10.1145/3209108.3209163.

[bib.bib10] [10] Mikolaj Bojanczyk, Sandra Kiefer, and Nathan Lhote. String-to-string interpretations with polynomial-size output. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, volume 132 of LIPIcs, pages 106:1–106:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.ICALP.2019.106.

[bib.bib11] [11] Mikołaj Bojańczyk and Rafał Stefański. Single-use automata and transducers for infinite alphabets. In Proceedings of the 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, volume 168 of LIPIcs, pages 113:1–113:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.ICALP.2020.113.

[bib.bib12] [12] Moses Charikar, Eric Lehman, Ding Liu, Rina Panigrahy, Manoj Prabhakaran, Amit Sahai, and Abhi Shelat. The smallest grammar problem. IEEE Transactions on Information Theory, 51(7):2554–2576, 2005. doi:10.1109/TIT.2005.850116.

[bib.bib13] [13] Francisco Claude, Gonzalo Navarro, and Alejandro Pacheco. Grammar-compressed indexes with logarithmic search time. Journal of Computer and System Sciences, 118:53–74, 2021. doi:10.1016/j.jcss.2020.12.001.

[bib.bib14] [14] Samuel Eilenberg. Automata, Languages, and Machines. Vol. A. Academic Press [A subsidiary of Harcourt Brace Jovanovich, Publishers], New York, 1974.

[bib.bib15] [15] Joost Engelfriet and Hendrik Jan Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic, 2(2):216–254, 2001. doi:10.1145/371316.371512.

[bib.bib16] [16] Joost Engelfriet and Heiko Vogler. Macro tree transducers. Journal of Computer and System Sciences, 31(1):71–146, 1985. doi:10.1016/0022-0000(85)90066-2.

[bib.bib17] [17] Paolo Ferragina and Giovanni Manzini. Indexing compressed text. Journal of the ACM, 52(4):552–581, 2005. doi:10.1145/1082036.1082039.

[bib.bib18] [18] Emmanuel Filiot and Pierre-Alain Reynier. Copyful streaming string transducers. In Proceedings of the 11th International Workshop on Reachability Problems, RP 2017, volume 10506 of Lecture Notes in Computer Science, pages 75–86. Springer, 2017. doi:10.1007/978-3-319-67089-8_6.

[bib.bib19] [19] Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polynomial-time algorithm for deciding equivalence of normed context-free processes. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, FOCS 1994, pages 623–631. IEEE Computer Society, 1994. doi:10.1109/SFCS.1994.365729.

[bib.bib20] [20] Artur Jeż. Approximation of grammar-based compression via recompression. Theoretical Computer Science, 592:115–134, 2015. doi:10.1016/J.TCS.2015.05.027.

[bib.bib21] [21] Artur Jeż. Faster fully compressed pattern matching by recompression. ACM Transactions on Algorithms, 11(3):20:1–20:43, 2015. doi:10.1145/2631920.

[bib.bib22] [22] Marek Karpinski, Wojciech Rytter, and Ayumi Shinohara. Pattern-matching for strings with short descriptions. In Proceedings of the 6th Annual Symposium on Combinatorial Pattern Matching, CPM 95, volume 937 of Lecture Notes in Computer Science, pages 205–214. Springer, 1995. doi:10.1007/3-540-60044-2_44.

[bib.bib23] [23] Sandra Kiefer, Lê Thành Dũng Nguyên, and Cécilia Pradic. Refutations of pebble minimization via output languages, 2023. arXiv:2301.09234.

[bib.bib24] [24] Yury Lifshits, Shay Mozes, Oren Weimann, and Michal Ziv-Ukelson. Speeding up HMM decoding and training by exploiting sequence repetitions. Algorithmica, 54(3):379–399, 2009. doi:10.1007/S00453-007-9128-0.

[bib.bib25] [25] Markus Lohrey. Leaf languages and string compression. Information and Computation, 209(6):951–965, 2011. doi:10.1016/J.IC.2011.01.009.

[bib.bib26] [26] Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241–299, 2012. doi:10.1515/GCC-2012-0016.

[bib.bib27] [27] Markus Lohrey. The Compressed Word Problem for Groups. SpringerBriefs in Mathematics. Springer, 2014. doi:10.1007/978-1-4939-0748-9.

[bib.bib28] [28] Kurt Mehlhorn, R. Sundar, and Christian Uhrig. Maintaining dynamic sequences under equality-tests in polylogarithmic time. In Proceedings of the 5th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 1994, pages 213–222. ACM/SIAM, 1994. URL: http://dl.acm.org/citation.cfm?id=314464.314496.

[bib.bib29] [29] Lê Thành Dung Nguyên, Camille Noûs, and Pierre Pradic. Comparison-free polyregular functions. In Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, volume 198 of LIPIcs, pages 139:1–139:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.ICALP.2021.139.

[bib.bib30] [30] Wojciech Plandowski. Testing equivalence of morphisms on context-free languages. In Proceedings of the 2nd Annual European Symposium on Algorithms, ESA 1994, volume 855 of Lecture Notes in Computer Science, pages 460–470. Springer, 1994. doi:10.1007/BFB0049431.

[bib.bib31] [31] Wojciech Plandowski and Wojciech Rytter. Complexity of language recognition problems for compressed words. In Juhani Karhumäki, Hermann A. Maurer, Gheorghe Paun, and Grzegorz Rozenberg, editors, Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 262–272. Springer, 1999. doi:10.1007/978-3-642-60207-8_23.

[bib.bib32] [32] Wojciech Rytter. Application of Lempel-Ziv factorization to the approximation of grammar-based compression. Theoretical Computer Science, 302(1–3):211–222, 2003. doi:10.1016/S0304-3975(02)00777-6.

[bib.bib33] [33] John C. Shepherdson. The reduction of two-way automata to one-way automata. IBM Journal of Research and Development, 3(2):198–200, April 1959. doi:10.1147/RD.32.0198.

[bib.bib34] [34] Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/149.

	$\displaystyle\mathtt{reverse}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{}\to A^{}}}$
	$\displaystyle\mathtt{concat}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{*}\to A^{}}}$
	$\displaystyle\mathtt{map}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0.6796875,0.9375}(A\to B)\to A^{}\to B^{}}}$
	$\displaystyle\mathtt{split}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}A^{}\to(A^{}\times A^{})^{}}}$
	$\displaystyle\mathtt{block}^{{\color[rgb]{0,0.6796875,0.9375}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0.6796875,0.9375}(A+B)^{}\to A^{}\times(B% \times A^{})^{}}}\qquad$

Transducers on Compressed Strings

Abstract

Keywords and phrases:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Grammar-based string compression

String-to-string functions

Definition 1.

Example 2 (duplication).

Example 3 (reversal).

Example 4 (squaring).

Example 5 (exponential outputs).

2 Transducers compatible with compression

2.1 Rational functions

Theorem 6.

Proof.

2.2 The map combinator

Lemma 7.

Proof.

Claim 8.

Proof.

2.3 Regular functions

Theorem 9.

Theorem 10.

Proof.

2.4 Polyregular functions

Example 11 (marked squaring).

Definition 12.

Lemma 13.

Proof.

Claim 14.

Proof.

2.5 Rectangular polyregular functions

Example 15 (rectangle).

Definition 16 (rectangular polyregular functions).

Theorem 17.

Theorem 18.

Proof.

A normal form.

Lemma 19.

Proof.

3 A functional programming language

Example 20 (duplication, squaring and rectangle).

3.1 Syntax

3.1.1 Variables, application and abstraction

3.1.2 Data constructors and destructors

3.1.3 List processing

3.1.4 Rational functions

3.2 Semantics

3.3 String-to-string functions

Theorem 21 ([7, Theorem 4.1]).

Theorem 22.

Proof.

String representation of programs.

Definition 23.

Reduction.

Lemma 24.

Proof.

A reduction strategy.

Lemma 25 ([6, Lemma 8.6]).

Corollary 26.

Proof.

3.4 Programs with combinators instead of 𝝀-abstraction

Theorem 27.

Proof.

4 Conclusions

References

3.4 Programs with combinators instead of $\lambda$ -abstraction