On decidability of list structures

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 $(\omega, +)$, 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.