Computability and Constrained Equations in Free Semigroups

Given a finite set (A), and an associative binary operation (\circ), a semigroup is a set that contains (A) and is closed under (\circ). If (|A| = n), the free semigroup (A^+) is a particular example of a semigroup. Often in computer science, (A) is a set of symbols called letters, (\circ) is the concatenation operation, and (A^+) contains all non-empty strings (also called words) comprising symbols from (A).

The first-order theory of a free semigroup is algorithmically undecidable in general; however, satisfiability for first-order quantifier-free formulas, including single equations, is well known to be decidable, at least in theory. In practice, developing sufficiently efficient algorithms remains a challenge. The aim of this project is to study equations or quantifier-free first-order formulas in free semigroups that are augmented by additional constraints, for example by restricting the values variables may take to rational subsets of (A^+) or by placing arithmetic constraints on their lengths, and as a result to better understand the limits of algorithmic approaches in solving the resulting satisfiability problems.

Such problems have implications in a variety of areas of mathematics and computer science, including formal methods, combinatorial group theory, arithmetic and number theory, formal language theory, theory of computation, and combinatorics on words. The project will consist primarily of producing novel definitions, theorems, and proofs, and may include some practical (programming) elements depending on the strengths and interests of a successful applicant. In all cases, a strong background in theoretical computer science and discrete mathematics is required, particularly in topics such as formal language theory, logic, algorithms, and complexity.

A successful candidate should have strong internal motivation and should enjoy problem-solving and abstract thinking. They should work well individually, although there will also be opportunities for collaboration and networking both locally and internationally. Good communication skills, both verbal and written, and experience in reading and writing formal mathematics (including proofs) are also desirable.

Applicants from diverse backgrounds are strongly encouraged. Further assessment criteria. The candidate will be part of the theoretical computer science research theme and will work closely with the primary supervisor, supported by regular supervision meetings.

They will likely share an office with other PhD students and postdocs working in a mixture of theoretical and applied areas of computer science. 94% of Loughborough’s research impact is rated world-leading or internationally excellent. REF 2021