Note that the 12,701 character regex is WRONG. It doesn't even match "70". Even the binary regex is wrong.

The original 32K regex pointed to in the stackexchange problem statement however is perfectly correct.

Test code:

    open(F, '< /tmp/q.in');
    $myre = <F>;
    chomp($myre);
    $myrecomp = qr/^(?:$myre)$/;
    while (<>) {
      chomp();
      if (m/$myrecomp/) {
        print "$_\n";
      }
    }

Examples of multiples of 7 not matched by the given regex: 70, 707, 7007, 11095

(I spent all morning trying to find the bug in my regex compiler based on the assumption that the answer there was correct)

> a 12,701 character regex for divisibility by 7:

I wonder if that's the optimal regex or can be reduced further using some rules[1] like the ones which we(humans) generally use to do it manually.

[1]. https://www.math.hmc.edu/funfacts/ffiles/10005.5.shtml

I wrote a 11811-character regex for divisibility by 7 back in August 2008: http://web.mit.edu/andersk/Public/regex

And unlike the one on stackexchange, it's actually correct!

(I have a regex -> DFA compiler here that I just threw your regex through. Seven states, connected as expected)

Do you have the source to the program you wrote the regex with? (Or did you write it by hand?)

It's definitely not the optimal regex. Finding the smallest regex is a hard problem (at least in theory): https://cs.stackexchange.com/questions/19686/is-regex-golf-n...

(I think I've read that finding the smallest one is not only NP-hard, but P-Space complete.)

Don't regular expressions have minimal, canonical forms?

The minimum DFA does not correspond in any particular sense to a minimal regular expression.

Of course not - my bad!

Yes they do. For reference, check Sipser.

Could you give a page number? I skimmed the regular expression section and couldn't find it. Also, while it is self-evident to me that there is a minimal form for each regex, the construction for finding one isn't immediately obvious to me (I can surely enumerate several ways of eliminating redundancy). Beyond that, I'm not sure a minimal form would minimize character length.

Of (a \star b \star ) \star and ( a ∪ b ) \star, which is the canonical form? The transformation from the former to the latter is nontrivial as a \star b \star is not equivalent with a ∪ b.

Of course, there is a shortest equivalent regular expression, but in general it's PSPACE-complete to find it: https://en.wikipedia.org/wiki/PSPACE-complete#Regular_expres...

It remains PSPACE-complete if you're given a corresponding DFA: "Jiang and Ravikumar [7] show moreover that the minimization problem for ... regular expressions remains PSPACE-complete, even when specifying the regular language by a dfa" from http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.60....

In that sense, the grandparent is incorrect. It is unknown, in both practice and theory, how to find the shortest equivalent regex.

It's not unknown, it just takes a long time.

I think you should think deeper on the idea of "unknown"

I don't understand what you mean. Regex minimization is in PSPACE, so take any PSPACE complete problem, eg Q-Sat, do the reduction and apply the algorithm. Q-Sat can be solved by recursively enumerating all possibilities. So there is a method for minimizing regular expressions. It just takes a long time to run. If you have time you can probably think of an algorithm that works directly on the regex problem without doing the Q-Sat thing. It might even be faster.

Heck, there might be an algorithm that works really well in practice. People who do model checking and verification laugh PSPACE completeness in the face and are not even really concerned with undecidability.

I would be very interested in finding an approach that works well in practice.

Okay, fine, but in this case N=7. What are the constant factors?

The weird part is that the regex is much bigger than the DFA (but the DFA is not accepting the symbols directly, it's transforming them first

It also seems that regexes can't express accepting expressions like AB where A is accepted by itself (considering AB is accepted), which in the DFA is implemented by sending it to the initial state

> It also seems that regexes can't express accepting expressions like AB where A is accepted by itself (considering AB is accepted), which in the DFA is implemented by sending it to the initial state

B* does that.

This is a DFA over the alphabet {0, 1} where the number is first transformed by writing out each digit in unary with 1 and delimiting digits with 0.

Wow, I'm famous.