= 27d567bc2d48d9f40e9ccc20ea370b15)
whpearson comments on AI cooperation in practice - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (157)
The most obvious implementation for the easy version will return 0 (or, if the length limit is lifted, fail to return at all).
It's important, however, to be clear on just what constitutes a valid proof. Consider the following implementation:
Not valid because it didn't find a proof, you say? On the contrary, assuming we are dealing with idealized mathematical computers that are perfectly deterministic and have no outside inputs, the fact that a program returns a given value on this run does indeed constitute a proof that it will do so on every run.
The point being that, while you can use concepts like proof to draw rigorous conclusions, in the face of counterintuitive things like self reference, you need some experience actually nailing things down before you can be sure you've closed all the loopholes.
The Curry-Howard correspondence is what you are referring to right?
That program does not prove its return value under the Curry-Howard Correspondence without a lot of footwork (see first caveat). Under the CH interpretation, programs are proofs that their types are inhabited, not that they can produce their return values. Thus, the canonical thing one could say the above program proves is "int".
Some caveats. First, one could imagine a sufficiently complex type system where there is a type of all integers which are 1. Then, one could say that the above program is a proof of the type "type-of-ints-that-are-1". However, when adding this much specificity to one's type system, one has to be careful that the resulting system can decidably type terms; adding richness often leads to undecidability.
Second, there is simple constructive proof that the the above program produces 1. Just run it and see; if it returns 1 in finite time, that's a proof.
That is certainly one way to look at it.
Another way to look at it is to consider purely computational proofs, such as the four color theorem, or the solutions to checkers and 5 x 5 Go.