In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data
For functions over data
We focus on two kinds of data domains: first, the general setting of oligomorphic data, which encompasses any data domain with equality, as well as the setting of rational numbers with linear order; and second, the set of natural numbers equipped with linear order. For both settings, we prove that functionality, i.e. determining whether the relation recognized by the transducer is actually a function, is decidable. We also show that the so called next letter problem is decidable, yielding equivalence between (uniform) continuity and (uniform) computability. Last, we provide characterizations of (uniform) continuity, which allow us to prove that these notions, and thus also (uniform) computability, are decidable. We even show that all these decision problems are PSpace-complete for $(\mathbb{N},\leq)$ and for a large class of oligomorphic data domains, including for instance $(\mathbb{Q},\leq)$.
This work has been submitted to the LMCS Special Issue dedicated to FoSSaCS 2020, and has been accepted with minor revisions. The preprint is available on arXiv. Nathan Lhote joined us to extend the results presented in On Computability of Data Word Functions Defined by Transducers (FoSSaCS 2020) in the following ways:
To obtain those generalisations, we shifted to a more abstract presentation of the problem. The reader who is mainly interested in the $(\mathbb{N},=)$ case can consult the conference version, where the proofs use more concrete objects, although they are arguably less elegant. They might also have a look at Section 12.1 of my manuscript, where the presentation of the concepts and the proofs have been rewritten and detailed2.