Re^3: Comparative satisfiability of regexps.

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.

Comment on Re^3: Comparative satisfiability of regexps.

Replies are listed 'Best First'.
Re^4: Comparative satisfiability of regexps. by demerphq (Chancellor) on Jan 19, 2005 at 22:12 UTC
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. --- demerphq	[reply]

Replies are listed 'Best First'.

Re^4: Comparative satisfiability of regexps.
by demerphq (Chancellor) on Jan 19, 2005 at 22:12 UTC

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.

---
demerphq

[reply]