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)

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)