Home     |     .Net Programming    |     cSharp Home    |     Sql Server Home    |     Javascript / Client Side Development     |     Ajax Programming

Ruby on Rails Development     |     Perl Programming     |     C Programming Language     |     C++ Programming     |     IT Jobs

Python Programming Language     |     Laptop Suggestions?    |     TCL Scripting     |     Fortran Programming     |     Scheme Programming Language


 
 
Cervo Technologies
The Right Source to Outsource

MS Dynamics CRM 3.0

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 2007-04-02 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.

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.

In article <2007040221282516807-aaronhsu@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 Turing-complete
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 2007-04-03 02:14:05 -0500, Lauri Alanko <l@iki.fi> said:

> In article <2007040221282516807-aaronhsu@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 Turing-complete
> 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)888-4567,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 more-or-less orders the operating system to
deallocate their resources and stop scheduling them for CPU
time.

                                Bear

On 2007-04-03 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 more-or-less 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 non-terminating
program), and then have terminating sub routines and modules which
handle most everythng else.

- Aaron Hsu
--
aaron.@sacrificumdeo.net

On 2007-04-03, 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 n-tuple of naturals, checks whether the tuple is a solution to D, and
halts if it is. (The business with Diophantine equations relies on the
so-called 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 non-mathematical 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 non-termination 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 Logico-Philosophicus

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 2007-04-05, 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 Logico-Philosophicus

Add to del.icio.us | Digg this | Stumble it | Powered by Megasolutions Inc