Talk:Proof: Difference between revisions

Line 209:

::::: Typically a type, in computer programming, symbolizes a set of values which may validly be represented in the computer program. If the set is infinite, however, the validity requirement vanishes. --[[User:Rdm|Rdm]] 22:27, 13 May 2012 (UTC)

:::::: Not even wrong... I don't think it will be fruitful to continue this discussion. —''[[User:Ruud Koot|Ruud]]'' 22:41, 13 May 2012 (UTC)

::: > However, in a computer program, an infinity cannot be implemented

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

::: Yes, linked lists is a countably infinite data type, this means that there is a countably many linked lists that can be (potentially) constructed. In contrast, the boolean data type has the cardinality = 2.

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

::: > natural numbers are not countable

::: Finite sets is countable too (well, depending on the terminology, see the wikipedia entry on the countable sets).

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

::: By "you" you mean anybody who "believe" in Agda/Coq/Epigram/Twelf/ATS/NuPRL/ALF/DML/LEGO/HOL/Isabele/ACL2/Mizar/MetaMath/etc. proofs? Did you believe in 4-color theorem proof? Did you reject implementations of the homotopy type theory in Coq/Agda?

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