Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2008-11-26

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:03 lispy Does coq have a way to extract the run-time complexity?
01:03 Heffalump time complexity?
01:03 lispy yeah
01:04 lispy like the bigO
01:04 Heffalump I doubt it could do it automatically.
01:04 Heffalump I guess in principle you could write proofs about it.
01:04 lispy I thought maybe when you have a proof of termination that it could be done by the machine
01:04 lispy I really don't know if this is a hard problem or not
01:05 Heffalump termination proofs in that setting are generally done just by restricting the language
01:05 lispy But, say you're using structural recursion, then the time complexity shouldn't be too hard right?
01:05 Heffalump you can't play the same game so easily for time complexity (though see the work of Bellantoni and Cook in that area)
01:06 lispy Cook proved 3sat is NP-hard right?
01:06 lispy I'm not familiar with anything else by himm
01:06 Heffalump I think in cases where the complexity is easy to see by eye, you could (relatively) easily add the complexity proof to the main proof.
01:06 Heffalump "A New Recursion-Theoretic Characterization of the Polytime Functions"
01:07 Heffalump and yes, I think so re 3sat
01:16 Igloo That's not too useful for camp at least, because it's easy to work out by hand
01:19 lispy Igloo: cool
01:19 lispy It was more of a general wonderment on my part Ithink...
01:19 lispy just idle thought
01:19 lispy But, I'm glad to hear you can work out your complexities
01:19 lispy I wish we had tht with darcs
01:20 lispy I have no idea what the complexity of darcs is, space or time
01:20 lispy I just know that it tends to suck :)
01:20 lispy Either that or we have really bad constants
01:30 Igloo It's a little harder for darcs, but working it out isn't very useful from teh PoV of making darcs faster
03:52 lispy I disagree :)
08:50 arjanb joined #darcs-theory
10:36 kowey joined #darcs-theory
14:40 kowey joined #darcs-theory
15:27 arjanb joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary