# Is unification over regular expression equations doable?

By way of example, suppose I know that $$X + a = b + Y$$ where $$X$$ and $$Y$$ are variables standing for regular expressions, then $$(X, Y) = (b, a)$$ is a solution to this set of equations.

Generalizing over all such equations, is there a computable (decidable) procedure for calculating the regular expressions which the variables must stand for in order for the equation to be solvable? Is there some kind of uniqueness, e.g. of minimal solutions?

In case the alphabet size matters: you can represent $$\{1, \ldots, n\}$$ in unary using just two symbols, so I assume the answer for $$k$$- and $$m$$-symbol alphabets are the same when $$k \geq 2 \land m \geq 2$$, in which case I care primarily for alphabets of size $$\geq 2$$—the reason I stress the word "assume" is that I know some properties of regular languages don't hold for regular expression equations (when suitably translated).

The application I have in mind is miniKanren-style logic programming.

Since families of sets closed under union form a semilattice, and the family of regular languages is one such closed family, programming with regular languages seems straightforward. For example, let each logic variable $$V$$ represent some indeterminate language $$L$$. For each $$V$$ store a pair of bounds $$(sub, disj)$$ expressing the knowledge $$sub \subseteq L \land (L \cap disj) = \emptyset$$, i.e. store two sets of strings for which the membership-ness is known. Grow them in the variable unification part and fail when $$sub \cap disj \not= \emptyset$$.

It would be nice to add logic over regular expressions and not just regular languages. No obvious approach occurs to me, and I suspect it's a whole other ballgame.

• I'm not talking about syntactic (expression-tree recursive) equality, i.e. I'm happy with $(X, Y) = (b, a)$ as a solution to your example. I don't quite understand the $X = Y = \{a, b\}^*$ part. My terms are standard regexps $(0, 1, a ∈ Σ, +, ·,\ ^*)$ with variables. An equation is satisfied if it holds whenever (variable-free) regular expressions variables are substituted for the variables (over all substitutions), and "holds" means the two sides describe the same language—i.e. (I think) I want e.g. $\{(X, Y) \mid a + b = X + Y\}$, suitably generalized. Does that answer your questions? Nov 10 '19 at 21:59

## 1 Answer

I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe.

They're decidable, even when we allow negation. You can see a great survey here: https://theory.stanford.edu/~aiken/publications/papers/ppcp94.pdf In general, Alexander Aiken has a lot of great papers on set constraints.

You might find more of what you're looking for with "word constraints" or "set constraints over words". The complexity situation isn't great for trees, but it might be better for words.

• I looked through it quickly, and I don't quite see how I map the concrete bits of my problem onto the general framework described in the paper. Could you help me out a bit here? Note: what I'm after is an assignment of regular expressions to variables such that the two sides of equations denote the same language, not such that the expressions are syntactically equal (i.e. tree-isomorphic). Nov 11 '19 at 23:57