|
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. :) [[User:Markhobley|Markhobley]] 15:33, 13 July 2011 (UTC)
== J version ==
This is not a proof, right? — [[User:Ht|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. --[[User:Rdm|Rdm]] 13:36, 10 May 2012 (UTC)
:: But this page is using the term "proof" in formal sense of [[wp:constructive mathematics|constructive mathematics]]/[[wp:Curry-Howard correspondence|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. —''[[User:Ruud Koot|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.
::: --[[User:Rdm|Rdm]] 14:17, 10 May 2012 (UTC)
::::# I think the boldfaced note expresses this, although the task description can indeed be made more clear.
::::# 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. –[[User:Dkf|Donal Fellows]] 08:36, 14 May 2012 (UTC)
::::# 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.
:::: —''[[User:Ruud Koot|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 [[Help:Adding a new programming task#Things_to_avoid|the guidelines]].
::::: --[[User:Rdm|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.—''[[User:Ruud Koot|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. --[[User:Rdm|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 [[wp:Peano axioms|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:
::::::::# State the required theorem (e.g. encoded as a type in the language's type system.)
::::::::# 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. —''[[User:Ruud Koot|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 --[[User:Rdm|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. —''[[User:Ruud Koot|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. --[[User:Rdm|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? —''[[User:Ruud Koot|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. --[[User:Rdm|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. —''[[User:Ruud Koot|Ruud]]'' 20:38, 10 May 2012 (UTC)
::::::::::::::: No. I made no claims about the Collatz conjecture. --[[User:Rdm|Rdm]] 20:44, 10 May 2012 (UTC)
:::::::::::::::: No you didn't, but your method is equally applicable. I used it to prove [[wp:Goldbach's conjecture|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 [[User:Rdm|Rdm]] believes in such proof of GC, he just does't believe in presented proofs for the task. — [[User:Ht|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.) --[[User:Rdm|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.
::: --[[User:Rdm|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. --[[User:Ledrug|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. --[[User:Rdm|Rdm]] 19:24, 13 May 2012 (UTC)
== Draft status ==
|