TY - JOUR

T1 - On Decidability of List Structures

AU - Aleksandrova, S. A.

AU - Bazhenov, N. A.

PY - 2019/5/1

Y1 - 2019/5/1

N2 - 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.

AB - 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.

KW - automatic structure

KW - decidable structure

KW - linear list

KW - list structure

KW - tree automatic structure

UR - http://www.scopus.com/inward/record.url?scp=85067383505&partnerID=8YFLogxK

U2 - 10.1134/S0037446619030029

DO - 10.1134/S0037446619030029

M3 - Article

AN - SCOPUS:85067383505

VL - 60

SP - 377

EP - 388

JO - Siberian Mathematical Journal

JF - Siberian Mathematical Journal

SN - 0037-4466

IS - 3

ER -