Theories of orders on the set of words

Dietrich Kuske

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2006)

  • Volume: 40, Issue: 1, page 53-74
  • ISSN: 0988-3754

Abstract

top
It is shown that small fragments of the first-order theory of the subword order, the (partial) lexicographic path ordering on words, the homomorphism preorder, and the infix order are undecidable. This is in contrast to the decidability of the monadic second-order theory of the prefix order [M.O. Rabin, Trans. Amer. Math. Soc., 1969] and of the theory of the total lexicographic path ordering [P. Narendran and M. Rusinowitch, Lect. Notes Artificial Intelligence, 2000] and, in case of the subword and the lexicographic path order, improves upon a result by Comon & Treinen [H. Comon and R. Treinen, Lect. Notes Comp. Sci., 1994]. Our proofs rely on the undecidability of the positive Σ 1 -theory of ( ℕ , + , · ) [Y. Matiyasevich, Hilbert’s Tenth Problem, 1993] and on Treinen’s technique [R. Treinen, J. Symbolic Comput., 1992] that allows to reduce Post’s correspondence problem to logical theories.

How to cite

top

Kuske, Dietrich. "Theories of orders on the set of words." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 40.1 (2006): 53-74. <http://eudml.org/doc/245673>.

@article{Kuske2006,
abstract = {It is shown that small fragments of the first-order theory of the subword order, the (partial) lexicographic path ordering on words, the homomorphism preorder, and the infix order are undecidable. This is in contrast to the decidability of the monadic second-order theory of the prefix order [M.O. Rabin, Trans. Amer. Math. Soc., 1969] and of the theory of the total lexicographic path ordering [P. Narendran and M. Rusinowitch, Lect. Notes Artificial Intelligence, 2000] and, in case of the subword and the lexicographic path order, improves upon a result by Comon & Treinen [H. Comon and R. Treinen, Lect. Notes Comp. Sci., 1994]. Our proofs rely on the undecidability of the positive $\Sigma _1$-theory of $(\mathbb \{N\},+,\cdot )$ [Y. Matiyasevich, Hilbert’s Tenth Problem, 1993] and on Treinen’s technique [R. Treinen, J. Symbolic Comput., 1992] that allows to reduce Post’s correspondence problem to logical theories.},
author = {Kuske, Dietrich},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {decidability; undecidability; first-order theory; words; subword order; lexicographic path; homomorphism preorder; infix order},
language = {eng},
number = {1},
pages = {53-74},
publisher = {EDP-Sciences},
title = {Theories of orders on the set of words},
url = {http://eudml.org/doc/245673},
volume = {40},
year = {2006},
}

TY - JOUR
AU - Kuske, Dietrich
TI - Theories of orders on the set of words
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2006
PB - EDP-Sciences
VL - 40
IS - 1
SP - 53
EP - 74
AB - It is shown that small fragments of the first-order theory of the subword order, the (partial) lexicographic path ordering on words, the homomorphism preorder, and the infix order are undecidable. This is in contrast to the decidability of the monadic second-order theory of the prefix order [M.O. Rabin, Trans. Amer. Math. Soc., 1969] and of the theory of the total lexicographic path ordering [P. Narendran and M. Rusinowitch, Lect. Notes Artificial Intelligence, 2000] and, in case of the subword and the lexicographic path order, improves upon a result by Comon & Treinen [H. Comon and R. Treinen, Lect. Notes Comp. Sci., 1994]. Our proofs rely on the undecidability of the positive $\Sigma _1$-theory of $(\mathbb {N},+,\cdot )$ [Y. Matiyasevich, Hilbert’s Tenth Problem, 1993] and on Treinen’s technique [R. Treinen, J. Symbolic Comput., 1992] that allows to reduce Post’s correspondence problem to logical theories.
LA - eng
KW - decidability; undecidability; first-order theory; words; subword order; lexicographic path; homomorphism preorder; infix order
UR - http://eudml.org/doc/245673
ER -

References

top
  1. [1] F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press (1998). Zbl0948.68098MR1629216
  2. [2] A. Björner, The Möbius function of subword order, in Invariant theory and tableaux, IMA Springer. Math. Appl. 19 (1990) 118–124. Zbl0706.06007
  3. [3] A. Boudet and H. Comon, About the theory of tree embedding, in TAPSOFT’93, Springer. Lect. Notes Comp. Sci. 668 (1993) 376–390. 
  4. [4] J.R. Büchi, Transfinite automata recursions and weak second order theory of ordinals, in Logic, Methodology and Philos. Sci., North Holland, Amsterdam (1965) 3–23. Zbl0207.31001
  5. [5] J.R. Büchi and S. Senger, Coding in the existential theory of concatentation. Archiv Math. Logik 26 (1986) 101–106. Zbl0646.03040
  6. [6] H. Comon and R. Treinen, Ordering constraints on trees, in CAAP’94, Springer. Lect. Notes Comp. Sci. 787 (1994) 1–14. Zbl0938.68589
  7. [7] H. Comon and R. Treinen, The first-order theory of lexicographic path orderings is undecidable. Theor. Comput. Sci. 176 (1997) 67–87. Zbl0903.68107
  8. [8] D.E. Daykin, To find all “suitable” orders of 0 , 1 -vectors. Congr. Numer. 113 (1996) 55–60. Festschrift for C. St. J. A. Nash-Williams. Zbl0898.15002
  9. [9] N. Dershowitz, Orderings for term rewriting systems. Theor. Comput. Sci. 17 (1982) 279–301. Zbl0525.68054
  10. [10] V.G. Durnev, Undecidability of the positive ∀ ∃ 3 -theory of a free semigroup. Sibirsky Matematicheskie Jurnal 36 (1995) 1067–1080. Zbl0853.20035
  11. [11] F.D. Farmer, Homotopy spheres in formal languages. Stud. Appl. Math. 66 (1982) 171–179. Zbl0511.55009
  12. [12] A. Finkel and Ph. Schnoebelen, Well-structured transition systems everywhere! Theor. Comput. Sci. 256 (2001) 63–92. Zbl0973.68170
  13. [13] K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38 (1931) 173–198. Zbl57.0054.02JFM57.0054.02
  14. [14] T. Harju and L. Illie, On quasi orders of words and the confluence property. Theor. Comput. Sci. 200 (1998) 205–224. Zbl0915.68104
  15. [15] G. Higman, Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2 (1952) 326–336. Zbl0047.03402
  16. [16] S. Kosub and K. Wagner, The boolean hierarchy of NP-partitions, in STACS 2000, Springer. Lect. Notes Comp. Sci. 1770 (2000) 157–168. Zbl0959.68521
  17. [17] D. Kuske, Emptiness is decidable for asynchronous cellular machines, in CONCUR 2000. Springer. Lect. Notes Comp. Sci. 1877 (2000) 536–551. Zbl0999.68132
  18. [18] U. Leck, Nonexistence of a Kruskal-Katona type theorem for subword orders. Technical Report 98-06, Universität Rostock, Fachbereich Mathematik (1998). Zbl1058.06003
  19. [19] M. Lothaire, Combinatorics on Words. Addison-Wesley (1983). Zbl0514.20045MR675953
  20. [20] G.S. Makanin, The problem of solvability of equations in a free semigroup, Math. Sbornik, 103 (1977) 147–236. In Russian; English translation in: Math. USSR Sbornik 32 (1977). Zbl0396.20037
  21. [21] Y. Matiyasevich, Hilbert’s Tenth Problem. MIT Press (1993). Zbl0790.03008
  22. [22] P. Narendran and M. Rusinowitch, The theory of total unary rpo is decidable, in Computational Logic 2000, Springer. Lect. Notes Artificial Intelligence 1861 (2000) 660–672. Zbl0983.68175
  23. [23] M.O. Rabin, Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969) 1–35. Zbl0221.02031
  24. [24] V.L. Selivanov, Boolean hierarchy of partitions over reducible bases. Algebra and Logic 43 (2004) 77–109. Zbl1061.03044
  25. [25] R. Treinen, A new method for undecidability proofs of first order theories. J. Symbolic Comput. 14 (1992) 437–458. Zbl0769.03026

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.