On Decidability of List Structures

Abstract

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.