Andrew Lentvorski wrote: > Christopher Smith wrote: >> Hmm... I can't think of how one might do the NDFA/DFA proof > > A DFA can always be constructed from an NDFA. I understand the proof, I'm just not sufficiently skilled with an FPL to figure out a way to validate such a proof with a compiler. >> certainly your typical Haskell or ML compiler can verify the equivalence >> of a transform. > > There's a whole bunch of theoretical math folks who wish that were > true... > > Even checking the equivalence of two VLSI state machines (very > structured, well-defined, etc.) is O(n^2) or worse (normally much > worse). Actually returning useful information about *where* those > things differ always much worse than O(n^2) (normally O(2^n), IIRC). I didn't say that it'd be fast, merely that it'd be possible. Validating equivalence is very different identifying where the differences are (I can't think of a way to do that with an FPL).
--Chris -- [email protected] http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-lpsg
