Talk:Proof: Difference between revisions

Line 219:

:::: This is trivially false, since every computer has a finite amount of memory -- even if it's virtual memory -- and linked lists must fit in memory or the links are invalid. At most, the number of linked lists which can be represented is the factorial of 2^N where N is the number of bits of memory (N is wordsize * 2^64 in a computer with 64 bit addressing). Now, I will agree that that is a large number, which might distract you from noticing that it's a finite number, but it's still finite. And even if you changed from a parallel bit implementation to a serial bit implementation and addresses were represented by a sequence of 1 bits (the first 0 terminating them), which would let you have arbitrarily long addresses, you still run into issues like the lifetime of the universe (or, more practically, the funding which keeps your computer system running). It's still not infinite, except in your imagination. --[[User:Rdm|Rdm]] 01:44, 14 May 2012 (UTC)

::::: > This is trivially false, since every computer has a finite amount of memory

::::: Real computers are not even Turing complete, that is why the word "potentially" was used. But this is not a problem because of [[wp:Finitism|finitism]].

::::: 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 linked lists which can be represented is the factorial of 2^N where N is the number of bits of memory

::::: 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]]).

::: See also this link: http://okmij.org/ftp/Computation/uncountable-sets.html.

Line 231:

Line 241:

:::: If your description here is correct, then these implementations of homotopy type theory have weaknesses in their treatment of upper bounds. No big deal, perhaps, except that you seem rather intolerant of other implementations with the same kind of limitation. --[[User:Rdm|Rdm]] 01:53, 14 May 2012 (UTC)

::::: [http://ncatlab.org/nlab/show/homotopy+type+theory Homotopy type theory] originally appeared as the discovery of connection between homotopy theory and Martin-Löf type theory, and one of the interesting points consisted in the fact that an implementation of type theory (e.g. Agda or Coq) can be used as the language for homotopy theory. Needless to say that most of the proofs in HoTT are held for potentially infinite structures and higher-order types.

::::: "Upper bounds" makes sense for brute-forcing "proofs" but the real proof system uses unification... Well, it's still required to get the point. Talking about the "upper bounds" is not even funny :)

::: My current inclination is to believe that you cannot get [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf the point] of dependently-typed programming languages / proof systems. — [[User:Ht|Ht]] 23:00, 13 May 2012 (UTC)