Re^2: Comparative satisfiability of regexps.

[hardburn]

"Compiler optimizations" :)

Seriously, an optimizer's job is to anaylize code, realize that it is computationally equivilent to another peice of code, and then using the better version ("better" could be one or more of less processor time, RAM, space on disk, etc.).

I'm not sure if this is useful here or not, though.

[Meowse]

Which brings to mind a good point, for which I thank you. That is--the challenge "compare two algorithms, and decide if they do the same thing" is provably incomputable in the general case (c.f. "the Halting Problem")--and yet, compilers replace code with more efficient but guaranteed-identical code every day. Thus, while it might not be possible to determine for all regexps whether one is a subset of another, it may well be possible for most regexps to determine if one is a subset of another.

And this is all that is needed in our case, because we're trying to derive as much information as possible, not all information. If we can only prove nine of ten steps in a process, we can't say that we've proven the process, but we're a lot better off than if we couldn't prove any of them.

So. If we restate the problem as "For most simple regexps, determine whether regexp A matches a subset of the strings that regexp B matches", does that make it seem more tractable?

Hopefully,

Mickey.

[demerphq]

I think you are confusing "proving any arbitrary algorithm is formally equivelent to another arbitrary algorithm" with "find an algorithm Y that is more efficient yet formally equivelent to algorithm X". Since we know that there are an infinite number of algorithms that are formally equivelent to any given algorithm the latter isnt such a difficult problem, especially not for a human and not when X is particularly inefficient. Also a lot of optimisation code is pretty simple in principle replacing templates that match a certain pattern with other templates that do the same thing more efficiently, and still there is no guarantee that your compilers optimizations actually work.

I think all you can do is show us what type of regexes you mean, and perhaps we can advise based on that.