Anonymous user
Talk:Proof: Difference between revisions
→J version: re
(→J version: re) |
|||
Line 109:
::::::::# Give the proof of the theorem in such a way that it can be mechanically verified - in a finite amount of time - to be a valid proof by the compiler (e.g. encoded as a program that has the required type encoding the theorem.)
:::::::: The Agda, Coq and Twelf solutions do precisely this. The Omega solution does as well, if one is convinced this solution restricts itself to a sound subset of language. I don't quite follow the J sample but it seems to add a small number of even number and verifies that they are in fact even (one counterexample is enough to disprove a theorem, any finite number of examples are not enough to demonstrate a property holds for all natural numbers.) It doesn't seem to "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers." as requested by the task. —''[[User:Ruud Koot|Ruud]]'' 16:44, 10 May 2012 (UTC)
::::::::: For example, given this "entirety" of natural numbers, count the number of primes between 10^x and 10^y where x = 10^1000000000000000 and y= 10^x --[[User:Rdm|Rdm]] 17:03, 10 May 2012 (UTC)
:::::::::: Given sufficient time and memory this would be possible, yes. However this "rhetorical question" only indicates you're still missing the point here. Counting prime number is a very different task from proving that even + even = even. For the latter you don't have to check that this is the case for each natural number. You can simply proceed by induction and this is exactly what the Agda, Coq, Omega and Twelf solutions do. The compiler only has to verify the base case (zero) and the inductive case (successor). The whole process only takes a few bytes of memory and a few microseconds of time. You J "solution" would take an infinite amount of time. —''[[User:Ruud Koot|Ruud]]'' 17:30, 10 May 2012 (UTC)
| |||