Talk:Proof: Difference between revisions
→J version
(→J version: re) |
|||
Line 111:
::::::::: 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)
::::::::::: I think you are missing the point here. For the purpose of distinguishing even and odd numbers, "single digit numbers" combined with "sum" have all the necessary properties to represent natural numbers. There is nothing in this task which can distinguish this set from any larger set of natural numbers. --[[User:Rdm|Rdm]] 17:42, 10 May 2012 (UTC)
| |||