# Error in Conway's "Regular Algebra and Finite Machines"

I was following “Proof Pearl: Regular Expression Equivalence and Relation Algebra” (Krauss & Nipkow, 2012) to implement a **regular expression equivalence checker** in OCaml to validate it as a project idea for my “Advanced Topics in Automata, Languages and Compilers” course.

Once the neat implementation was done, I wanted to test it, especially with pairs of regular expressions that aren’t trivially equivalent. I scoured the internet (mostly Stack Overflow) and the literature for such examples. Eventually I stumbled upon **“Regular Algebra and Finite Machines”** (Conway, 1971).

## The error

Deep into the book, on page 121 it contains the following exercises:

(Here \(+\) indicates the regex operator `|`

, \(1\) is the empty string aka \(\varepsilon\) and \([]\) are just nested parenthesis for grouping, not a regex character class.)

Exercise 3 asks us to prove that `(xy)*(x|xy(yy*x)*)*`

is equivalent to `((xy*y)*yx|x)*(xy)*`

. However, my checker didn’t agree and spat out the **counterexample yx**. Indeed, it’s not too hard to verify by hand that the first regex does not match

`yx`

while the second regex does. Hence, they aren’t equivalent!## The fix

The correct formulation of exercise 3 would be:

\[(\boldsymbol{yx})^*[x+xy(yy^*x)^*]^* = [(xy^*y)^*yx+x]^*(xy)^*.\]The difference compared to the book is shown in **bold**: beginning of the left-hand side should have `yx`

instead of `xy`

. My checker agrees that the two are now equivalent.

This is indirectly corroborated later in the book as well. Solutions to the exercises say:

A proof of 3 (not from C1-14) is implicit in later exercises.

And exercise 9 includes the fixed left-hand side regular expression.