Hacker News Reader

Comment by tprice7 | Hacker News Reader

"As the new shorter proof is the compressed representation + the decompression program." A proof is a sequence of deductions, not a program that generates a sequence of deductions.

View on HN

You might be interested in reading about the Curry Howard Correspondence. From wikipedia: "In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects." https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Yes, I've encountered one form of the Curry-Howard correspondence before. Are you claiming that, via the Curry-Howard correspondence or some related phenomenon, the corresponding proof of a program used to compress a proof is the same (or at least, proves the same theorem) as the original proof that the program was meant to compress? That is interesting and I would appreciate if you could expand on it.

If you’re using the right language, proofs are programs; it’s as simple as that. “Compressing” a proof, then, amounts to doing what good programmers are already doing — noticing patterns and eliminating redundancy.

I’ll refer you to an authority on the subject, Phil Wadler. If you like watching videos, try <https://www.youtube.com/watch?v=IOiZatlZtGU>. If you’d rather read an entertaining paper, try <http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-....

The Curry-Howard correspondence does not apply here though. The coloring theorem is not encoded in the type of the program that enumerates and checks the possible colorings. The program itself is a restatement of the coloring theorem, with the result type being boolean (all the enumerated colorings satisfy the property, or not). So the proof would consist of proving that the program must terminate with a true value. Of course that is not actually useful as it does not simplify anything.

This is a simple mechanization of the proof steps, on par with using a calculator for arithmetic.

Depending on what programming language you use for your Curry-Howard correspondence, there is actually a related thing. Probably the most well known realization of C-H is dependent type theories like Coq and Agda. And those support a proof method called "proof by reflection".

The idea is that in those languages, types can contain program terms as subexpressions, and two types are considered "the same" if they evaluate to the same expression. Because the languages enforce that all expressions terminate, it's still decidable whether a program is well-typed or not, so the language can still be considered a proof system, but the type checker can take almost arbitrarily long time to check a program because it has to evaluate subexpressions to values in order to check type equality.

Anyway, the point is that this can be used to write down short programs that act as proofs. For example, suppose you want to prove there are no counterexamples to Fermat's last theorem for exponent 5 and numbers less than 100000000. In this case, you would write down a function

    f : nat -> bool

which evaluates the expression for all numbers less than the argument and returns whether there is a counterexample, then you would prove a lemmma

   soundness : forall n, (f n = false) 
              -> forall x y z, 
                   (x < n) -> (y < n) -> (z < n) 
                   -> (x^5 + y^5 ≠ z^5)

and then the proof of the final theorem is just

   soundness 100000000 eq_refl

In order to check the eq_refl part, the type checker would evaluate (f 100000000) and verify that it evaluated to false. But all that computation is not recorded in the proof term. So the program that represents the proof is very small, and constant size in the bound.

This is actually very useful in practice, because storing and manipulating big proof terms is slow and memory-hungry, so it's useful to be able to push the computation under the carpet in this way. On the other hand, it is sometimes considered a little philosophically dubious.

That doesn't make proofs any shorter or any more elegant, though. The same "noticing patterns" can be done on the proof in non-FP form. C-H is basically an observation about encoding.

Reply on news.ycombinator.com