Deciding the Computability of Regular Functions over Infinite Words
share
The class of regular functions from infinite words to infinite words is characterised by MSO-transducers, streaming ω-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. This paper proposes a decision procedure for the fundamental question : given a regular function f, is f computable (by a Turing machine with infinite input)? For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational functions in NLogSpace (it was already known to be in PTime by Prieur), and of regular functions.
READ FULL TEXT