Regular and First Order List Functions
Mikolaj Bojanczyk, Laure Daviaud, Krishna Shankara Narayanan

TL;DR
This paper introduces classes of list-manipulating functions called regular and first-order list functions, characterizes their equivalence to MSO-transductions and first-order transductions, and provides a formal framework for their construction.
Contribution
It defines regular and first-order list functions using combinators and shows their equivalence to MSO- and first-order transductions, respectively.
Findings
First-order list functions are equivalent to first-order transductions.
Regular list functions correspond exactly to MSO-transductions.
The framework formalizes list function construction using combinators.
Abstract
We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting them together using four combinators (most importantly, composition of functions). Our main results are that first-order list functions are exactly the same as first-order transductions, under a suitable encoding of the inputs; and the regular list functions are exactly the same as MSO-transductions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
