A theorem establishes that MSO queries on strings with O(n0 * n1) results can be reparameterized to identify each result from one 0-position, one 1-position and finite data, with the result extending to FO logic.
Polyregular Functions.CoRR, abs/1810.08760
2 Pith papers cite this work. Polarity classification is still indexing.
abstract
This paper is about certain string-to-string functions, called the polyregular functions. These are like the regular string-to-string functions, except that they can have polynomial (and not just linear) growth. The class has four equivalent definitions: 1. deterministic two-way transducers with pebbles; 2 the smallest class of string-to-string functions that is closed under composition, contains all sequential functions as well as two extra functions called squaring and iterated reverse 3. a fragment of the lambda-calculus, which has a list type constructor and limited forms of iteration such as map but not fold; 4. an imperative programming language, which has for loops that range over input positions. The first definition comes from [milo2003typechecking], while the remaining three are new to the author's best knowledge. The class of polyregular functions contains known classes of string-to-string transducers, such as the sequential, rational, or regular ones, but goes beyond them because of super-linear growth. Polyregular functions have good algorithmic properties, such as: - the output can be computed in linear time (in terms of combined input and output size); - the inverse image of a regular word language is (effectively) regular. We also identify a fragment of polyregular functions, called the first-order polyregular functions, which has additional good properties, e.g. the output can be computed by an AC0 circuit.
verdicts
UNVERDICTED 2representative citing papers
Equivalence of higher-order string-to-string polyregular functions is undecidable by reduction from the tiling problem.
citing papers explorer
-
A finer reparameterisation theorem for MSO and FO queries on strings
A theorem establishes that MSO queries on strings with O(n0 * n1) results can be reparameterized to identify each result from one 0-position, one 1-position and finite data, with the result extending to FO logic.
-
Polyregular equivalence is undecidable in higher-order types
Equivalence of higher-order string-to-string polyregular functions is undecidable by reduction from the tiling problem.