Continuous Regular Functions
arXiv:1901.03366 · doi:10.23638/LMCS-16(1:17)2020
Abstract
Following Chaudhuri, Sankaranarayanan, and Vardi, we say that a function is -regular if there is a Büchi automaton that accepts precisely the set of base representations of elements of the graph of . We show that a continuous -regular function is locally affine away from a nowhere dense, Lebesgue null, subset of . As a corollary we establish that every differentiable -regular function is affine. It follows that checking whether an -regular function is differentiable is in . Our proofs rely crucially on connections between automata theory and metric geometry developed by Charlier, Leroy, and Rigo.