Hacker News Reader

Comment by stygianguest | Hacker News Reader

Only proofs in 'constructive' logic. There's a lot of proofs that aren't executable. Most importantly proofs by contradiction.

See: http://en.wikipedia.org/wiki/Intuitionistic_logic

In practical terms, however, this isn't a huge hurdle and comes with the nice advantage that you always have a program.

BTW. I'm kinda sure you know this already, but I think it is important to mention.

Thanks for the Haskell proof-book link. I'll check it out sometime.

View on HN

Hmm, I don't understand the problem. There is a philosophical question there, of course, but as long as you assume something like the law of excluded middle, you can easily set up a proof system allowing you to execute proofs by contradiction. This is a common strategy in Coq, for instance.

Maybe I'm not understanding your point, though. I also don't think this chain of conversation is the sense that darkxanthos meant, either :)

The idea is that the Curry-Howard isomorphism allows you to "play" with constructive mathematics easily. For example, consider the fact that the composition of two functions f and g is continuous if each function is continuous. Suppose f : X -> Y and g : Y -> Z. Then, in pseudo-Haskell syntax, we could say

  continuousf  : Open set in Y -> Open set in X
  continuousg  : Open set in Z -> Open set in Y
  continuousgf : Open set in Z -> Open set in X
  continuousgf = continuousf . continuousg

The idea is that the fact that f is continuous means that we can produce open sets in X given open sets in Y. Now, consider the fundamental theorem of algebra over complex numbers. This says that any polynomial with complex coefficients with degree greater than 0 has at least one complex root. We'd like to have a function

  fta : Polynomial P of degree >0 over C -> (Point x in C, proof that P(x)=0)

which would compute this root. But the thing is, the standard proof (e.g., by Louiville's Theorem) of the FTA is not constructive. The proof is by contradiction: Suppose there were no root. Then we violate some principle of complex analysis that we know is true (Louiville's Thm, or Maximum Modulus Principle, for example). Thus there must be a root.

But this doesn't tell us at all how to compute the root! So instead we need a constructive proof of the FTA in order to produce a root.

So, the idea is that you can't "play" with non-constructive mathematics in programming as you can with constructive mathematics. Our standard FTA proof would look like

  fta : Polynomial P of degree >0 over C -> Exists x. P(x)=0.

But the type of the object that this function produces isn't very fun to play with. We have no idea what the root is!

I think this is unfair: you're comparing a trivial observation to a nontrivial theorem, and complaining why the complicated thing isn't as easy to play with as the trivial thing.

The Curry-Howard isomorphism really doesn't add anything to the conversation that wasn't already there. Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

Besides, we already know that there is no general way to compute roots of arbitrary polynomials using elementary arithmetic. What you really want is a procedure to find a description of such an x (to arbitrary accuracy, disregarding efficiency), and these are a dime a dozen.

> Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

It is often more easy to prove that some object exists (by contradiction) than to construct such an object.

For example: by applying Zorn's lemma it is easy to prove that any vector space has a Hamel basis. But it is often non-trivial to construct such a basis.

Reply on news.ycombinator.com