Document Open Access Logo

On Uniformization in the Full Binary Tree

Author Alexander Rabinovich



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.77.pdf
  • Filesize: 0.75 MB
  • 14 pages

Document Identifiers

Author Details

Alexander Rabinovich
  • The Blavatnik School of Computer Science, Tel Aviv University, Israel

Cite AsGet BibTex

Alexander Rabinovich. On Uniformization in the Full Binary Tree. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 77:1-77:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.77

Abstract

A function f uniformizes a relation R(X,Y) if R(X,f(X)) holds for every X in the domain of R. The uniformization problem for a logic L asks whether for every L-definable relation there is an L-definable function that uniformizes it. Gurevich and Shelah proved that no Monadic Second-Order (MSO) definable function uniformizes relation "Y is a one element subset of X" in the full binary tree. In other words, there is no MSO definable choice function in the full binary tree. The cross-section of a relation R(X,Y) at D is the set of all E such that R(D,E) holds. Hence, a function that uniformizes R chooses one element from every non-empty cross-section. The relation "Y is a one element subset of X" has finite and countable cross-sections. We prove that in the full binary tree the following theorems hold: ▶ Theorem (Finite cross-sections) If every cross-section of an MSO definable relation is finite, then it has an MSO definable uniformizer. ▶ Theorem (Uncountable cross-section) There is an MSO definable relation R such that every MSO definable relation included in R and with the same domain as R has an uncountable cross-section.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Monadic Second-Order Logic
  • Uniformization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Vince Bárány, Łukasz Kaiser, and Alex Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundamenta Informaticae, 100(1-4):1-17, 2010. Google Scholar
  2. Arnaud Carayol and Christof Löding. MSO on the infinite binary tree: Choice and order. In International Workshop on Computer Science Logic, pages 161-176. Springer, 2007. Google Scholar
  3. Arnaud Carayol, Christof Löding, Damian Niwinski, and Igor Walukiewicz. Choice functions and well-orderings over the infinite binary tree. Open Mathematics, 8(4):662-682, 2010. Google Scholar
  4. Grzegorz Fabianski, Michal Skrzypczak, and Szymon Torunczyk. Uniformisations of regular relations over bi-infinite words. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 384-396. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394782.
  5. Yuri Gurevich. Monadic second-order theories. Model-theoretic logics, pages 479-506, 1985. Google Scholar
  6. Yuri Gurevich and Saharon Shelah. Rabin’s uniformization problem 1. The Journal of Symbolic Logic, 48(4):1105-1119, 1983. Google Scholar
  7. Shmuel Lifsches and Saharon Shelah. Uniformization and skolem functions in the class of trees. The Journal of Symbolic Logic, 63(1):103-127, 1998. Google Scholar
  8. Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141:1-35, 1969. Google Scholar
  9. Saharon Shelah. The monadic theory of order. Annals of Mathematics, 102(3):379-419, 1975. Google Scholar
  10. Wolfgang Thomas. Automata on infinite objects. In Formal Models and Semantics, pages 133-191. Elsevier, 1990. Google Scholar
  11. Wolfgang Thomas. Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In Structures in Logic and Computer Science, pages 118-143. Springer, 1997. Google Scholar
  12. Boris Trakhtenbrot and Ya Martynovich Barzdin. Finite automate: behaviour and synthesis. North-Holland, 1973. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail