The task is to prove that (0+1)* and 0*(1.0*)* are equivalent.
1. http://rubular.com/r/K9Hp9tU6px
2. http://rubular.com/r/N8VpoEcch4
EDIT: Forgot that + was ambiguous here!

I want to prove that the second expression accepts all binary strings, without constructing the equivalent DFAs manually.
Induction comes to mind, but I am probably missing something crucial.
Can anyone of you recommend a few good methods that I can use here?
Also, relevant identities are welcome.
As a generalization of my question here, does a generic pattern for proving "A language is accepted by R1 if and only if it is accepted by R2" exist ?

  • $\begingroup$ Could you rewrite them in Ruby :) I don't follow your syntax. rubular.com $\endgroup$ Aug 16, 2013 at 15:25
  • $\begingroup$ @ChadBrewbaker: Thanks, didn't consider the ambiguity when typing out..added. $\endgroup$ Aug 16, 2013 at 15:41
  • 2
    $\begingroup$ Take a string $s \in \{0,1\}^*$ and try to prove that it is in $0^*(10^*)^*$. Start with a string $s$ that consists only of zeros. Then try a string that contains a single 1. And so on... $\endgroup$ Aug 16, 2013 at 15:48
  • $\begingroup$ @IgorShinkar: How do I enumerate all the way to 'all possible strings' that way, by choosing specific subsets at a time? $\endgroup$ Aug 16, 2013 at 15:51
  • 1
    $\begingroup$ Don't worry about enumeration. It is enough to prove that any string belongs to $0^*(10^*)^*$. For example, try to understand first why $0010 \in 0^*(10^*)^*$ just get the feeling of what's going on. Then try to see why $001010 \in 0^*(10^*)^*$. Just try a few examples... $\endgroup$ Aug 17, 2013 at 6:29

1 Answer 1


The identity $(x + y)^* = x^*(yx^*)^*$ is a classical identity of regular expressions, but it is a nontrivial problem to find a complete set of identities for regular expressions. An infinite complete set was proposed by John Conway and this conjecture was ultimately proved by D. Krob.

J.H. Conway, Regular algebra and finite machines, Chapman and Hall, 1971, ISBN 0-412-10620-5

D. Krob, A complete system of $\mathcal{B}$-rational identities. Automata, languages and programming (Coventry, 1990), LNCS 443, Springer, New York, (1990) 60--73. DOI

D. Krob, Complete Systems of $\mathcal{B}$-Rational Identities, Theor. Comp. Sci. 89 (1991), 207–343. DOI

See also for a complete theory:

S. L. Bloom and Z. Ésik. Iteration Theories: the Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1993. xvi+630 pp. ISBN: 3-540-56378-4

and for a related discussion for deciding the corresponding equational theory in Coq:

T. Braibant, D. Pous, Deciding Kleene algebras in Coq, Log. Methods Comput. Sci. 8 (2012), no. 1, 1:16, 42 pp. DOI

  • 2
    $\begingroup$ How does this compare with Salomaa's classic Two complete axiom systems for the algebra of regular events? $\endgroup$ Aug 16, 2013 at 19:01
  • 2
    $\begingroup$ Salomaa's system makes use of an axiom scheme which permits essentially to formally solve linear systems. So it is not a set of identities but a more powerful mechanism. $\endgroup$
    – J.-E. Pin
    Aug 16, 2013 at 19:22
  • 1
    $\begingroup$ I guess the right hand side of your identity should read $x^*(yx^*)^*$, i.e., $x$ and $y$ be switched underneath the outmost star. As written, for example, it would not match $y$. $\endgroup$
    – StefanH
    Apr 29, 2020 at 11:28
  • 1
    $\begingroup$ @stefanh Ooops! Thanks, corrected. $\endgroup$
    – J.-E. Pin
    Apr 29, 2020 at 11:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.