Talk:Proof: Difference between revisions
(proofs and Type dependency) |
No edit summary |
||
| Line 9: | Line 9: | ||
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... [[User:Sgeier|Sgeier]] 17:45, 11 March 2008 (MDT) |
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... [[User:Sgeier|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. --[[User:Short Circuit|Short Circuit]] 19:40, 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. --[[User:Short Circuit|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"? |
|||
--[[User:Kevin Reid|Kevin Reid]] 00:07, 17 February 2009 (UTC) |
|||
Revision as of 00:07, 17 February 2009
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)