-4
$\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 ?

|cite|improve this question
$\endgroup$
  • $\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
  • 1
    $\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
  • $\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
10
$\begingroup$

The identity $(x + y)^* = x^*(xy^*)^*$ 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

|cite|improve this answer
$\endgroup$
  • 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

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.