We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Formal Languages and Automata Theory

Title: Continuous Uniformization of Rational Relations and Synthesis of Computable Functions

Abstract: A uniformizer of a binary relation is a function whose graph is contained in the relation and which is defined on the same domain as the relation. It is known that any rational relation of infinite words, i.e. a relation given as a transducer, admits a rational uniformizer. Although rational, those uniformizers are not necessarily well-behaved, in the sense that the $i$th letter of the output word may depend on the whole infinite input word. In other words, those uniformizers might not be continuous (for the Cantor topology). This paper addresses the question of whether rational relations of infinite words can be uniformized by continuous functions. On the negative side, continuous uniformizers might not exist in general and we prove that deciding their existence is algorithmically impossible. On the positive side, we exhibit a large class of rational relations of infinite words, called weakly deterministic rational relations, for which deciding whether a relation in this class admits a continuous uniformizer is an ExpTime-c problem. This class includes the known classes of deterministic rational relations and automatic relations of infinite words.
As an application of the previous result, and by exploiting a connection between computability and continuity for rational functions of infinite words, we show a result on the synthesis of computable functions from specifications given as weakly deterministic rational relations. In particular, we show that deciding the existence of a computable uniformizer is ExpTime-c and if there is one, it is possible to effectively synthesize a deterministic two-way transducer computing it. This generalizes the classical setting of Church synthesis to asynchronous implementations which can arbitrarily delay the production of their output signals.
Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
Cite as: arXiv:2103.05674 [cs.FL]
  (or arXiv:2103.05674v1 [cs.FL] for this version)

Submission history

From: Sarah Winter [view email]
[v1] Tue, 9 Mar 2021 19:21:00 GMT (486kb)
[v2] Fri, 30 Jul 2021 09:03:27 GMT (512kb,D)
[v3] Wed, 6 Oct 2021 09:43:35 GMT (537kb,D)

Link back to: arXiv, form interface, contact.