Talk:Proof

The subtype Natural is pre-defined for all Ada implementations. Arithmetic upon that subtype is also pre-defined. This does not appear to be a very interesting problem in Ada. Any suggestions? --Waldorf 14:42, 21 December 2007 (MST)

This seems like less of a computing problem, and more of a discrete math problem. I'm not sure if it's a good task. --Mwn3d 14:45, 21 December 2007 (MST)

The task was intended to demonstrate dependent types. I've got some C++ code I'm working that demonstrates how it can be accomplished there. --Short Circuit 20:50, 21 December 2007 (MST)

Proof vs. Formal Verification

After reading Social Processes and Proofs of Theorems and Programs, I decided to provide a "mathematical proof" as opposed to an "essentially meaningless" (possible to understand only for trivial concepts) formal verification. If anyone feels they should mark that solution incorrect, please first be prepared to rationally discuss the issues raised in the pdf which I have linked to here. --Rdm 03:08, 27 August 2011 (UTC)

Huh?

The data type for "natural numbers" is what would be called an "unsigned integer" in other languages, right? Or did you want us to create a data type that can deal with arbitrary-size integers?

If we're merely talking about unsigned ints, then the data type for "even numbers" is of course the exact same thing (since the two sets are isomorphic). So the programming task boils down to writing functions for I/O that take an unsigned int and interpret it as "one half of the number we're talking about". Is that what is intended here? If not, then what exactly are we supposed to do here? You see me somewhat puzzled... Sgeier 17:45, 11 March 2008 (MDT)

If you ignore the numbers given, the proposal still makes sense. I think the task was intended as an exercise of type dependency with proof systems. This possibility is supported by the project pages for Coq, Agda2 and Twelf. (How is it that all the links on this page are uncreated, I wonder...) It doesn't look like an imperative problem. It could be done in C++ with classes and operator overloading, for example. The proof is whether or not the proper code compiles. It looks like I'd intended to do that, but I recall life getting in the way that week. --Short Circuit 19:40, 11 March 2008 (MDT)

Proofs

Does this task apply to languages which are not built as theorem-proving systems? If so, what constitutes an acceptable implementation of "prove that the addition of any two even numbers is even"? --Kevin Reid 00:07, 17 February 2009 (UTC)

I'm thinking about implementing theorem proving system as an application in the language. This could be done with at least any Turing-equivalent language. Still unsure how that would be for this particular task.Avmich 00:03, 12 November 2009 (UTC)

I did this in Haskell, but I dunno how easy it would be in other languages, especially dynamically-typed ones. —Underscore (Talk) 18:11, 18 February 2010 (UTC)

Clarification needed

The first line of the description reads: "Define a type for a sub-set of natural numbers (0, 1, 2, 3, ...) representable by a computer, and addition on them." Can somebody please clarify that last phrase, "addition on them"? I think I know what it's supposed to mean (and I'm fairly sure I understand the task as a whole) but just in case... -- Eriksiers 22:24, 5 November 2009 (UTC)

In mathematics, when we speak of "a binary operation on S", we mean a function whose domain is S × S and whose codomain is S. So "addition on the natural numbers" means an addition function that takes two naturals and returns a natural. —Underscore 00:42, 6 November 2009 (UTC)

Hmmm... I slept through most of my calculus classes, due to having THE MOST BORING TEACHER IN THE UNIVERSE (really) and as a result, most math above simple algebra I just don't get. I think I'll give this task a pass. -- Eriksiers 15:05, 6 November 2009 (UTC)

But this is not much more than elemental type theory. Hardly as complex as the infinitesimal calculus... –Donal Fellows 16:38, 6 November 2009 (UTC)

I passed Calc 2, and it still took me a couple years and lurking in discussions of C++0x before I really started understanding what was being talked about in this task. Type theory and calculus seem to me to be orthogonal subjects. --Michael Mol 19:19, 6 November 2009 (UTC)

Rightly or wrongly, elementary calculus is in most colleges a prerequisite for courses on basic proof-writing. I'm a math major and I ended up taking vector calculus before "foundations of mathematics". —Underscore 20:34, 6 November 2009 (UTC)

The Go proof?

The Go sample seems questionable. It claims that successful compilation completes the proof, but what if I make some small changes to the code? <lang Go>var zero number = e0.pn // see axiom 5, below. var one = zero.successor() // I added this .... func (s *evenPeano) hasEvenSuccessor() (even, bool) { // if s.normalize() == zero { //original code

     if s.normalize() == one {   //I added this
       return nil, false

</lang>By the way, all the "has*Successor" probably should have been named "hasPredecessor" instead. Anyway, by the proof's logic, what was evenPeano is in fact "oddPeano" now, and it still compiles fine. Does that just prove sum of two odd numbers are also odd numbers? --Ledrug 20:46, 21 June 2011 (UTC)

On "hasSuccessor," yes, sorry, that does look silly. I'll fix it soon. On trying to prove sum of two odd numbers is odd, I think your edits are not quite enough. Your declaration of variable one didn't create a variable of type evenPeano, so it doesn't quite work as an an even number. one.evenSuccessor(), for example, won't compile, and nothing that can be passed to hasEvenSuccessor (sic) will ever compare equal to it. Trying to hack this up more, though, we might try,

var zero number = &peanoNumber{}
var one = zero.successor()
var e0 = &evenPeano{one.(*peanoNumber), nil}

This compiles, and now looks even worse because now one and all its successors counting by twos are of the type evenPeano. What we're left with though, is a bug in in addEven. It terminates with a sum when it gets to the first "even" number, one. To get the correct answer, we still have to add this remainder of one, and this is now what we can't get to compile. Trying a.successor() or a.add(p) returns a regular peanoNumber that won't match the return type of evenPeano. The compile error is saying odd numbers are not closed under addition.

I'll add that while I had fun with this task, I don't consider it much of a proof. There's way too much hand waving for me. —Sonia 23:29, 21 June 2011 (UTC)

I'm sure it was a fun thing to write, but "not much of a proof" is the problem here. I can write any kind of code to prove odd + odd = odd, and I can make it compile, but that proves nothing; only when I run the code, and do a test like "is 1 + 3 odd?" The code will go 1 + 3 = 4-> pred 2 ->pred 0 (BOOM, hopefully, because first element is 1), so that's a counterproof, but, the key is, you have to run your logic in the code to make a proof, merely compiling means nothing. If you aggree to that, now convince me your code can prove even + even = even: I won't likely live long enough to see your program exhastively test all even numbers. See my point? However fun it was with the axioms and writing the code, I just don't think this code counts as fullfilling the task. --Ledrug 23:43, 21 June 2011 (UTC)

The task might be poorly worded and poorly named, but I think the examples posted by the task author and every example except Haskell show the same thing, which is using the language type system enforcement of closure over a type as an analog of mathematical closure over a set of numbers. The code to demonstrate isn't the code that you write, but the code that is in the language translator. —Sonia 01:09, 22 June 2011 (UTC)

I'm not sure what you meant by the last sentence (actually, I'm not sure what you meant by the sentence before that one, either). As to other examples, Coq seems to be doing the right thing; TCL seems to be doing the right thing (or pretending to, I can't tell); Haskell seems to be doing a slight variant of the right thing. Of the other ones, Adaga and Omega do seem to only define a set without verifying it's closed, if so they are incorrect, too, but I don't know enough about them to say for sure. Unfortunately, I do know what the Go code does.

It is capable of verifying (when run) if any given instance of a number is even, doing so by recursion to individual instances of predecessors, not induction based on definition, which is a big difference. Your other argument, that if it passed compiler type checking, it must be consistent, is false: my bogus "oddPeano" passed it with gaping logic holes, and the compiler didn't catch it, because it's not supposed to. True that if I read the code, I may say "that's not going to work, the hasPredecessor() will go past one and reach -1 and below", but a) I'm not the compiler; b) the task requires the program to prove, not "let Ledrug read the code and prove".

Now if the we can change the task description to say "show by examples that such and such", your code is perfectly fine (again, if you run it). As it is, though, it's not enough as a proof.

Lest I look too harsh, I'm not trying to be overly righteous or trying to kill your fun; it just so happens that I think "prove" is not a verb to be used slightly. --Ledrug 02:09, 22 June 2011 (UTC)

The task description reads "Define a type for natural numbers (0, 1, 2, 3, ...) representable by a computer, and addition on them". This does not make any sense. I think this should read "Define a datatype for natural numbers and their associated additions that can be represented on a computer.". It still doesn't make any more sense, but hey the words look better. :) Markhobley 15:33, 13 July 2011 (UTC)

J version

This is not a proof, right? — Ht 13:27, 10 May 2012 (UTC)

According to my discrete math teacher, a "proof" is a "convincing explanation".

In this case: 1 represents "true", and the J implementation is showing that the theorem holds for all cases in a specific example.

That said, to be treated as a proof, some reader involvement is required. If you do not understand the notation that would be difficult. --Rdm 13:36, 10 May 2012 (UTC)

But this page is using the term "proof" in formal sense of constructive mathematics/Curry-Howard correspondence, not your math teacher's definition. I'm not at all familiar with J, but this does not look a proof in the former sense, i.e. it requires the reader to finish the proof by induction, external to the program, while e.g. in Coq of Agda the induction step can be done in the language itself. —Ruud 13:53, 10 May 2012 (UTC)

1) The requirements you are expressing here currently not stated in the task description.

2) The reader still needs to understand and the relevant aspects of Coq (or whatever else) before a proof implemented in Coq can be valid for that user.

3) It's not clear to me that this narrow of a definition of proof is valid in the context of rosettacode. For it to be valid it would have to be shown that your restricted concept of proof does not exclude most programming languages.

--Rdm 14:17, 10 May 2012 (UTC)

1. I think the boldfaced note expresses this, although the task description can indeed be made more clear.
2. You're confusing things here. The Coq program here is a proof (one that can be verified by the compiler to be correct!). Clearly the reader needs to understand some things about Coq to understand exactly what has been proven, but this is no different from most samples in any other task and quite different from what (I believe) the J, Go and Tcl samples are doing: they give a program and the instruct the reader to mentally construct some kind of correctness proof.

   There's no particular reason a proof system couldn't use Tcl directly; it would just require some sort of protected store to hold axioms and proved theorems (this would have to live outside value-space) and commands for querying the store and supplying new axioms and evidence for theorems. Tcl provides the tools to do that natively (via coupled interpreters, with one hosting a proof session and the other the protected store) but actually doing it would require rather more effort than I believe is reasonable to use in a task. (That is, it involves building a theorem proving environment/application.) What is practical is doing the individual steps, the lemmas, in the proof. –Donal Fellows 08:36, 14 May 2012 (UTC)

3. On the contrary, this task explicitly excludes the majority of languages. I don't see a problem with this at all. Because most languages are Turing-complete an algorithmic or computational task can be implemented in nearly any language. However there also exist tasks that concern the abstraction or other languages facilities which simply cannot be reasonably implemented in any language. E.g. one can imagine tasks that only make sense in either dynamically-typed or statically-typed languages, languages having a sufficiently expressive type system or supporting reflection. Adding "fake" solutions only distracts the reader from the thing the task is trying to demonstrate or compare.

—Ruud 14:48, 10 May 2012 (UTC)

All programs are "proofs", in the sense of showing the existence of a mathematical construct. The issue is "what are they proving". (In many cases, what is being proven is not very interesting, in a general mathematical sense.)

As for "explicitly excluding the majority of languages", please see the guidelines.

--Rdm 14:58, 10 May 2012 (UTC)

As most programming languages correspond to an unsound logic the answer to "what are they proving" is usually "nothing". I think it's generally good advice to make a task widely applicable/implementable, but in this particular case it is not. The task's intention is to demonstrate the difference in syntax and semantics of the 15 or so proof assistants currently in existence. This is useful and clearly in line with Rosetta Code's mission. Adding 100 "faked" solutions of languages never intended to be used as a proof assistant is not. Those solutions add no value and distract from the information that is there. Finally, also note that the Agda, Coq and Twelf solutions implement the exact same thing, while the J solution seems very different.—Ruud 15:20, 10 May 2012 (UTC)

I disagree with your opening sentence unless it is further qualified with

"because the user does not understand what is happening".

As for the last sentence, that cannot be a problem in and of itself.

More specifically, when dealing with a concept like "Natural Numbers", a computer cannot represent them in their entirety. Instead, we have to accept some symbol which represents them. And, thus, when we deal with a "proof about Natural Numbers" we are really dealing not with natural numbers but with a surrogate. The surrogate can have only a subset of all properties of natural numbers. A question then, in the context of a proof is: does the mechanical implementation represent all relevant properties of natural numbers in the surrogate? In the context of "even" and "odd" all of the relevant properties are present in single digit decimal numbers and their sums (and by this, I mean that you are not going to be able to demonstrate any relevant exceptions, without going outside the bounds of this task).

Thus, your point seems to be that you want the task to be expressed in a system which expresses the relevant rules using a particular system of symbols, and you want the task to demonstrate that the language uses the "proper sorts of manipulation" of those symbols. But that has problems: (a) the task does not really define what is "proper", and (b) as near as I can tell, a person would have to study the language implementation to determine whether treatment of [for example] induction with excluded middle is handled adequately. --Rdm

A computer certainly can represent the natural numbers in their entirety! For example in Agda:

data N : Set where
 o : N
 1+ : N ? N

The number of inhabitants of this type is infinite, but its representation is finite. This type has exactly the same properties as the natural numbers, because it precisely encodes the Peano axioms.

There certainly are different approaches to "solving" this task (e.g. a solution in HOL or Isabelle would look rather different than one in Agda, Coq or Twelf) but there are some reasonable things a solutions/language would have to do/support:

1. State the required theorem (e.g. encoded as a type in the language's type system.)
2. Give the proof of the theorem in such a way that it can be mechanically verified - in a finite amount of time - to be a valid proof by the compiler (e.g. encoded as a program that has the required type encoding the theorem.)

The Agda, Coq and Twelf solutions do precisely this. The Omega solution does as well, if one is convinced this solution restricts itself to a sound subset of language. I don't quite follow the J sample but it seems to add a small number of even number and verifies that they are in fact even (one counterexample is enough to disprove a theorem, any finite number of examples are not enough to demonstrate a property holds for all natural numbers.) It doesn't seem to "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers." as requested by the task. —Ruud 16:44, 10 May 2012 (UTC)

For example, given this "entirety" of natural numbers, count the number of primes between 10^x and 10^y where x = 10^1000000000000000 and y= 10^x --Rdm 17:03, 10 May 2012 (UTC)

Given sufficient time and memory this would be possible, yes. However this "rhetorical question" only indicates you're still missing the point here. Counting prime number is a very different task from proving that even + even = even. For the latter you don't have to check that this is the case for each natural number. You can simply proceed by induction and this is exactly what the Agda, Coq, Omega and Twelf solutions do. The compiler only has to verify the base case (zero) and the inductive case (successor). The whole process only takes a few bytes of memory and a few microseconds of time. You J "solution" would take an infinite amount of time. —Ruud 17:30, 10 May 2012 (UTC)

I think you are missing the point here. For the purpose of distinguishing even and odd numbers, "single digit numbers" combined with "sum" have all the necessary properties to represent natural numbers. There is nothing in this task which can distinguish this set from any larger set of natural numbers. --Rdm 17:42, 10 May 2012 (UTC)

Not even wrong. Where does the J solution "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers.", as requested by the task description? —Ruud 17:48, 10 May 2012 (UTC)

A type, in J, is the set of values which can result from a parenthesizable expression. In this case, it's a restriction on the argument to isEven -- corresponding to the case where the result of isEven is true. --Rdm 19:58, 10 May 2012 (UTC)

Great. It's still not a proof, though. What's next? You're going to claim you've proved the Collatz conjecture because you have checked the first 9 cases using a J program? Now, if you managed to pull that feat using Coq there's probably both a Turing Award and a Fields Medal waiting for you. —Ruud 20:38, 10 May 2012 (UTC)

No. I made no claims about the Collatz conjecture. --Rdm 20:44, 10 May 2012 (UTC)

No you didn't, but your method is equally applicable. I used it to prove Goldbach's conjecture:<lang text> even + even = even even = prime + prime

---

1. Print sum of a bunch of even numbers, Print even numbers from 4 to a billion,

  show that they are all even;                   show that they are each sum of two primes;

2. Argue that step 1 is "convincing", induction schminduction;

3. (backup plan) Dare any disagreeing reader to find a counter example;

4. Profit! I mean, proof!</lang>

I don't think that Rdm believes in such proof of GC, he just does't believe in presented proofs for the task. — Ht 07:55, 14 May 2012 (UTC)

That's not to far from one of my issues here, which is that a proof is only valid for a person if the person understands its notation. This, seemed to be the basis for the objections to my earlier implementation, before the task was changed. (A second set of issues has to do with the changes introduced a couple days ago.) --Rdm 09:58, 14 May 2012 (UTC)

It's easy to show that my approach here does not handle the Collatz conjecture. Consider the values 1 and 3. Their Collatz sequences have different lengths. Nothing in my approach deals with these sequence lengths.

It's also easy to show that my approach here does not handle the Goldbach conjecture: Nothing in my approach deals with primes.

--Rdm 19:28, 13 May 2012 (UTC)

Your arguments thoughout this discussion varied, but none of them justfies the J example as a proof:

1. "The task didn't say what kind of proof it wants": it doesn't matter. What J offers is anecdotal evidence, not a proof. You can't quote a nameless math teacher to subvert the well-agreed meaning of a word, not when the context is programming/math/logic.

2. "Authors of the pdf I linked says machine proof/program verification sucks": it's true. I mean, they did say that. So?

3. "Coq/Adga/whatever's output still requires the reader to understand it": true. It also requires the reader to know what mathematical induction is. But if you can read it, you'll see that it's done the way how a human would have proved it, with the critical "for any number n, it can be reduced to..." thingy, which no amount of integer printout can replace.

4. "Rosettacode tasks should allow every language to participate": I don't believe so. It's good to have a task that's applicable to most languages, but tasks tailored towards a handful specific languages are worthwhile, too. Case in point: it's good to show readers how a proof assistant works; barging in with something completely irrelevant like the J example is very unhelpful.

All in all, it's pretty clear what the task wanted, and that the J example didn't deliver. When a task is asking for something your language is not designed for or is incapable of doing, the decent thing to do is: nothing. Just omit the task. --Ledrug 22:07, 11 May 2012 (UTC)

This is not a language issue, unless you consider J to be C (because, after all, J is implemented in C). This is a task specification issue. --Rdm 19:24, 13 May 2012 (UTC)

Draft status

I suggest the task should be draft status. The varied solutions posted and the resulting discussions here show disagreement on what the current wording requires. —Sonia 20:33, 11 May 2012 (UTC)

I think the task is quite clear: "prove that the addition of any two even numbers is even". Any. It is not possible with bruteforcing, since there is a countable many even numbers. Nevertheless, a constructive proof can be given in a suitable logical system (such as ACL2) or in a language with dependent types (Agda, Coq, Twelf to name a few).

Putting something that looks like "2" in the CPU register, the same "2" in another, performing ADD, and getting something that looks like "4" doesn't help - that is not a proof! :) You need to define numbers, rules for arithmetic, induction, etc in the language based on a suitable metatheory such as MLTT or CoC/CoIC, then prove. E.g., in the Agda version even+even=even takes any two even numbers and returns their sum as an even number, this is a type, i.e. logical proposition, algorithm itself is a proof by induction which builds a required term of a given (inhabited) type, and the typechecker performs that proof (so that this is compile-time verification). — Ht 02:44, 12 May 2012 (UTC)

It seems a wothwhile task in the way you describe it here on the talk page. Maybe the task description needs similar expansion to remove J-like entries and require "induction solving capabilities" or people to create such in a language without it, then apply it to the problem at hand. --Paddy3118 07:22, 12 May 2012 (UTC)

The recent rewrite of the task description makes my point. Much of the wording, and the new requirement about showing associativity are one day old. —Sonia 17:17, 12 May 2012 (UTC)

Apart from the small additional subtask, I don't think this task has been changed in any essential way since 2007. —Ruud 18:09, 12 May 2012 (UTC)

Wrong. It's full of additional restrictions. In 2011 even, it said nothing about dependent types. These new restrictions are approaching a task description that says something like "languages must have built-in support for at least one of (loosely related) features x, y or z. all others must omit." But the task isn't clear yet on what those features are. —Sonia 18:39, 12 May 2012 (UTC)

I think it was as clear in 2007 what this task was supposed to be about as it is now to someone who has had some previous exposure to proof assistants. The only problem here is effectively communicating this to programmers who do not have such a background. The letter of task description might have changed a bit, but its spirit certainly hasn't.

One of the problem with stating the description precisely is exactly because it should not exclude solutions in HOL or Isabelle (they are not based on dependent types) or perhaps even a very creative solution using C++ template programming. —Ruud 18:49, 12 May 2012 (UTC)

Haskell

Looks like GHC can typecheck the same expression as in the Omega/Agda version. ?an not guarantee the totality, however. — Ht 02:52, 12 May 2012 (UTC)

Does it satisfy the task? Hard to say due to existing inconsistencies in the task description. The description starts out saying it only makes sense for dependently typed languages and proof assistants. It later wants to allow Haskell for implementing System-F. Is type checking enough, and if so, must it be run time or can it be compile time? My understanding is that dependent typing, by definition, is done at run time and that Haskell does the type checking at compile time. Does a clean compile constitute a proof? —Sonia 18:18, 12 May 2012 (UTC)

"Yes, but..." The solution requires two languages extensions (GADTs and type families) that together allow one to express some dependent types. They are not as expressive as full dependent types, but are powerful enough to express this rather simple theorem and its proof.

Your understanding of dependent types is wrong: the typing is not done at run time, but rather code is executed at compile time. Haskell cannot execute arbitrary code at compile-time, but type checking type families and GADTs effectively does require some execution at run-time.

The "but" is that fact that Haskell allows general recursion, making the logic unsound, i.e. any theorem - including false ones - can be proven by an expression that would diverge at run-time. The given solution does not use this "feature", however.

This is a solution that the task should clearly allow, with the appropriate footnotes, though. —Ruud 18:35, 12 May 2012 (UTC)

Quantifiers

The currently phrasing of this task places emphasis on "any" (pair of even natural numbers) and on "every" (use of addition between those numbers).

But the task also requires that the language implement the natural numbers so represented.

This is either a contradiction (since every language can only implement a finite set of distinct numbers and there are an infinite number of "Natural Numbers") or a new use of the term "Natural Number" which I am not familiar with (in which case the required definition should be included in the task description).

--Rdm 19:44, 13 May 2012 (UTC)

Put differently: the task asks for a countable set of natural numbers. This would be trivial, except that the peano postulates do not hold for a countable set. --Rdm 20:19, 13 May 2012 (UTC)

The set of natural numbers is countably infinite. They are defined by a finite formal systems (the Peano axioms). A proof about a property holding for all natural numbers can be given in a finite form (using induction). You may indeed not be familiar with these facts, but they are most certainly not novel. —Ruud 20:41, 13 May 2012 (UTC)

Ok, that's ambiguous terminology. I agree that "countable" in the mathematical sense means aleph null style infinity -- "has a one-to-one correspondence with natural numbers".

However, in a computer program, an infinity of values cannot be implemented -- it can be symbolized, but that is different from implementing it. A computer program can only implement a finite set of distinct values. Thus, in the context of a type -- when using the normal meanings of "countable" and "type" -- natural numbers are not countable.

That said, if you really mean for a program to implement a "countably infinite" type, that is itself a failure in specification. At the very least, you should be obligated to say what you mean by "type" when the usual meaning of type in programming refers to something which can only enumerate a finite set of values without failure.

My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types. --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. —Ruud 21:33, 13 May 2012 (UTC)

You have overgeneralized my statement. Overgeneralizations are, generally speaking: wrong.

The issue I raised was not "computers are incapable of working with 'infinities'". The issue I raised was "computers can only represent finitely many distinct values. By leaving out that "distinct" part, you ignored my entire point.

It seems, though, that you are saying that you accept as valid a type system where an infinity of the symbolized values are not implemented by the implementation -- where only finitely many values symbolized by the type are implemented. --Rdm 21:42, 13 May 2012 (UTC)

Then read my above sentence as "... have an infinite set of distinct values". The "distinct" was already there implicitly (all elements in a set are always distinct), so the statement remains equally true.

I'm not exactly sure what you mean with "accept as valid a type system where an infinity of the symbolized values are not implemented by the implementation", so I can't say if I agree with that or not. As a proof by induction of even + even = even does not rely on actually computing any particularly large objects, it is quite irrelevant if the implementation has any limitations of what the maximum size of the finite representation of these infinite models can be. —Ruud 22:12, 13 May 2012 (UTC)

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. --Rdm 22:27, 13 May 2012 (UTC)

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

Typically "not even wrong" indicates a lack of testability. It's not clear how that is relevant here. I am guessing, though, that you disagree with me about the meaning of the word type. But if that were the case I think you should present your own definition.

My suspicion though, is that in this case "not even wrong" means the same thing as "right". --Rdm 00:21, 14 May 2012 (UTC)

Most of your comments here consist semantically empty rambling. I therefore cannot possibly give a genuine reply to them, they are so incoherent I cannot even state what is wrong them, ergo "not even wrong". —Ruud 13:00, 14 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. — Ht 07:33, 14 May 2012 (UTC)

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 2^N where N is the number of bits of memory including virtual memory (N might be limited by the OS to a value smaller than 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. --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 constructivism/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 distinct linked lists which can be represented has a limit which cannot exceed the factorial of 2^N where N is the number of bits of available memory

No, usually sizeof(struct DList) for some DList type is not equal to the machine word size. Also, what if the machine has 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 mathematical proofs (the correspondence between programs and proofs is well known). — 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). One common failure mode (e.g. two's complement, fixed width) violates the peano axioms for approximately half of the representable combinations of values. Another common failure mode (inductive representation or variable width) also poses an additional constraint where time needed to complete the operation increases as the values increase in size. This second failure mode can be made so burdensome that it disguises the first failure mode, but that's not always a good thing. My problem, here, is that this task currently seems to be asking for a type system with no failure modes. Of course we know that any actual implementation of the peano axioms must eventually fail to implement some cases, 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. --Rdm 10:08, 14 May 2012 (UTC)

"the point is that there is a limit" - of course (this was my minor comment on minor comment for the minor point), but a type always has it cardinality (i.e. the cardinality of the corresponding set, for example, aleph-null for natural numbers or finite strings), this is unbeatable, it does not matter how many terms can be constructed physically. "This means, in the context of this task" - this means nothing in the context of this task. Again: 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. Using the same axioms and deriving rules! In the Agda version there is no numbers which are directly tested for the statements of the task (well, only the first natural number is verified directly), the computation is done in a general form over terms and types. Imagine the following, you have the formulas, you have a finite set of axioms and inference rules, there is a way to apply these rules to formulas to obtain new formulas, starting with the axioms. So using only terms of finite size, and applying a finite number of rules you can deduce the truth of the `even + even = even` statements in a suitable metatheory. Proof systems do just that, they do not directly test the statements for some finite set of test data. The proof itself is a compile-time type checking (in the case of languages with dependent types). Not all the math, but some formal mathematical systems is definitely systems that can be implemented: their symbolic data (the "math" itself) can be implemented, the reasoning in such systems can be implemented and so on. We can trust in proofs that helds in such systems, as well as we trust in "ordinary" proofs. — Ht 12:56, 14 May 2012 (UTC)

I think that it's fair to say that the failure of the implementation to satisfy the properties which were proved for the type means nothing to you. If you ever care to become aware of counter example, I suggest you spend some time visiting the risks forum. Nevertheless, I shall endeavor to create an implementation which fails in this fashion. It's a shame that you feel this concept is too complicated for you to explain for it to be included in the task description. But I shall propose this change, myself. --Rdm 12:17, 14 May 2012 (UTC)

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? — Ht 07:33, 14 May 2012 (UTC)

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. --Rdm 01:53, 14 May 2012 (UTC)

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 systems uses unification... Well, it's still required to get the point. Talking about the "upper bounds" is not even funny :) — Ht 07:33, 14 May 2012 (UTC)

And that's fine, until you start asking people to implement these infinite concepts as types. To use your turn of phrase, that's "not even funny :)". --Rdm 11:53, 14 May 2012 (UTC)

My current inclination is to believe that you cannot get the point of dependently-typed programming languages / proof systems. — Ht 23:00, 13 May 2012 (UTC)

This will be my final attempt to clarify this to you (please grab a book or article on type theory if you want to know how mathematicians and computer scientists define a type): The only implication of the fact that an actual implementation of a given logic/type theory runs on a machine with a finite amount of memory is that the set of results the compiler can give is extended from "I was able to verify the proof as correct" and "I was able to verify the proof as incorrect" with "I'm unable to verify the proof as either correct or incorrect because I ran out of memory". The third option must not occur here. The compiler should say "I was able to verify the proof as correct", assuring us that the property even + even = even hold for all countably infinite pairs of natural numbers.

Similarly if the theorem asked us to proof that reversing a linked list twice gives us back the original linked list, we should be able to prove this. This proof should hold independently of whether the machine has an 32-bit, 64-bit or even unbounded word size. Having a finite amount of memory will not prevent a computer working with infinities, it will only bound the maximum complexity of the proof - exactly similar to the situation where a mathematician only has a finite amount of paper to work on (and I've yet to meet a mathematician with an infinite supply of paper).

I'm strongly getting the impression that you've never managed to work out a proof by induction on paper, however, making this beyond you abilities to comprehend. In that case either do the appropriate background research or simply accept this on authority. —Ruud 12:04, 14 May 2012 (UTC)

Deletion of statement about finite limits from task

(I moved this from in the middle of some other comments to its own subtopic.)

Your last addition:

Note also that it's expected that the implementation of the type will fail to satisfy the peano axioms for some values. It's only required that the implementation succeed for values which do not exceed some non-trivial finite limit. The proof is not meant to apply to the implementation for values which exceed that limit.

The "implementation of the type" is the implementation of Martin-Lof type theory (or its extension), the paper has a model of natural numbers similar to the system of Peano axioms. — Ht 12:56, 14 May 2012 (UTC)

This is not searchable text, it's photographic material and it uses a variety of definitions defined in other places. So it's difficult, at a glance to see if it adequately treats the topic of machine limitations in an implementation. If any of this is relevant to the topics of limits of validity, please restate the relevant constructs in your own words. --Rdm 13:17, 14 May 2012 (UTC)

By extension Rdm believes that because mathematicains only have a finite number of sheets of paper they have only been able to prove theorems about the natural numbers which hold up to some non-trivial finite limit. I'm not sure how to argue with someone who is so confused about elementary concepts. —Ruud 13:11, 14 May 2012 (UTC)

This is trivially false, in the sense that I have stated nothing about a relationship between sheets of paper and proofs. Please refrain from making up stuff about me. --Rdm 13:17, 14 May 2012 (UTC)