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.

Original languageEnglish
Pages (from-to)377-388
Number of pages12
JournalSiberian Mathematical Journal
Issue number3
Publication statusPublished - 1 May 2019


  • automatic structure
  • decidable structure
  • linear list
  • list structure
  • tree automatic structure


Dive into the research topics of 'On Decidability of List Structures'. Together they form a unique fingerprint.

Cite this