4 ms·

Here we hit against a law of nature: there is no algorithm that would analyze an arbitrary piece of code and determine whether it will only produce valid search

• nostrademons 18y ago
  In order to produce a valid search tree, the code must halt. Therefore, an algorithm that can tell whether an arbitrary piece of code will produce valid search trees can tell whether that piece of code will halt. This isn't really a good example though, because it's quite possible to examing an arbitrary piece of code and, assuming it halts, determine whether it will produce valid search trees. The Haskell and ML typecheckers are existence proofs for this, as is the static typechecker that Wadler did as a bolt-on addition to Erlang.
  • Herring 18y ago
    roughly how does the assumption help?
  • ntoshev 18y ago
    More practically, the "arbitrary piece of code" can be expressed in a less-than-turing-complete language or language subset, and it would actually be possible to prove useful things about it.
• andrejbauer 18y ago
  It is a classic diagonal argument. Suppose algorithm P determines whether a given algorithm produces a valid search tree. Consider the following algorithm Q: "if P(Q) the produce invalid tree else produce valid tree." In words, the algorithm Q does the opposite of what P predicts. Such Q exists by Kleene's Recursion Theorem (or simply because you can write its code in your favorite language).