Anonymous user
Talk:Proof: Difference between revisions
→Quantifiers: re
(→Quantifiers: re) |
|||
Line 194:
:: My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types. --[[User:Rdm|Rdm]] 21:05, 13 May 2012 (UTC)
::: Your persistent assumption that computers incapable of working with "infinities" is wrong. When a mathematician wants to prove a theorem about the natural numbers he will not proceed be trying out the theorem for each natural number until the heat death of the universe.Instead, he will give a finite proof. A computer is equally capable of this.
::: Inductively defined types (e.g. a linked list) have an infinite set of values. (An implementation will generally be limited by the word size of the underlying machine, but a proof should be independent of this and work for an arbitrary word size.)
::: Might I suggest you read a good book about the foundations of mathematics? Perhaps my terminology will seem less ambiguous to you after this. —''[[User:Ruud Koot|Ruud]]'' 21:33, 13 May 2012 (UTC)
| |||