On existential theories of list concatenation

Abstract

We discuss the existential fragments of two theories of concatenation. These theories describe concatenation of possibly nested lists in the algebra of finite trees with lists and in the algebra of rational trees with lists. Syntax and the choice of models are motivated by the treatment of lists in PROLOG III. In a recent prototype of this language, Colmerauer has integrated a built-in concatenation of lists, and the constraint-solver checks satisfiability of equations and disequations over concatenated lists. But, for efficiency reasons satisfiability is only tested in a rather approximative way. The question arises whether satisfiability is decidable. Our main results are the following. For the algebra of finite trees with lists, the existential fragment of the theory is decidable. For the algebra of rational trees with lists, the positive existential fragment of the theory is decidable. Problems in the treatment of the existential fragment may be traced back to a difficult question about solvability of word equations with length constraints for variables.

Supported by EC Working Group CCL, EP 6028.