Almost free algebras: from the word problem to elimination of quantifiers

TL;DR

This paper studies almost free algebras, showing that several decision problems are polynomial time decidable and that they admit quantifier elimination, providing a new approach with potential for broader applications.

Contribution

It introduces a novel method for quantifier elimination in almost free algebras, extending the class of algebras with polynomial time decision procedures.

Findings

Decision problems like canonical representatives and isomorphism are polynomial time decidable.

Almost free algebras admit quantifier elimination with expanded language.

Constructs examples of non-initial algebras with polynomial time word problem.

Abstract

Term algebras are important objects in computer science and are correspondingly well-studied. A natural generalization is to quotient these algebras by finitely many ground term equations, obtaining what we call almost free algebras. One of the earliest results on almost free algebras is that their word problem is polynomial time decidable. In this paper, we show that other natural problems: finding canonical representatives; computing the cardinality of a congruence class; checking if all congruence classes are infinite; checking if the algebra is finite; checking if two algebras are isomorphic, are all polynomial time decidable. Another famous result regarding term algebras is that they admit quantifier elimination in a suitably expanded language. Following this pattern, we also show that almost free algebras admit quantifier elimination by expanding the language with the standard tester predicates. While this is implied by existing results, we view our main contribution here as providing a different approach, which we posit can be easily extended to a larger class that is not covered by existing works. Finally, we provide an application to the quantifier elimination procedure, constructing examples of non-initial algebras over arbitrary signatures with a polynomial time word problem.