tag:blogger.com,1999:blog-3722233.post5087276843942639614..comments2023-02-04T08:48:36.553-06:00Comments on Computational Complexity: Proving DFA-langs closed under concat and * without using equiv to NDFA's Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger16125tag:blogger.com,1999:blog-3722233.post-91826721762006923452013-03-01T11:03:04.158-06:002013-03-01T11:03:04.158-06:00ps re complementing the NFA without determinizing....ps re complementing the NFA without determinizing. on pondering this yrs ago, decided that there seems to be a natural generalization of NFAs as follows. instead of the halt state based on a multistate configuration landing in "any of S1" states where S1 is a set (as in determinization algorithm), consider a new concept of a multistate configuration landing in "all of S2" states where S2 is the complement of S1. but this does not seem to be considered in the literature. there is some discussion of this on a recent cs.se question:<br /><br /><a href="http://cs.stackexchange.com/questions/9954/is-there-a-efficient-test-for-if-an-nfa-accepts-a-subset-of-another-nfa/" rel="nofollow">Is there a efficient test for if an NFA accepts a subset of another NFA?</a>Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-284053723495693402013-03-01T10:58:12.797-06:002013-03-01T10:58:12.797-06:00ps re working with complements of DFAs, this quest...ps re working with complements of DFAs, this question popped up on cs.se recently & the answers relate to complementing an NFA without determinizing it 1st. when thinking about it yrs ago, decided there seems to be a natural generalization of an NFA which halting is based on a multistate transition landing in "all of S1" states where S is a set, in contrast to the standard halt condition of landing in "any of S2" states, where S1 and S2 are complementary states on the NFA. but havent seen this considered in the literature. maybe someone else?<br /><br /><a href="http://cs.stackexchange.com/questions/9954/is-there-a-efficient-test-for-if-an-nfa-accepts-a-subset-of-another-nfa/" rel="nofollow">Is there a efficient test for if an NFA accepts a subset of another NFA?</a>Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-10969333758839491992013-02-26T01:15:58.074-06:002013-02-26T01:15:58.074-06:00I agree with the last Anonymous post on Brzozowski...I agree with the last Anonymous post on Brzozowski derivatives. On a personal note, though, I think that the set difference operator is probably easier for an undergraduate class to grok than the complement operator. Maybe it's my inner category theorist talking, but I don't think that set complement is in any way natural.Pseudonymhttps://www.blogger.com/profile/04272326070593532463noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-32215148260225883252013-02-15T10:35:54.241-06:002013-02-15T10:35:54.241-06:00You can show pretty easily that regular languages ...You can show pretty easily that regular languages are closed under complement via Brzozowski derivatives.That is, you can directly show that Da(not(r)) = not(Da(r)), and then you can show separately that the set of derivatives (modulo the ACU axioms for +) of a regular expression r is finite, which gives you a DFA for recognizing a regular language. You never even have to mention the existence of NFAs.<br /><br />See "Derivatives of Regular Expressions", Janusz A. Brzozowski, Journal of the ACM, Volume 11 Issue 4, Oct. 1964, Pages 481-494. <br /><br />Derivatives give a very pretty, algebraic way of proceeding, without forcing you into the weeds of automata constructions. It's a shame they are not better-known.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-38540868527720339622013-02-14T15:16:49.610-06:002013-02-14T15:16:49.610-06:00hi UC ... yes of course did understand the paper i...hi UC ... yes of course did understand the paper is not presenting an automated proof. also the Jukna problem is far from being solved even with a powerful prover and even with lots of human hand holding. am just stating that its in the realm of possibility with a concerted attack. however, the myhill-nerode theorem is all about FSM optimization and leads to an actual algorithm given in Hopcroft & Ullman, intro to automata, languages, and computation. 1978. suspect some important proofs based on induction with FSM optimization are on the near horizon and that Jukna's problem is similar. and someday, maybe push button results will actually be possible. [thats whole other can of worms, I mean, another research program!]Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-4979239450149609662013-02-14T03:21:23.171-06:002013-02-14T03:21:23.171-06:00This brings up the question: Is it in the class LS...This brings up the question: Is it in the class LSSL (Limited Success Student Learnable)? Can we use it to separate LSSL from CRT?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-45679308423167235162013-02-13T19:36:35.096-06:002013-02-13T19:36:35.096-06:00I think there is a slight confusion. Notice I have...I think there is a slight confusion. Notice I have not written "automated theorem provers", but "interactive theorem provers". In interactive theorem proving we have the joke that thinking is only "Plan B" ("Plan A" being to first try quite powerful and integrated automated provers), but it is only a joke. The paper does not describe a push-button-result. On the contrary, it makes the case that even with such powerful tools a lot of (human) thinking is needed - in this case what is the right datastructure over which the proof should proceed. So I would not yet hold my breath that current technology in this area can on their own make any significant advances with open problems. But I am hoping too (and develop interactive theorem provers to be of more help in the future). Anonymoushttps://www.blogger.com/profile/12456191973008189690noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-89124707829875441642013-02-13T09:53:31.892-06:002013-02-13T09:53:31.892-06:00The question `is there a proof of closure under CO...The question `is there a proof of closure under CONCAT or * that only used DFA's' is of course an informal one. What I really wanted to know is `is there a proof I could show my class before they<br />saw DFA's' and to that the proof Richard emailed me WOULD suffice.<br />That is, it is simple enough to show them. (I did email them a link<br />to this post, though that was after they had seen the normal proofs.)<br /><br />By contrast, from the comments here, it seems that comp of reg exp<br />would not be in the class class-room-teachable.GASARCHhttps://www.blogger.com/profile/06134382469361359081noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-82652110338370550162013-02-13T03:02:09.663-06:002013-02-13T03:02:09.663-06:00Yes, Josh, this is in the paper of Yu et al. that ...Yes, Josh, this is in the paper of Yu et al. that I cited. They give exact bounds.Jeffrey Shallithttps://www.blogger.com/profile/12763971505497961430noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-74002472195487722322013-02-12T23:20:13.711-06:002013-02-12T23:20:13.711-06:00I agree with Jeff Erickson: those proofs seem like...I agree with Jeff Erickson: those proofs seem like they just take the conversion from NFAs to DFAs and "inline" them into the proof that DFAs are closed under concat and *. I wonder if one can show that at least the resulting blow-up in size is necessary, as in Jeffrey Shallit's answer: is there a regular language L where the size of the smallest DFA for L* is exponential in the size of the smallest DFA for L? (And the analogous idea for concat.)Josh Grochownoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-57839169467693383872013-02-12T19:09:07.653-06:002013-02-12T19:09:07.653-06:00Richard Beigel's constructions have been known...Richard Beigel's constructions have been known for a long time in the "state complexity" literature. The first appearance (with proof sketches only) seems to be in A. Maslov: Estimates of the number of states of finite automata, Soviet Mathematics Doklady, 11 (1970) 1373-1375. <br />Later the results were rediscovered and elaborated by S. Yu, Q. Zhuang, K. Salomaa, The state complexity of some basic operations on regular languages, Theoret. Comput. Sci. 125 (1994) 315–328.<br /><br />As for the question about regular expressions, there are recent results of Gelade and Neven exhibiting a family of regular expressions for which the smallest regular expression for the complement has a doubly-exponential blowup in size. So any direct construction of the complement from the regular expression will have to be rather complicated. See http://tocl.acm.org/accepted/401neven.pdf .Jeffrey Shallithttps://www.blogger.com/profile/12763971505497961430noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-58292417482909622352013-02-12T14:09:01.723-06:002013-02-12T14:09:01.723-06:00hi "UC". your paper is very interesting!...hi "UC". your paper is very interesting! was recently trying to convince stasys jukna to attack an important problem of his using an FSM minimization attack & suggested that automated theorem proving may someday crack problems somewhere in this area. your paper shows significant advancement in this area. now, can it be used to break some important open problems? the formalization of the <a href="http://en.wikipedia.org/wiki/Myhill%E2%80%93Nerode_theorem" rel="nofollow">myhill-nerode thm</a> seems like a huge step in this direction.<br /><br />his problem is to prove that bellman ford algorithm for shortest path is optimal and interestingly it seems to result in something that looks a lot like finding optimal FSMs. here is the problem on stackexchange.<br /><br /><a href="http://cstheory.stackexchange.com/questions/14591/combinatorics-of-bellman-ford-or-how-to-make-cyclic-graphs-acyclic" rel="nofollow">Combinatorics of Bellman-Ford or how to make cyclic graphs acyclic?</a><br /><br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-32943963488442874542013-02-12T12:34:03.964-06:002013-02-12T12:34:03.964-06:00See Moshe Vardi's lecture here:
http://www.fi...See Moshe Vardi's lecture here:<br /><br />http://www.fields.utoronto.ca/audio/11-12/CLS_constraint/vardi3/<br /><br />They had to deal with a similar issue.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-43221526464043855742013-02-12T11:49:16.562-06:002013-02-12T11:49:16.562-06:00In the context of interactive theorem provers, thi...In the context of interactive theorem provers, this is actually a serious<br />question: since it is really hard to reason formally about automata.<br />So my co-authors and I set out to prove the Myhill-Nerode theorem by only<br />using regular expressions (never introducing the notion what an automaton<br />is). Once you have the Myhill-Nerode theorem, closure under complementation<br />is trivial. The short paper appeared at ITP 2012; the longer version is<br />here <br /><br />http://www.inf.kcl.ac.uk/staff/urbanc/Publications/rexp.pdf<br /><br />So the short answer is it can be done.Anonymoushttps://www.blogger.com/profile/12456191973008189690noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-3480138343115633672013-02-12T11:25:33.619-06:002013-02-12T11:25:33.619-06:00I would argue that Richard's proofs are using ...I would argue that Richard's proofs <em>are</em> using equivalence with NFAs.JeffEhttps://www.blogger.com/profile/17633745186684887140noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-3375384085839373032013-02-12T10:59:52.915-06:002013-02-12T10:59:52.915-06:00Sounds like you need a programming language guy.Sounds like you need a programming language guy.Gretylhttps://www.blogger.com/profile/08176170219641912731noreply@blogger.com