On Fri, Jan 25, 2008 at 10:57:36AM -0800, SJS wrote:
And when it comes to code, there's nothing "easily provable". That's just mathematician-speak for "I told me thesis student to do it."
But there is a lot more value in constructs that are easier to reason about. Problems that involve complex interacting parts are hard to reason about, and therefore it is easier to have problems. Sometimes, a recursively represented problem is easier to reason about, especially things like termination. You can do similar kinds of things with iteration, for example Eiffel's loop invariant constructs (You give a value that must start as a non-negative integer. It must decrease each iteration of the loop, and never go negative. If you can find such a value your loop will either terminate or signal an error when the value either doesn't decrease or goes negative. Common values are the size of a data structure, remaining items to process, and stuff like that). Recursing maps nicely to proof by induction. Even just testing at the REPL, you can start with the end cases and make sure it does the right thing, and then construct an argument one recurse above that, trace the recursive call, and make sure the inductive step works right. It gives you more confidence that it will work on other inputs. I've used the Coq theorem prover to prove correctness of a simple recursive definition. It was possible but very painful, and didn't give me any more confidence in it's correctness than intuition and testing would. Dave -- [email protected] http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-lpsg
