On Decidability of List Structures
- 9 Downloads
The paper studies computability-theoretic complexity of various structures that are based on the list data type. The list structure over a structure S consists of the two sorts of elements: The first sort is atoms from S, and the second sort is finite linear lists of atoms. The signature of the list structure contains the signature of S, the empty list nil, and the binary operation of appending an atom to a list. The enriched list structure over S is obtained by enriching the signature with additional functions and relations: obtaining a head of a list, getting a tail of a list, “an atom x occurs in a list Y,” and “a list X is an initial segment of a list Y.” We prove that the first-order theory of the enriched list structure over (ω, +), i.e. the monoid of naturals under addition, is computably isomorphic to the first-order arithmetic. In particular, this implies that the transformation of a structure S into the enriched list structure over S does not always preserve the decidability of first-order theories. We show that the list structure over S can be presented by a finite word automaton if and only if S is finite.
Keywordslinear list list structure decidable structure automatic structure tree automatic structure
Unable to display preview. Download preview PDF.
- 3.Goncharov S. S. and Sviridenko D. I., “Theoretical aspects of E-programming,” in: Mathematical Methods of Specification and Synthesis of Software Systems’85, Springer-Verlag, Berlin and Heidelberg, 1986, 169–179 (Lect. Notes Comput. Sci.; V. 215).Google Scholar
- 14.Bárány V., Grädel E., and Rubin S., “Automata-based presentations of infinite structures,” in: Finite and Algorithmic Model Theory, Cambridge Univ. Press, Cambridge, 2011, vol. 379, 1–76 (Lond. Math. Soc. Lect. Note Ser.).Google Scholar
- 18.Blumensath A., Automatic Structures: Diploma Thesis, RWTH, Aachen (1999).Google Scholar
- 28.Colcombet T., “Equational presentations of tree-automatic structures,” in: Workshop on Automata, Structures and Logic, Auckland, 2004.Google Scholar