Talk:Proof: Difference between revisions
Content added Content deleted
(→J version: re) |
|||
| Line 112: | Line 112: | ||
:::::::::: 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) |
:::::::::: 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) |
::::::::::: 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) |
||
:::::::::::: Not even wrong. Where does the J solution "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers.", as requested by the task description? —''[[User:Ruud Koot|Ruud]]'' 17:48, 10 May 2012 (UTC) |
|||