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 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.8137&rep=rep1&type=pdf 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.
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 http://rosettacode.org/wiki/Help:Adding_a_new_programming_task#Things_to_avoid

--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 ℕ : Set where
 o : ℕ
 1+ : ℕ → ℕ

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)