The World's Shortest Proof of Parikh's Theorem
Mark Hopkins
Otherwise known as: The Untold Story of Formal Language Theory 4.
Other parts of this series are contained in sci.math.research, and are also
available (for a limited time) direct by e-mail. The term "Rational
Monoid" is defined in part 1 and is referred to here, but is not used in
this presentation (which is self-contained).
This theorem will be formulated in a general context of "Kleene Monoids",
whose axiom set is weaker than that of "Rational Monoids" presented in
previous articles. What we will show is that every system of equations over
an Abelian Kleene Monoid has a least solution, and we can find this solution
in closed form by applying the result:
The least solution to f(x) <= x
is f(0) f'(f(0))*
where f(x) is in K[x], the (Abelian) extension of a Kleene Monoid K by x
and where f'(x) denotes the *derivative* of f(x) with respect to x.
The significance of this result is the emergence of an analytic structure
on a formal language algebra. This structure, in fact, is cosistent with
the structure found by Brzozowski in 1964 for the algebra of regular
expression
and extends it into the Abelian domain, where it is MUCH more well-behaved.
In fact, we can even write down a Taylor's Theorem:
f(x + h) = f(x) + h f'(x + h)
and it is directly from this that the result above follows(!)
(4.1) Kleene Monoids
Like a Rational Monoid, a Kleene Monoid is a partially ordered monoid
with the following properties:
(1) Every finite subset has a least upper bound
(2) lub (A B) = (lub A) (lub B) where A, B are finite
(3) 1, a a* and a* a are all <= a*
(4) If a, bx, xc are all <= x then so is b* a c*.
An equivalent definition was formulated by Kozen in a 1994 issue of
_Information and Computation_ (I forget the title off-hand), which was also
proven to be equationally complete over the algebra of regular expressions:
DEFINITION: A Kleene Algebra K is an idempotent semiring --
(1) (ab)c = a(bc) (a+b)+c = a+(b+c)
a1 = a = 1a a+0 = a = 0+a
a(b+d)d =abd+acd a+b = b+a
a0d = 0 a+a = a
with an operator a |-> a* such that:
(2) 1 + a a* <= a*
(3) If a + b x <= x then b* a <= x
If a + x c <= x then a c* <= x
where the ordering relation is defined by a <= b if and only if a + b = b.
One can define a Kleene Monoid homomorphism as a monoid homomorphism
which preserves the star and the least upper bounds of finite subsets.
This will also be equivalent to the correspoonding notion of a Kleene
Algebra homomorphism (which preserves sums, products and the star).
With equational completeness, all the proerties of regular expressions
will be true in a Kleene Monoid, e.g.
a* a* = a** = (1 + a)* = a* = 1 + a a*
a (b a)* = (a b)* a
0* = 1* = 1
(a* b)* a* = a* (b a*)* = (a + b)*
and so on. The interested (and motivated) reader may want to try and
prove these directly from the axioms above.
Also one has the following properties:
THEOREM: The 3 basic operations are all order-preserving.
THEOREM: If X is the least solution to the fixed-point inequality f(x) <= x
where f(x) is an order-preserving function of x, then it is also
the least solution to the equation f(x) = x.
THEOREM: Every f(x) in K[x], the free (or Abelian) extension of a Kleene
Monoid by x, is an order-preserving function of x.
Examples of fixed-point inequalities with general solutions are the following:
THEOREM: The following inequalities have the following least fixed-point
solutions:
a + bx + xc + xdx <= x x = b* a c* (d b* a c*)*
a + xdx <= x x = a (d a)* = (a d)* a
a + bx <= x x = b* a
a + xc <= x x = a c*
(4.2) Abelian Kleene Monoids
In an abelian Kleene Monoid, the operator a |-> a* will play a role that
is completely analogous to the exponential function. The reason for this
can be seen as follows. In the stronger algebra, Rational Monoids, we
have the definition
a* = lub { a^n: n >= 0 }
which can be expressed formally as the infinite sum, since sums in Rational
Monoids are least upper bounds:
a* = 1 + a + a^2 + a^3 + ...
However, a Kleene Monoid (and Rational Monoid) have idempotent sums.
Therefore 2a = a + a = a, 3a = 2a + a = a + a = a, and generally na = a
for n =1, 2, 3, ... This can also be extended to fractional n. Therefore,
a* can also be written formally as the sum:
a* = 1 + a + a^2/2 + a^3/3! + ... = exp(a)
The forms that this correspondence take is as a law of exponents:
THEOREM: In Abelian Kleene Monoids, (a + b)* = a* b*
and as a function invariant under a naturally occurring formal derivative
operator.
Proof (of exponential rule):
The expression (a + b)* is the least solution to the equation
x = 1 + (a + b)x = 1 + ax + bx
and a* b* to
x = 1 + ax + xb
Both equations are equivalent when the algebra is Abelian. Threfore by
the uniqueness of the least solution, (a + b)* = a* b*.
We can also extend the absorption rule b* b* = b* to the following form:
THEOREM: If f(x) is in K[x], the Abelian extension of an Abelian Kleene
monoid K, then f(a b*) b* = f(a) b*
Proof:
By induction over K[x]. We only show that the theorem is invariant
with respect to the star operation, the rest is left to the reader.
Let f(x) be in K[x], and assume the theorem holds true of it. Then
(f(a b*))* b* = (f(a b*) + b)* = b* (f(a b*) b*)*
and the latter term reduces to b* (f(a) b*)* by assumption, so after undoing
the steps above, we get f(a)* b*.
(4.3) The Analytic Structure on K[x].
Let K be an Abelian Kleene Algebra, and K[x] the Abelian extension of K
by x. Then we can define the following operation:
DEFINITION: d/dx
dk/dx = 0, dx/dx = 1
d(A*)/dx = dA/dx A*, d(A+B)/dx = dA/dx + dB/dx
d(AB)/dx = dA/dx B + A dB/dx
where k is an element of K
That this definition defines a unique operator follows from the definition
of K[x] by induction. That it is well-defined (i.e. invariant under the
axioms for a Kleene Monoid/Algebra, as well as under the equality of terms
in K) needs to be proven by induction and it is something that makes
cruciel use of the Abelian property.
Without the Abelian property, in fact, the d/dx operator will split into
two distinct operators, "Left quotient" and "right quotient", which were
first discovered by Brzozowski in 1964. Neither operator exactly satisfies
the Leibnitz property, but both satisfy a limited form of Taylor's Theorem.
THEOREM: d/dx is well-dfined over K[x].
Proof:
We'll only show the invariance under axiom (2) of the definition of
Kleene Algebras:
d(1 + A A* + A*)/dx = d1/dx + dA/dx A* + A d(A*)/dx + d(A*)/dx
= 0 + dA/dx A* + A dA/dx A* + dA/dx A*
= dA/dx A* (1 + A)
= dA/dx A* = d(A*)/dx
noting that A* (1 + A) = A* + A* A = A*, and that the inequality in the
axiom (2) when written as an equation is:
1 + A A* + A* = A*
The other axioms (including (3)) can be done just as easily. Note that
d/dx is invariant with respect to equality of terms in K since it maps
everything in K to 0.
THEOREM: Taylor's Theorem -- f(x + h) = f(x) + h f'(x + h)
The proof also proceeds by induction, over all f(x) in K[x]. This is also
fairly routine, though care must be taken in ensuring the invariance of
the theorem with respect to the star operator. In particular, if the
theorem holds of f(x), then:
f(x + h)* = (f(x) + h f'(x + h))*
= f(x)* (h f'(x + h))*
= f(x)* (1 + h f'(x + h) (h f'(x + h))*)
= f(x)* + h f'(x + h) f(x)* (h f'(x + h))*
= f(x)* + h f'(x + h) f(x + h)*
where f'(x) denotes d/dx f(x), for each f(x) in K[x] and note that
d/dx f* = df/dx f* = f' f*
therefore if we define g(x) = f(x)* the above equation reads
g(x + h) = g(x) + h g'(x + h).
As a couple corollaries we list the following:
COROLLARIES: f(x) = f(0) + x f'(x), for f(x) in K[x].
f(a b*) = f(0) + a f'(a) b*
The second result is a special case of the first with the absorption
property used to reduce a f'(a b*) b* to a f'(a) b*.
(4.4) Parikh's Theorem
And now on to the matter at hand: the Shortest and simplest proof
ever of Parikh's Theorem. Note that even finding a direct equation-
solving proof in the first place was an open problem of sorts -- until
now.
THEOREM: If f(x) is in K[x], K an Abelian Kleene monoid, and K[x] its
Abelian extension by x, then the least solution to f(x) <= x
is f(0) f'(f(0))*.
Proof:
By Taylor's Theorem, we may write:
f(0) + x f'(x) = f(x) <= x
Therefore,
f(0) f'(x)* <= x
and by monotonicity of f'(x) (since f(0) <= x):
f(0) f'(f(0))* <= f(0) f'(x)* <= x
So it's a lower bound onn all solutions.
But it's also a solution. For convenience, let a = f(0) and b = f'(a).
Then
f(a b*) = f(0) + a f'(a) b*
= a + a b b*
= a (1 + b b*)
= a b*
Amazing, isn't it?
========================================