Folding interpretations

TL;DR

This paper introduces a new formal system with a fold-based iteration mechanism that characterizes polyregular string-to-string functions, expanding the understanding of automata and logic in defining such functions.

Contribution

It presents a novel combinator system including a fold operator, with a type system that precisely captures polyregular functions, extending previous models.

Findings

The system characterizes exactly polyregular functions.

Inclusion of fold enables defining all polyregular functions.

Related systems for quantifier-free and linear regular functions are also described.

Abstract

We study the polyregular string-to-string functions, which are certain functions of polynomial output size that can be described using automata and logic. We describe a system of combinators that generates exactly these functions. Unlike previous systems, the present system includes an iteration mechanism, namely fold. Although unrestricted fold can define all primitive recursive functions, we identify a type system (inspired by linear logic) that restricts fold so that it defines exactly the polyregular functions. We also present related systems, for quantifier-free functions as well as for linear regular functions on both strings and trees.