[FOM] regular expressions

[Vaughan Pratt]

Adam Kolany wrote:
> I am sorry for possibly trivial questions:
>     1. Is the problem of equality of languages given by two regular
> expresions equal decidable?
>     2. Is there a (decidable) formal system for proving the above
> equalities?

Normally one would just answer this in the affirmative and point to any 
good automata text such as Hopcroft and Ullman, Lewis and Papadimitriou, 
Sipser, etc.  However this is a nice example of where there is a really 
slick proof that is essentially categorical in nature (exhibit the 
initial automaton and then the final automaton in the category of all 
deterministic automata accepting L) yet which doesn't require knowing 
any category theory to appreciate.  (Another such is the proof that two 
algebras freely generated by sets of the same cardinality are 
isomorphic.)  I believe the late Joe Goguen was the first to point this 
out.  I like this story enough that I can't resist telling it here.

For this purpose a deterministic automaton is any graph with set Q of 
vertices, possibly infinite, with one start state and an arbitrary set 
of final states (possibly empty, possibly all of Q), such that there are 
exactly |S| edges leaving each state, called the *transitions* from that 
state, each labeled with a different letter of the alphabet S.  Two or 
more of the edges from one state may go to the same state (this is the 
usual dispensation permitted for directed graphs whose edges are 
labeled---without labels graph theorists only allow one edge per ordered 
pair of vertices though category theorists don't feel so constrained). 
There are no epsilon transitions, every edge must be labeled with a 
single letter.

The crucial propositions are as follows.

Proposition 1.  Given any language L, as a subset of S*, there exists a 
canonical deterministic automaton A_L recognizing L.

(L need not be regular, or recursive, or recursively enumerable, it can 
be any language whatsoever.)

Proposition 2.  Any regular expression denoting a language L can be 
effectively transformed into A_L with a number of states at most 
exponential in the size of the regular expression.

For Proposition 1, take an infinite tree T all of whose vertices are of 
out-degree the cardinality s of the alphabet S.  All are of in-degree 1 
save the root vertex which is of in-degree zero.  There are no 
leaves---all paths are infinite.

Label the s edges leaving each vertex of T with the respective s letters 
of S.

Label the vertices of T with words from S* according to the labels on 
the path to that vertex from the root.  Thus the root will be labeled 
epsilon (the empty word), the s vertices immediately below the root will 
be labeled with the s one-letter words, and the s^n vertices n levels 
below the root will be labeled with the s^n n-letter words, for all 
natural numbers n (which is why every path from the root must be infinite).

Make T an automaton by taking its start state to be the root vertex of T 
and its set of final states to be the vertices of T labeled with members 
of L.

It should be clear that T is a deterministic automaton accepting L.  (It 
is in fact the initial such in a suitable category of all such.)

Now associate to every vertex v of T the language w\L defined as the set 
of those words x in S* such that wx is in L, where w is the word 
labeling v per the above procedure.  Call two vertices with labels v and 
w *equivalent* when v\L = w\L, that is, when the two subtrees with 
respective roots v and w are made equivalent automata by taking the 
respective subtree's root to be the start state in each case.  (The 
final states remain marked as originally.)

One can show that the automaton obtained by identifying equivalent 
vertices is the final automaton A_L in the category of all deterministic 
automata accepting L.  It has the further property that *any* automaton 
accepting L can be turned into the final one by identifying states (the 
sense in which it is final).  This is crucial for the last stage of the 
construction in Proposition 2.

It is further the case that A_L as defined above is finite if and only 
if L is regular.  (The initial automaton is always infinite as long as S 
is nonempty, the usual though not necessary assumption in automata 
theory.)  This automaton is the canonical deterministic finite state 
automaton A_L recognizing L, as promised by Proposition 1.  (It is also 
the minimal deterministic such, subject to a remark below.)

Proposition 2 is shown by a series of standard reductions.  First 
transform the regular expression into a nondeterministic finite state 
automaton A.  (The end product should have no epsilon transitions; a 
popular two-step approach first produces one with epsilon transitions 
and then eliminates them, but it can also be done in one step.)  Then 
"determinize" A by taking the set of states of A' to be the power set 
2^Q of the set Q of states of A.  Exercise: given a subset X of Q, 
determine the unique subset Y of Q that the transition from X labeled s 
must go to.  Then determine which subsets of Q should be the final 
states of A' and which the start state of A'.

The last step is to identify the equivalent states of A'.  (This is far 
from the fastest way but it is the easiest to describe.)  Start out with 
the very coarse equivalence relation such that two states are equivalent 
just when either both or neither are final (so there are only two 
equivalence classes, or one when all or no states are final).  Now 
refine this to the (new) equivalence relation holding between (old) 
equivalent states that also have (old) equivalent successor states. 
That is, if q is equivalent to q' before, and for all s the two states 
reached by the s-transitions from q and q' are equivalent before, then q 
and q' are still equivalent after, the new equivalence relation.  Refine 
to convergence (i.e. when nothing changes), necessarily in at most |2^Q| 
steps since no relation can be finer than the identity relation.  Now 
identify equivalent states.  The result is A_L.

To decide if two regular expressions are equivalent (denote the same 
language L), compute their respective canonical automata and test 
whether they are isomorphic.  (Isomorphism of automata is trivial to 
decide in comparison with graph isomorphism: start by pairing up the 
initial states, then the successor states of the initial states, and so 
on.  With graph isomorphism one does not have any good starting place in 
general.)

Note that this A_L is not necessarily minimal in the standard sense used 
in automata textbooks because some authors define "deterministic" to 
mean only that *at most* one s-transition leaves each state, whereas the 
definition needed for the above treatment calls for *exactly* one 
s-transition.  The difference is that the A_L produced above will in 
general (but not always) include a state that leads to no final state; 
the other definition eliminates that state (but no other) out of a sense 
of efficiency.

Also note that the initial and final automata are always connected and 
countable (provided the alphabet is countable), but that other automata 
in the category of automata accepting L need be neither.  These are 
points that are almost never made in automata theory texts but that 
should appeal to FOM subscribers.

============

Regarding the second question on formal systems, there are two good 
axiom systems, each with its own merits.

1.  Kleene algebras.  This is a quasiequational theory which proves 
exactly the identities of regular algebra, such as a** = a*, a(ba)* = 
(ab)*a, and so on.  The first nontrivial result about axiomatizing these 
identities is due to V. Redko in 1967 who showed that no finite set of 
equations could axiomatize them.  Arturo Salomaa then gave an axiom 
schema for the theory.  In 1971 John Conway (of Life and surreal-numbers 
fame) wrote a book on the subject which includes the observation that 
the equational theory includes a four element algebra in which aa = a 
yet a* is not equal to a, i.e. a nonstandard model.  In 1990 Dexter 
Kozen gave a finite equational theory together with a quasiequation 
expressing induction, the equations of which were the desired equations 
and which did not have Conway's nonstandard model.  Kozen defined a 
Kleene algebra to be any model of this quasiequational (universal Horn) 
theory.  For more details see the relevant Wikipedia article at 
http://en.wikipedia.org/wiki/Kleene_algebra .

I'm embarrassed to say I don't know what's known about decidability of 
Kleene algebra.  The Wikipedia article doesn't address the question.

2.  Action algebras.  In 1990 I posed and answered affirmatively the 
question of whether the equational theory of regular expressions had a 
finitely axiomatizable equational conservative extension.  That is, 
could there be a superset of the regular operations and a finitely 
axiomatized theory thereof, such that those equations in the language of 
regular expressions were exactly the regular identities defined by 
Kleene and studied by Redko, Salomaa, etc.  The extension amounts to 
adding "guards" or "tests" to the language of regular expressions, so 
one can think of the language of action algebra as guarded regular 
expressions.  The two new constructs are a --> b and a <-- b, understood 
as assertions "if a before then b now" and "a now if ever b in the 
future".  Concatenation ab is viewed as conjunction ("a and then b") 
while a+b is disjunction ("a or b").  The crucial axiom pinning down * 
is (a --> a)* |- a --> a, where |- can be read as <= (less-or-equal), 
with a <= b in turn being viewed as an abbreviation for a+b = b.  (Or 
more simply (a --> a)* = a --> a which is equivalent but less elegant, 
asserting that a --> a is its own reflexive transitive closure.) 
Conway's nonstandard model is killed off by this equational theory, and 
moreover in every model of the theory a* is reflexive transitive closure 
in the sense that a is reflexive when 1 <= a and transitive when aa <= 
a.  For more details see the relevant Wikipedia article at 
http://en.wikipedia.org/wiki/Action_algebra .

It is a long-standing (17 years) open problem whether action algebra is 
decidable.  This has been looked at by a number of algebraists, mainly 
in Europe, so far without success.

Vaughan Pratt