Pebble Minimization of Polyregular Functions

TL;DR

This paper characterizes polyregular functions based on output size and pebble transducer complexity, providing decidability results and applications to MSO interpretations, linking pebble count to output growth.

Contribution

It establishes a precise relationship between pebble transducers and output size of polyregular functions, including decidability and minimal pebble computation.

Findings

Polyregular functions are regular iff output size is linear.

k-pebble transducers realize functions with polynomial output of degree k.

Decidability of minimal pebble transducer realization for polyregular functions.

Abstract

We show that a polyregular word-to-word function is regular if and only if its output size is at most linear in its input size. Moreover a polyregular function can be realized by: a transducer with two pebbles if and only if its output has quadratic size in its input, a transducer with three pebbles if and only if its output has cubic size in its input, etc. Moreover the characterization is decidable and, given a polyregular function, one can compute a transducer realizing it with the minimal number of pebbles. We apply the result to mso interpretations from words to words. We show that mso interpretations of dimension k exactly coincide with k-pebble transductions.