<p>The identity <span class="math-container">$(x + y)^* = x^*(yx^*)^*$</span> 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.</p>

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

<p>D. Krob, A complete system of <span class="math-container">$\mathcal{B}$</span>-rational identities. Automata, languages and programming (Coventry, 1990), LNCS 443, Springer, New York, (1990) 60--73. <a href="http://dx.doi.org/10.1007/BFb0032022" rel="nofollow noreferrer">DOI</a></p>

<p>D. Krob, Complete Systems of <span class="math-container">$\mathcal{B}$</span>-Rational Identities, <em>Theor. Comp. Sci</em>. <strong>89</strong> (1991), 207–343. <a href="http://dx.doi.org/10.1016/0304-3975(91)90395-I" rel="nofollow noreferrer">DOI</a></p>

<p>See also for a complete theory:</p>

<p>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</p>

<p>and for a related discussion for deciding the corresponding equational theory in Coq:</p>

<p>T. Braibant, D. Pous, <a href="http://arxiv.org/pdf/1105.4537.pdf" rel="nofollow noreferrer">Deciding Kleene algebras in Coq</a>, Log. Methods Comput. Sci. 8 (2012), no. 1, 1:16, 42 pp. <a href="http://dx.doi.org/10.1007/978-3-642-14052-5_13" rel="nofollow noreferrer">DOI</a></p>

CC BY-SA 3.0
2013-08-16T19:01:36.750Z
How does this compare with Salomaa's classic *Two complete axiom systems for the algebra of regular events*?
Yuval Filmus
CC BY-SA 3.0
2013-08-16T19:22:02.960Z
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.
J.-E. Pin
CC BY-SA 4.0
2020-04-29T11:28:51.563Z
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$.
StefanH
CC BY-SA 4.0
2020-04-29T11:32:39.093Z
@stefanh Ooops! Thanks, corrected.
J.-E. Pin
CC BY-SA 4.0
2013-08-16T18:17:50.443Z
2020-04-29T11:32:33.990Z
2020-04-29T11:32:33.990Z
J.-E. Pin
<p>The task is to prove that (0+1)* and 0*(1.0*)* are equivalent.<br>
1. <a href="http://rubular.com/r/K9Hp9tU6px" rel="nofollow">http://rubular.com/r/K9Hp9tU6px</a><br>
2. <a href="http://rubular.com/r/N8VpoEcch4" rel="nofollow">http://rubular.com/r/N8VpoEcch4</a><br>
EDIT: Forgot that + was ambiguous here!</p>

<p>I want to prove that the second expression accepts all binary strings, without constructing the equivalent DFAs manually.<br>
Induction comes to mind, but I am probably missing something crucial.<br>
Can anyone of you recommend a few good methods that I can use here?<br>
Also, relevant identities are welcome.<br>
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 ?</p>

CC BY-SA 3.0
2013-08-16T15:25:40.630Z
Could you rewrite them in Ruby :) I don't follow your syntax. http://rubular.com/
Chad Brewbaker
CC BY-SA 3.0
2013-08-16T15:41:46.310Z
@ChadBrewbaker: Thanks, didn't consider the ambiguity when typing out..added.
manasij7479
CC BY-SA 3.0
2013-08-16T15:48:15.047Z
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...
Igor Shinkar
CC BY-SA 3.0
2013-08-16T15:51:52.970Z
@IgorShinkar: How do I enumerate all the way to 'all possible strings' that way, by choosing specific subsets at a time?
manasij7479
CC BY-SA 3.0
2013-08-17T06:29:35.673Z
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...
Igor Shinkar
<automata-theory><regular-expressions>
Can I show algebraically that this regular expression accepts all binary strings?
manasij7479
# Can I show algebraically that this regular expression accepts all binary strings?

(Asked by: username_0 on 2013-08-16)

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 ?

**Tags:** automata-theory, regular-expressions

> **Comments:**
> **username_1**: Could you rewrite them in Ruby :) I don't follow your syntax. http://rubular.com/  
> **username_0**: @ChadBrewbaker: Thanks, didn't consider the ambiguity when typing out..added.  
> **username_2**: 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...  
> **username_0**: @IgorShinkar: How do I enumerate all the way to 'all possible strings' that way, by choosing specific subsets at a time?  
> **username_2**: 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...  

---

## 1 answers

### Answer by username_3 on 2013-08-16. Score: 13 | Accepted answer

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](http://dx.doi.org/10.1007/BFb0032022)

D. Krob, Complete Systems of $\mathcal{B}$-Rational Identities, *Theor. Comp. Sci*. **89** (1991), 207–343. [DOI](http://dx.doi.org/10.1016/0304-3975(91)90395-I)

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](http://arxiv.org/pdf/1105.4537.pdf), Log. Methods Comput. Sci. 8 (2012), no. 1, 1:16, 42 pp. [DOI](http://dx.doi.org/10.1007/978-3-642-14052-5_13)

> **Comments:**
> **username_4**: How does this compare with Salomaa's classic *Two complete axiom systems for the algebra of regular events*?  
> **username_3**: 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.  
> **username_5**: 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$.  
> **username_3**: @stefanh Ooops! Thanks, corrected.  

---

