Talk:Proof: Difference between revisions
→Quantifiers
(yes: notation used in proof must be understood by the reader) |
|||
Line 231:
::::: Just as you can prove `even + even = even` (for ''all'' natural numbers) by using a finite amount of paper and in finite number of steps, computer (proof system) can do this using a finite amount of memory in a finite time.
::::: > the number of distinct linked lists which can be represented
::::: No, usually sizeof(struct DList) for some DList type is not equal to the machine word size. Also, what if the machine has [[wp:Physical_Address_Extension|PAE]], what about other real world restrictions? Of course, it's absolutely not important, you commenting a minor point. The real question is why you think that statements about natural numbers like `even + even = even` can't be proven with computer using proof systems and keep talking about unrelated discrete math stuff. This task is for peoples who believe in finitism and [[wp:Mathematical_proof|mathematical proofs]] (the correspondence between programs and proofs is [[wp:Curry%E2%80%93Howard_correspondence|well known]]). — [[User:Ht|Ht]] 07:33, 14 May 2012 (UTC)
:::::: (I fixed my phrasing there.) 1. You are talking about smaller limits, here, and 2. you are introducing new terminology (e.g. "DList") without bothering to define it, and making less general statements. In other words, these are meaningless objections -- the point is that there is a limit. This means, in the context of this task, that there will be even numbers which cannot be added associatively because they cannot be added. This leaves us with two options: either (a) the type system is incomplete and does not represent this failure mode, (b) the type system does represent this failure mode. Traditionally, static type systems use (a) and run-time typing is needed for (b). My problem, here, is that this task currently seems to be asking for a type system with neither of these failure modes. Of course we know that any actual implementation will have one of them, but -- because of earlier objections here -- I am afraid that if I present an implementation that has either of these failure modes that people will object to it. So I am asking that this task requirement be made explicit. --[[User:Rdm|Rdm]] 10:08, 14 May 2012 (UTC)
::: See also this link: http://okmij.org/ftp/Computation/uncountable-sets.html.
| |||