Hacker News Reader

Comment by jwtadvice | Hacker News Reader

Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-terminating programs?

I can see Cantor Diagonalization as a non-terminating program really easily, but I don't understand what the Probabilistic Method looks like as a program.

View on HN

Cantor's diagonalisation is certainly constructive. Given a a sequence of sequences of binary digits, it gives a way of constructing a sequence not occurring in the sequence of sequences. The resulting sequence is as computable as the input.

But to answer your question: Many mathematicians regard their (classical) proofs as algorithms. They just allow themselves to use an oracle call for any well-formed question:

Say I want to prove B. Then, at some point in my proof, I formulate a sentence A, and make a call to the oracle. My proof/algorithm then branches: in one branch I assume A is true, in the other I assume A is false. If I can continue such each branch gives B true, then my proof works (classically). [0]

The constructive critique is that such an algorithm cannot be executed my humans, or turing machines for that matter.

Also there is a whole continuum of stronger and stronger oracles below this ultimate oracle allowed by classical logic — which is an interesting continuum to study. Often one can locate an exact class of oracles needed for a given classical proof to work out.

[0]: This is the «church encoding» version of the law of excluded middle: For all B, we have (A → B) → (¬A → B) → B, which is equivalent to the usual formulation (A ∨ ¬A).

Gotcha. So basically the "axiom" of the law of excluded middle would become an oracle, and then with a call to that oracle a problem requiring the law of excluded middle becomes a proof. Basically - the axiomatic decisions made by mathematicians can be represented as programs by turning them into oracles.

In this case, with the axiom of choice implemented as an oracle, the program for Cantor's Diagonalization can be written.

This makes a kind of ultimate sense. Rice's Theorem shows how a program with an oracle about the behavior of a Turing Machine is contradictory, and this implies that "even with a finite set of axioms" there are no proofs about general classes of Turing Machines and thus there are statements independent of mathematics (a kind of Godelian statement).

Is that right?

If so, that's profoundly simple and also incredible to me. (Hopefully I haven't excited myself into thinking I "got it".)

Could you help me understand what Erdo's Probablistic Method looks like as a program? Which oracles might be required and how you would call them?

I was thinking about LEM today. Without the oracle, you can prove that the double negation of the law of the excluded middle is true, which can be represented with the following type:

    negneg_lem :: ((Either a (a -> r)) -> r) -> r

I'm using a polymorphic r to represent the void type, and I'm using the idea that "not a" is the same as "a -> r".

The proof of negneg_lem is just

    negneg_lem f = (f . Right)(f . Left)

No oracle there. If you had an oracle

    oracle :: ((a -> r) -> r) -> a

then you would get the normal LEM as

    lem = oracle negneg_lem

An interesting thing about the type (a -> r) -> r, i.e., double negation, is that it is the type for continuation-passing style. This suggests that a classical proof is something which is allowed to do backtracking search, but I'm still trying to understand exactly how that is.

(Also, the oracle is somewhat absurd. Really, if you have a function which takes functions, you can produce an element of the function's domain? It might almost make more sense if r was a void type.)

Yes, classical propositional logic can be given a constructive interpretation using call-with-current-continuation. This was first worked out by Timothy Griffin [1], and there is a cute story by Philip Wadler about making a deal with the devil [2, section 4].

[1] http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf [2] http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf

As black_knight said, you don't need the axiom of choice for Cantor's diagonalization proof---that particular proof is completely constructive and can be written as an ordinary non-oracular program.

Huh looks like I need to do a lot more reading to understand all of this! :)

I'm still trying to understand what the Probablistic Method looks like as a program. Any thoughts on that?

I think it is hard to talk about cantor diagonalization as constructive or non-constructive because it is reasoning about uncountable sets.

A more down to earth example of a non-constructive proof would be proofs using non-constructive elements of classical logic like excluded middle (P V ~P), double negation elimination (~~P -> P) or Peirce's law (((P->Q)->P)->P). For example, this proof[1].

There are some similarities between non-constructive logic and non-purely-functional programming. It it possible to see language features such as mutable assignment, exceptions and call-with-current-continuation as analogous to the non-constructive parts of classical logic. These features all make the language depend on the order of evaluation, which destroys makes the program non-constructive[2]

Anyway, I had a really good reference for this but I can't find it right now :( Hopefully someone else can provide a better link explaining how call/cc is equivalent to peirce's law.

[1] http://math.stackexchange.com/a/1118851 [2] http://stackoverflow.com/questions/24711643

I've always seen some close parallels between Peirce's approach to logic and Dijkstra's approach to program construction. Both start with an "empty" object and then transform it according to simple rules until the finished product satisfies some chosen set of predicates.

But most everyone here knows Dijkstra, so I'm mostly just replying to thank you for bringing up Peirce. He's wildly under acknowledged and more importantly under-appreciated. Truly an American genius.

Nit: I'm not sure I would consider Cantor Diagonalization non-constructive. I wouldn't consider it constructive either, though. It's used to prove things like the uncountability of the reals: how do you constructively prove that no bijection exists between the naturals and the reals?

Sure, you can add an oracle for axiom of choice and you're done (note that AoC -> Excluded Middle). A proof is then "constructive" in the same way (e.g. Can be also written as a program, there).

Reply on news.ycombinator.com