Theories of orders on the set of words
RAIRO - Theoretical Informatics and Applications (2010)
- Volume: 40, Issue: 1, page 53-74
- ISSN: 0988-3754
Access Full Article
topAbstract
topHow to cite
topKuske, Dietrich. "Theories of orders on the set of words." RAIRO - Theoretical Informatics and Applications 40.1 (2010): 53-74. <http://eudml.org/doc/92789>.
@article{Kuske2010,
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 ∑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},
keywords = {decidability; undecidability; first-order theory; words; subword order; lexicographic path; homomorphism preorder; infix order},
language = {eng},
month = {3},
number = {1},
pages = {53-74},
publisher = {EDP Sciences},
title = {Theories of orders on the set of words},
url = {http://eudml.org/doc/92789},
volume = {40},
year = {2010},
}
TY - JOUR
AU - Kuske, Dietrich
TI - Theories of orders on the set of words
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
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 ∑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/92789
ER -
References
top- F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press (1998).
- A. Björner, The Möbius function of subword order, in Invariant theory and tableaux, IMA Springer. Math. Appl.19 (1990) 118–124.
- A. Boudet and H. Comon, About the theory of tree embedding, in TAPSOFT'93, Springer. Lect. Notes Comp. Sci.668 (1993) 376–390.
- 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.
- J.R. Büchi and S. Senger, Coding in the existential theory of concatentation. Archiv Math. Logik26 (1986) 101–106.
- H. Comon and R. Treinen, Ordering constraints on trees, in CAAP'94, Springer. Lect. Notes Comp. Sci.787 (1994) 1–14.
- H. Comon and R. Treinen, The first-order theory of lexicographic path orderings is undecidable. Theor. Comput. Sci.176 (1997) 67–87.
- 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.
- N. Dershowitz, Orderings for term rewriting systems. Theor. Comput. Sci.17 (1982) 279–301.
- V.G. Durnev, Undecidability of the positive ∀∃3-theory of a free semigroup. Sibirsky Matematicheskie Jurnal36 (1995) 1067–1080.
- F.D. Farmer, Homotopy spheres in formal languages. Stud. Appl. Math.66 (1982) 171–179.
- A. Finkel and Ph. Schnoebelen, Well-structured transition systems everywhere! Theor. Comput. Sci.256 (2001) 63–92.
- K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik38 (1931) 173–198.
- T. Harju and L. Illie, On quasi orders of words and the confluence property. Theor. Comput. Sci.200 (1998) 205–224.
- G. Higman, Ordering by divisibility in abstract algebras. Proc. London Math. Soc.2 (1952) 326–336.
- S. Kosub and K. Wagner, The boolean hierarchy of NP-partitions, in STACS 2000, Springer. Lect. Notes Comp. Sci.1770 (2000) 157–168.
- D. Kuske, Emptiness is decidable for asynchronous cellular machines, in CONCUR 2000. Springer. Lect. Notes Comp. Sci.1877 (2000) 536–551.
- U. Leck, Nonexistence of a Kruskal-Katona type theorem for subword orders. Technical Report 98-06, Universität Rostock, Fachbereich Mathematik (1998).
- M. Lothaire, Combinatorics on Words. Addison-Wesley (1983).
- 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 Sbornik32 (1977).
- Y. Matiyasevich, Hilbert's Tenth Problem. MIT Press (1993).
- P. Narendran and M. Rusinowitch, The theory of total unary rpo is decidable, in Computational Logic 2000, Springer. Lect. Notes Artificial Intelligence1861 (2000) 660–672.
- M.O. Rabin, Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.141 (1969) 1–35.
- V.L. Selivanov, Boolean hierarchy of partitions over reducible bases. Algebra and Logic43 (2004) 77–109.
- R. Treinen, A new method for undecidability proofs of first order theories. J. Symbolic Comput.14 (1992) 437–458.
NotesEmbed ?
topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.