The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer. We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we prove to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.

翻译：综合问题要求从正确输入-输出对的规范中自动生成算法（若存在）。本文研究了无限词上可计算函数的综合问题，基于经典图灵可计算性概念在无限输入上的推广。我们考虑的规范是无限词上的理性关系，即由非确定性奇偶转换器定义的规范。我们证明了从理性规范综合可计算函数的问题是不可判定的。我们提出了一种不完整但可靠的归约方法，将问题归约到某种奇偶博弈，若伊芙赢得该博弈，则该理性规范可由可计算函数实现。我们证明该函数甚至可由确定性双向转换器计算。我们给出了上述博弈归约完备的充分条件。这导出了可计算函数综合问题的可判定性，并证明对于理性规范的一个大子类——即确定性理性规范，该问题是ExpTime-完全的。该子类包含无限词上的自动关系，后者是反应式综合的基准。