Regular Choice Functions and Uniformisations For countable Domains
We view languages of words over a product alphabet A x B as relations between words over A and words over B. This leads to the notion of regular relations - relations given by a regular language. We ask when it is possible to find regular uniformisations of regular relations. The answer depends on the structure or shape of the underlying model: it is true e.g. for ω-words, while false for words over ℤ or for infinite trees.
In this paper we focus on countable orders. Our main result characterises, which countable linear orders D have the property that every regular relation between words over D has a regular uniformisation. As it turns out, the only obstacle for uniformisability is the one displayed in the case of ℤ - non-trivial automorphisms of the given structure. Thus, we show that either all regular relations over D have regular uniformisations, or there is a non-trivial automorphism of D and even the simple relation of choice cannot be uniformised. Moreover, this dichotomy is effective.
Uniformisation
Monadic Second-order logic
Countable words
Theory of computation~Regular languages
Theory of computation~Automata over infinite objects
69:1-69:13
Regular Paper
Vincent
Michielini
Vincent Michielini
University of Warsaw, Poland
The first author has been supported by the European Research Council (ERC) grant under the European Union’s Horizon 2020 research and innovation programme (ERC Consolidator Grant LIPA, grant agreement No. 683080).
Michał
Skrzypczak
Michał Skrzypczak
University of Warsaw, Poland
https://orcid.org/0000-0002-9647-4993
The second author has been supported by Poland’s National Science Centre (NCN) (grant No. 2016 D/ST6/00491).
10.4230/LIPIcs.MFCS.2020.69
Arnaud Carayol and Christof Löding. MSO on the infinite binary tree: Choice and order. In CSL, pages 161-176, 2007.
Olivier Carton, Thomas Colcombet, and Gabriele Puppis. An algebraic approach to MSO-definability on countable linear orderings. J. Symb. Log., 83(3):1147-1189, 2018.
Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic. Undergraduate Texts in Mathematics. Springer New York, 1996.
Grzegorz Fabiański, Michał Skrzypczak, and Szymon Toruńczyk. Uniformisations of regular relations over bi-infinite words. In LICS, pages 384-396, 2020.
Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
Yuri Gurevich and Saharon Shelah. Rabin’s uniformization problem. Journal of Symbolic Logic, 48(4):1105-1119, 1983.
Shmuel Lifsches and Saharon Shelah. Uniformization and Skolem functions in the class of trees. Journal of Symbolic Logic, 63(1):103-127, 1998.
Anil Nerode. Linear automaton transformations. Proceedings of the American Mathematical Society, 9(4):541-544, 1958.
Alexander Rabinovich. On decidability of monadic logic of order over the naturals extended by monadic predicates. Information and Computation, 205(6):870-889, 2007.
Dirk Siefkes. The recursive sets in certain monadic second order fragments of arithmetic. Arch. Math. Logik, 17(1-2):71-80, 1975.
Vincent Michielini and Michał Skrzypczak
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode