




Scheme Programming Language









Question: Mathematics and Computer Science
Hello all, This is not exactly a scheme question, but I assume many of you will have some good insight and advice to help me understand this topic. My mathematics professor, who is by no means a computer scientist, made a oomment regarding the relationship between computer science and mathematics. He personally guessed that any conceivable computer program ought to be theoretically provable. That is, even if it might not be reasonably feasible to actually develop and verify the proof, it is conceivable that any computer program should be provable mathematically (I assume this is just a way of saying that it is rigorously provably correct, but correct me, please if I am wrong here). However, as I began to think about this I wondered if this was indeed the case. Assuming a turing complete computer language, is it possible to create a program which does not have a conceivable proof of correctness that would fall within the realm of mathematical rigour or domain? My inclination is to say, yes, there is such a program; however, my professor guesses that there is not; neither of us really knows one way or the other. The second question along these lines is whether it is possible to create a program which is provably unprovable. Now, admittedly, I'm not all that fluent in the underlying concepts surrounding the most basic theories of computer programs and process in general, and so I could be barking up a ridiculously small tree or I could be attempting to swim up Niagra Falls, I don't know. I am hoping that someone could take some time out of their lives to enlighten me on how this all works out, because I'm rather curious here. :) Thanks, Aaron  aaron.@sacrificumdeo.net
I'd think the halting problem would not be provable. http://en.wikipedia.org/wiki/Halting_problem  A bad analogy is like a leaky screwdriver.  Richard Braakman
>>>>> "Eric" == Eric Hanchrow <off @blarg.net> writes: Eric> I'd think the halting problem would not be provable. Eric> http://en.wikipedia.org/wiki/Halting_problem Er, I mean, a program that doesn't halt wouldn't be provable.  [Dijkstra's] great strength is that he is uncompromising. It would make him physically ill to think of programming in C++.  Donald E. Knuth
On 20070402 22:51:28 0500, Eric Hanchrow <off@blarg.net> said: >>>>>> "Eric" == Eric Hanchrow <off @blarg.net> writes: > Eric> I'd think the halting problem would not be provable. > Eric> http://en.wikipedia.org/wiki/Halting_problem > Er, I mean, a program that doesn't halt wouldn't be provable.
Hrm, I suppose that makes sense, but what about programs that run to completion? I mean, there are not a whole lot of programs that are in practical use at the moment which run forever and never complete, or at least part of their code goes to completion. Aaron  aaron.@sacrificumdeo.net
>>>>> "Aaron" == Aaron Hsu <aaron. @sacrificumdeo.net> writes: >> Er, I mean, a program that doesn't halt wouldn't be provable. Aaron> Hrm, I suppose that makes sense, but what about programs Aaron> that run to completion? Well, sure, but (if my vague "understanding" of the Halting Problem is correct), the point is there's no way, in general, to tell whether the programs will halt or not, by inspection.  Always code as if the guy who ends up maintaining your code will be a violent psychopath who knows where you live.  John F. Woods
Eric Hanchrow <off @blarg.net> writes: >>>>>> "Eric" == Eric Hanchrow <off @blarg.net> writes: > Eric> I'd think the halting problem would not be provable. > Eric> http://en.wikipedia.org/wiki/Halting_problem > Er, I mean, a program that doesn't halt wouldn't be provable.
This is a strange way of putting it. What the Halting Problem says is this (from the article): Given a description of a program and a finite input, decide whether the program finishes running or will run forever, given that input. To Aaron Hsu: several other problems about computer programs have been shown to be equivalent to the halting problem. That means they are also undecidable. One of them, IIRC, is whether a program will produce a certain output from a given input. This may be more similar to what you and your professor have in mind when you talk about proving computer programs. This Wikipedia article may also be of interest: <http://en.wikipedia.org/wiki/List_of_undecidable_problems>  Wolfram Fenske A: Yes.
>Q: Are you sure? >>A: Because it reverses the logical flow of conversation. >>>Q: Why is top posting frowned upon?
Eric Hanchrow <off @blarg.net> writes: >>>>>> "Aaron" == Aaron Hsu <aaron. @sacrificumdeo.net> writes: > >> Er, I mean, a program that doesn't halt wouldn't be provable. > Aaron> Hrm, I suppose that makes sense, but what about programs > Aaron> that run to completion? > Well, sure, but (if my vague "understanding" of the Halting Problem is > correct), the point is there's no way, in general, to tell whether the > programs will halt or not, by inspection.
You understand correctly. :)  Wolfram Fenske A: Yes.
>Q: Are you sure? >>A: Because it reverses the logical flow of conversation. >>>Q: Why is top posting frowned upon?
In article <2007040221282516807aaronhsu@sacrificumdeonet>, Aaron Hsu <aaron.@sacrificumdeo.net> wrote: > My mathematics professor, who is by no means a computer scientist, made > a oomment regarding the relationship between computer science and > mathematics. He personally guessed that any conceivable computer > program ought to be theoretically provable.
A program is not provable. A proposition regarding the program might be. Presumably what you are asking is whether for any proposition regarding the behavior of a program written in a Turingcomplete language, either that proposition or its negation is provable. As you have already been told, the answer is clearly no, as shown by Rice's theorem. However, if your specification language is "the language of ordinary mathematics" (presumably ZFC, more or less), the answer is no even regardless of our inability to reason about computation. For example, suppose we wish to prove the following property: P(x) := program x evaluates to #t if and only if G where G is the Gdel sentence of the particular logical theory we are working with, and states that in that theory G is not provable Then let the program x, written in Scheme, be the following: x := #t If the logical theory is consistent, G is undecidable, and hence P(x) is also, even though the program x itself is quite trivial. So in short, since there are undecidable mathematical propositions, there are also undecidable mathematical properties of programs. Once we drop the math and restrict to purely computational statements about the programs, we find that gdelian diagonalization is still applicable, just in a different form, and that's called the halting problem. Lauri
On 20070403 02:14:05 0500, Lauri Alanko <l@iki.fi> said: > In article <2007040221282516807aaronhsu@sacrificumdeonet>, > Aaron Hsu <aaron. @sacrificumdeo.net> wrote: >> My mathematics professor, who is by no means a computer scientist, made >> a oomment regarding the relationship between computer science and >> mathematics. He personally guessed that any conceivable computer >> program ought to be theoretically provable. > A program is not provable. A proposition regarding the program might > be. Presumably what you are asking is whether for any proposition > regarding the behavior of a program written in a Turingcomplete > language, either that proposition or its negation is provable.
[...] Thanks! These answers have been really helpful to me understanding how this all works. Aaron Hsu  aaron.@sacrificumdeo.net
On Apr 2, 7:28 pm, Aaron Hsu <aaron.@sacrificumdeo.net> wrote: > Hello all, > This is not exactly a scheme question, but I assume many of you will > have some good insight and advice to help me understand this topic. > My mathematics professor, who is by no means a computer scientist, made > a oomment regarding the relationship between computer science and > mathematics. He personally guessed that any conceivable computer > program ought to be theoretically provable. That is, even if it might > not be reasonably feasible to actually develop and verify the proof, it > is conceivable that any computer program should be provable > mathematically (I assume this is just a way of saying that it is > rigorously provably correct, but correct me, please if I am wrong here).
Your professor is wrong. There exist programs that are correct but cannot logically have a proof of correctness. This is a direct consequence of Godel's Incompleteness Theorem. > However, as I began to think about this I wondered if this was indeed > the case. Assuming a turing complete computer language, is it possible > to create a program which does not have a conceivable proof of > correctness that would fall within the realm of mathematical rigour or > domain? My inclination is to say, yes, there is such a program; > however, my professor guesses that there is not; neither of us really > knows one way or the other. The second question along these lines is > whether it is possible to create a program which is provably unprovable.
Yes.
"Joe Marshall" <eval.ap @gmail.com> writes: > Your professor is wrong. There exist programs that are correct but > cannot logically have a proof of correctness. This is a direct > consequence of Godel's Incompleteness Theorem. On the other hand, there are positive statements one can make in this regard. Hoare's proof system for a simple imperative language has a small number of proof rules. Cook showed that the system was relatively complete for partial correctness, meaning that if the triple (precondition, program, postcondition) was semantically valid, then there was a proof of it in the system. The caveats are:  Validity for partial correctness means that when the program is started in a state satisfying the precondition, and it terminates, then the postcondition holds.  "Relatively" means that the logical assertions in the triple and in the intermediate triples used in the proof must be expressible, and that all true statements of the form P=>Q needed in order to adjust pre/postconditions of intermediate triples can be assumed. The two caveats rule out counterexamples based on the halting problem and the incompleteness theorem that we've seen in this thread (plus a third sort we haven't seen, namely "You can't prove this property of this program because you can't even say it in the logical language I let you use."). Hoare's language is pretty simple, and there is work showing that relative completeness does not hold for certain more expressive languages. PR  Prabhakar Ragde, Professor plragde at uwaterloo dot ca Cheriton School of Computer Science http://www.cs.uwaterloo.ca/~plragde Faculty of Mathematics DC 1314, (519)8884567,x4660 University of Waterloo Waterloo, Ontario CANADA N2L 3G1
Prabhakar Ragde wrote: > The two caveats rule out counterexamples based on the halting problem > and the incompleteness theorem that we've seen in this thread (plus a > third sort we haven't seen, namely "You can't prove this property of > this program because you can't even say it in the logical language I > let you use.").
In the context of this thread, that's a misleading way to say it. It would be better to explain "relative completness" as saying Hoare's system would be complete if only we had an oracle capable of solving all mathematical problems, including the halting problem. Since no such oracle exists, there cannot be any complete method for proving the correctness of programs. The math professor was just wrong about that. The importance of relative completeness for Hoare logic is that it doesn't add any new sources of incompleteness. If you can't prove something about a While program using Hoare logic, it's because there is no complete proof system for mathematics. Will
Aaron Hsu wrote: > I mean, there are not a whole lot of programs that are in > practical use at the moment which run forever and never complete, or at > least part of their code goes to completion.
Servers and Daemons mostly have this property. Once you start them, there's no way to stop them without an explicit kill command that moreorless orders the operating system to deallocate their resources and stop scheduling them for CPU time. Bear
On 20070403 19:13:11 0500, Ray Dillinger <b@sonic.net> said: > Aaron Hsu wrote: >> I mean, there are not a whole lot of programs that are in practical use >> at the moment which run forever and never complete, or at least part of >> their code goes to completion. > Servers and Daemons mostly have this property. Once you start > them, there's no way to stop them without an explicit kill > command that moreorless orders the operating system to > deallocate their resources and stop scheduling them for CPU > time.
Well, I'm aware that many programs are designed to loop endlessly and handle connections or other kinds of repeated tasks. However, I assume that one can look at parts of the program which the "scheduler" or main loop calls as separate and independent entitiies on many of these programs, and so, if these are terminating programs, they might be provably correct, and the only part of the software which is not possible to prove correct would be the main loop. I'm aware that this is a specific case, but I assume the general principle would apply to any decently modular piece of software, right? If I write a server in Scheme I have that main loop (which would also have an exit message which could be passed to it which would allow the program to terminate (so I wouldn't quite ocnsider this an absolutely nonterminating program), and then have terminating sub routines and modules which handle most everythng else.  Aaron Hsu  aaron.@sacrificumdeo.net
On 20070403, Aaron Hsu wrote: > However, as I began to think about this I wondered if this was indeed > the case. Assuming a turing complete computer language, is it possible > to create a program which does not have a conceivable proof of > correctness that would fall within the realm of mathematical rigour or > domain? My inclination is to say, yes, there is such a program; > however, my professor guesses that there is not; neither of us really > knows one way or the other. The second question along these lines is > whether it is possible to create a program which is provably unprovable.
As Lauri pointed out, the locution "provable program" doesn't make much sense. From recursion theory we know that for any consistent formal theory satisfying certain criteria  which all theories formalising our mathematical knowledge satisfy  there are infinitely many true statements of the form "the Diophantine equation D(x_1, ..., x_n) = 0 has no solutions" are unprovable in the theory. If we assume that all mathematical principles which are in principle acceptable to us, whatever that actually amounts to, are contained in a formal theory, it follows that there are infinitely many programs the termination of which is not provable on basis of principles potentially acceptable to us. To see this pick any Diophantine equation D(x_1, ..., x_n) = 0 that has no solutions but for which this is unprovable in a formal theory containing all mathematical principles potentially acceptable to us, and construct a program that systematically goes through each ntuple of naturals, checks whether the tuple is a solution to D, and halts if it is. (The business with Diophantine equations relies on the socalled MRDP theorem that states that every recursively enumerable set is Diophantine). There is no mathematical characterisation of mathematical proof  or, in other words, there is no mathematical definition of "mathematical principle potentially recognisable as correct by us"  so there can be no question of mathematically proving that something is not mathematically provable, just as there can be no mathematical proof of other nonmathematical claims such as "bananas are quite tasty" or "Wiles's proof is very difficult for ordinary mortals to follow". On the other hand, due to the constructive nature of Gdel's theorem, for any formal theory T (again satisfying certain criteria) we can construct a program P such that P does not halt but this fact is not provable in T, provided T is consistent. We can, for example, explicitly write down a program such that it does not terminate, but this is not provable in ZFC, provided ZFC is consistent, which it of course is, or a program which does not terminate but the nontermination of which is not provable in ZFC + there exists billions of Woodin cardinals, or whatever strikes our fancy.  Aatu Koskensilta (aatu.koskensi@xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen"  Ludwig Wittgenstein, Tractatus LogicoPhilosophicus
In article <1175627069.828577.102@l77g2000hsb.googlegroups.com>, William D Clinger wrote: > The importance of relative completeness for Hoare logic is that it > doesn't add any new sources of incompleteness. If you can't prove > something about a While program using Hoare logic, it's because > there is no complete proof system for mathematics.
It's also possible I can't prove something about a while program because I am too dumb to come up with the proof. :)  Neel R. Krishnaswami n@cs.cmu.edu
On 20070405, Neelakantan Krishnaswami wrote: > It's also possible I can't prove something about a while program > because I am too dumb to come up with the proof. :)
Indeed. It's trivially the case that there are unprovable truths about programs in the sense that even if the truths are provable in some idealised sense all the proofs are too long and complicated for any human to follow or produce, even aided with all the computation power in the universe. Usually in discussing provability such matters are idealized away, which, depending on the context, might or might not make sense.  Aatu Koskensilta (aatu.koskensi@xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen"  Ludwig Wittgenstein, Tractatus LogicoPhilosophicus





