Talk:Proof: Difference between revisions

::: Infinity cannot be implemented in math either, we can only say "infinity" which is the finite statement. Every [constructive] mathematical proof is always finite and just represents a way of manipulation of finite symbolic information (the mathematical terms) that can be done in finite time (one can take a piece of paper and try for the even + even = even prop.). There is nothing surprising in the fact that symbolic information can be represented as types and terms in programming languages ​​(in almost any starting with C, because everywhere there are data types and their constructors), and the proof itself can be represented as a terminating algorithm of unification (e.g., type checking, but not everywhere, only in languages ​​with enough expressive type system).

 

 

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

::::: > the number of linked lists which can be represented is the factorial of 2^N where N is the number of bits of memory

 

 

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

::: > My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types

 

 

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

 

 

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