Existential and positive theories of equations in graph products (Q705067)

In this article it is proved that, for a fixed graph product \(\mathbb P\) of finite monoids, free monoids, and free groups, the existential (i.e., sentences in prenex normal form without universal quantifiers) theory of equations can be decided in PSPACE. Moreover, when the equations have normalized rational (NRAT\((\mathbb P)\)) constraints, the problem becomes PSPACE-complete. Another main result states that, for graph products of finite and free groups, the positive (i.e., sentences without negations) theory of equations with recognizible (REC\((\mathbb G)\)) constraints is decidable. These results continue the stream of research on decidability of theories of equations on monoids and groups started by \textit{G. S. Makanin} [Mat. Sb., Nov. Ser. 103(145), 147--236 (1977; Zbl 0371.20047)]. The results in this paper are based on the main result of \textit{V. Diekert} and \textit{A. Muscholl} [Lect. Notes Comput. Sci. 2076, 543--554 (2001; Zbl 0986.20036)] on existential theories of equations in trace monoids with involution. This result is used within the underlying trace monoid with involution of the graph product. It is proved that, for an existential sentence \(\phi\) with constraints in NRAT\((\mathbb P)\), there exist an existential sentence \(\phi'\) such that \(\phi\) holds in \(\mathbb P\) if and only if \(\phi'\) holds in the underlying monoid with involution. In this reduction, a specific confluent trace rewriting systems is used. The decidability of the positive theory of equations with constraints in REC\((\mathbb G)\), where \(\mathbb G\) is a graph product of finite and free groups, is proved in two steps. Firstly, it is proved that it possible to restrict the investigation to graph products of a particular type, and, secondly, the positive sentences with constraints in REC are reduced to existential sentences with constraints in NRAT. The result then follows by the first result.