Anonymous user
Talk:Proof: Difference between revisions
→J version: Add some notes on the Tcl code (and the fact that implementing a whole theorem prover for this task is unreasonable!); also tidy formatting
No edit summary |
(→J version: Add some notes on the Tcl code (and the fact that implementing a whole theorem prover for this task is unreasonable!); also tidy formatting) |
||
Line 85:
::::# 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
::::: --[[User:Rdm|Rdm]] 14:58, 10 May 2012 (UTC)
Line 95 ⟶ 96:
::::::: 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).
| |||