Regular functions of infinite words are (partial) functions realized by deterministic two-way transducers with infinite look-ahead. Equivalently, Alur et. al. have shown that they correspond to functions realized by deterministic Muller streaming string transducers, and to functions defined by MSO-transductions. Regular functions are however not computable in general (for a classical extension of Turing computability to infinite inputs), and we consider in this paper the class of deterministic regular functions of infinite words, realized by deterministic two-way transducers without look-ahead. We prove that it is a well-behaved class of functions: they are computable, closed under composition, characterized by the guarded fragment of MSO-transductions, by deterministic B\"uchi streaming string transducers, by deterministic two-way transducers with finite look-ahead, and by finite compositions of sequential functions and one fixed basic function called map-copy-reverse.
翻译:无限词的正则函数是通过具有无限前视的确定性双向换能器实现的(部分)函数。Alur等人已证明,这些函数等价于由确定性Muller流式字符串换能器实现的函数,以及由MSO-转录定义的函数。然而,正则函数通常不可计算(针对将图灵可计算性经典扩展到无限输入的情况)。本文研究由无前视的确定性双向换能器实现的无限词确定性正则函数类。我们证明该类函数具有良好性质:它们是可计算的、对复合运算封闭、可由MSO-转录的受保护片段刻画、可由确定性Büchi流式字符串换能器刻画、可由具有有限前视的确定性双向换能器刻画,以及可由顺序函数与一个称为map-copy-reverse的固定基本函数的有限复合刻画。