Table of Contents
Fetching ...

Effective equation solving, constraints and growth in virtually abelian groups

Laura Ciobanu, Alex Evetts, Alex Levine

TL;DR

The paper addresses the satisfiability of group equations in finitely generated virtually abelian groups under length, abelianisation, context-free, and lexicographic constraints. It develops an effective translation of these constraints into rational sets and reduces constrained equation solving to the known decidable DP with rational constraints, while also delivering methods to compute growth series. Central tools include semilinear set theory, Parikh images, integer affine maps, geodesic normal forms, and transducers for context-free languages. The results yield decidability and constructive descriptions of solution sets, with practical implications for constrained word problems and potential applications to SMT/string solvers, without asserting complexity bounds.

Abstract

In this paper we study the satisfiability and solutions of group equations when combinatorial, algebraic and language-theoretic constraints are imposed on the solutions. We show that the solutions to equations with length, lexicographic order, abelianisation or context-free constraints added, can be effectively produced in finitely generated virtually abelian groups. Crucially, we translate each of the constraints above into a rational set in an effective way, and so reduce each problem to solving equations with rational constraints, which is decidable and well understood in virtually abelian groups. A byproduct of our results is that the growth series of a virtually abelian group, with respect to any generating set and any weight, is effectively computable. This series is known to be rational by a result of Benson, but his proof is non-constructive.

Effective equation solving, constraints and growth in virtually abelian groups

TL;DR

The paper addresses the satisfiability of group equations in finitely generated virtually abelian groups under length, abelianisation, context-free, and lexicographic constraints. It develops an effective translation of these constraints into rational sets and reduces constrained equation solving to the known decidable DP with rational constraints, while also delivering methods to compute growth series. Central tools include semilinear set theory, Parikh images, integer affine maps, geodesic normal forms, and transducers for context-free languages. The results yield decidability and constructive descriptions of solution sets, with practical implications for constrained word problems and potential applications to SMT/string solvers, without asserting complexity bounds.

Abstract

In this paper we study the satisfiability and solutions of group equations when combinatorial, algebraic and language-theoretic constraints are imposed on the solutions. We show that the solutions to equations with length, lexicographic order, abelianisation or context-free constraints added, can be effectively produced in finitely generated virtually abelian groups. Crucially, we translate each of the constraints above into a rational set in an effective way, and so reduce each problem to solving equations with rational constraints, which is decidable and well understood in virtually abelian groups. A byproduct of our results is that the growth series of a virtually abelian group, with respect to any generating set and any weight, is effectively computable. This series is known to be rational by a result of Benson, but his proof is non-constructive.
Paper Structure (14 sections, 38 theorems, 42 equations, 1 figure)

This paper contains 14 sections, 38 theorems, 42 equations, 1 figure.

Key Result

Theorem 1.1

In any finitely generated virtually abelian group, it is effectively decidable whether a finite system of equations with the following kinds of constraints has solutions:

Figures (1)

  • Figure 1: Exact diagram from virtually abelian group

Theorems & Definitions (90)

  • Theorem 1.1
  • Theorem 1.2
  • Corollary 1.3
  • Proposition 1.4
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • ...and 80 more