-2
$\begingroup$

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 ?

Improve this question
$\endgroup$
5
  • $\begingroup$ Could you rewrite them in Ruby :) I don't follow your syntax. rubular.com $\endgroup$
    – Chad Brewbaker
    Aug 16 '13 at 15:25
  • $\begingroup$ @ChadBrewbaker: Thanks, didn't consider the ambiguity when typing out..added. $\endgroup$
    – manasij7479
    Aug 16 '13 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$
    – Igor Shinkar
    Aug 16 '13 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$
    – manasij7479
    Aug 16 '13 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$
    – Igor Shinkar
    Aug 17 '13 at 6:29
13
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ How does this compare with Salomaa's classic Two complete axiom systems for the algebra of regular events? $\endgroup$
    – Yuval Filmus
    Aug 16 '13 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 '13 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 '20 at 11:28
  • 1
    $\begingroup$ @stefanh Ooops! Thanks, corrected. $\endgroup$
    – J.-E. Pin
    Apr 29 '20 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.