steve@hubcap.clemson.edu ("Steve" Stevenson) (07/12/90)
amull@Morgan.COM (Andrew P. Mullhaupt) writes: >... includes comments by Graph Theory experts ... >suspect a hole in the arguments which reduce the problem.... This kind of >thing goes on all the time in math, and doesn't differentiate the >FCT from most other spectacular conjecture resolutions. True enough, however my interest is in the fact that a computer program is involved. In the philosophical sense, has FCT been `proven' if it has an `unproven' computer program in the middle? -- =============================================================================== Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
stig@idt.unit.no (Stig Hemmer) (07/13/90)
The story I have heard is that the output from the program is possible to check by hand, and that is was done. The proof consists of finding a unavoidable set of subgraphs, and then showing that each and every one can be reduced. Both parts were done with computer asistance, but both can be done by hand. As far as I remember there were ~1000 subgraphs, so it is quite a big task, but I think they did it. My source is 'Mathematics: The New Golden Age' by Keith Devlin. Stig 'Tortoise' Hemmer aka stig@idt.unit.no aka hemmer@norunit.bitnet
aesop@milton.u.washington.edu (Jeff Boscole) (07/13/90)
In article <9649@hubcap.clemson.edu> steve@hubcap.clemson.edu ("Steve" Stevenson) writes: >... however my interest is in the fact that a computer program is >involved. In the philosophical sense, has FCT been `proven' if it has an Forgive me for being dense.... I've attempted to understand these issues thru Philosophy of Science classes and so forth.... Precisely -where- is the beef with a "proof by an (unverified.by.hand.calculation) computer program?" :=:
aaron@grad2.cis.upenn.edu (Aaron Watters) (07/13/90)
In article <9649@hubcap.clemson.edu> steve@hubcap.clemson.edu ("Steve" Stevenson) writes: > >... my interest is in the fact that a computer program is >involved. In the philosophical sense, has FCT been `proven' if it has an >`unproven' computer program in the middle? What makes you think that the program is any more or less proven than other parts of this or other proofs? The algorithm is certainly not `unproven' by normal standards of mathematical discourse. If your problem is with the possibility of an implementation mistake or a hardware error in the execution, I'd say this is much less likely than the possibility of an ordinary mathematical nonsequitur in the main part of the proof, especially since the algorithm has been reimplemented and rerun. -aaron.
alan@essex.ac.uk [Alan M Stanier] (07/13/90)
In a blatant attempt to disturb the Universe, aesop@milton.u.washington.edu (Jeff Boscole) just said }Forgive me for being dense.... I've attempted to understand these issues }thru Philosophy of Science classes and so forth.... Precisely -where- is ^^^^^^^^^^ }the beef with a "proof by an (unverified.by.hand.calculation) computer ^^^^^^^^ }program?" "where is the beef?" Sorry, I don't understand this colloquialism. [ I can imagine it meaning "Where is the substance to ..." or "What is the objection to ..." ] Could someone translate this question into English English? -- Alan M Stanier | email barefeet@sx.ac.uk | These opinions void where tel +44 206-872153 | fax +44 206-860585 | prohibited by local laws.
amull@Morgan.COM (Andrew P. Mullhaupt) (07/13/90)
In article <9649@hubcap.clemson.edu>, steve@hubcap.clemson.edu ("Steve" Stevenson) writes: > amull@Morgan.COM (Andrew P. Mullhaupt) writes: > > >... includes comments by Graph Theory experts ... > >suspect a hole in the arguments which reduce the problem.... This kind of > >thing goes on all the time in math, and doesn't differentiate the > >FCT from most other spectacular conjecture resolutions. > > > True enough, however my interest is in the fact that a computer program is > involved. In the philosophical sense, has FCT been `proven' if it has an > `unproven' computer program in the middle? I am not aware of any reason that the computer part of the FCT proof should not be proven; what I mean here is that the source for the program can (and should) be equipped with a proof of partial correctness. (Since we know it halts, partial correctness implies total correctness.) Now the only hole in such an approach is faulty execution of the program by the system which processes it. (Likely a compiler or interpreter, an O/S and some hardware.) Now correctness of compilers and operating systems should be a given, but it's not. At present, the communities which produce compilers and operating systems are not sufficiently convinced of the merit and feasability of correct compilers and operating systems to produce them. So we can consider the whole of the proof from the compiler/interpreter, through the operating system and hardware as a single processor and assess the risk of error. The first point is the nature of errors. There are no floating point computations (as far as I know) so that a Lanford style proof by estimates is not necessary. The answer is either that you can successfully dispense with each of the finitely many critical cases or no you can't. Now the likelihood of an error in the hardware over the run in question is (on today's machines) a fixed small number, likewise the operating system and compiler. You can satisfy practical doubts you may have regarding the computation by repeating it more than once with different hardware, compilers and operating systems. (It might be easier to use different flavors or versions of the same operating system so long as they arent the same code.) It now becomes a problem in statistics to compute confidence bands for the hypothesis that the set of computations you have performed has been without error. You can quite reasonably expect to obtain results which are as good as you could obtain for passing manuscripts through referees, etc. So as a practical matter there is not much reason to treat computations as different from proofs. The other issue is that the computer proof of the FCT is not even in principle checkable by humans in reasonable time; whereas other, equally stultifying proofs (e.g. Carleson's pointwise convergence of L2 Fourier series theorem) _can_ be checked by _some_ (very determined) humans, even though most of us mortals take the experts' word on it. Well ok. There it is. You pays your nickel and you takes your choice. Who are you going to believe? This is not an idle issue; the recent proof of the Wagner conjecture (yet another jihad most of us will not experience in our lifetimes) results in a way to show that lots and lots of interesting kinds of graphs have only finitely many minimal cases under minors. I.e. this is a machine for resolving lots of questions in graph theory in the same way as the FCT. Before he got g_19 by hand, Deshouillers was aware that the result could have been had by exhaustion to the then best estimates by the use of a massively parallel computer. We almost went ahead and did it, too. A lot of mathematics is coming in range of cheaper and faster computers as time goes by, and we're going to see more and more cases where results hang by hybrid proofs. My response is twofold. We have to make mathematicians aware of the fact that programming can be done as theorem-proving. We have to institute a standard for quality control in computation. The right people to do it are the mathematicians, because they have the greatest need to understand the reliability of computations, and because they are the best equipped to face the problems involved. Later, Andrew Mullhaupt
jeffr@sco.COM (Jeff Radick) (07/14/90)
In article <4997@milton.u.washington.edu> aesop@milton.u.washington.edu (Jeff Boscole) writes: > ... >Forgive me for being dense.... I've attempted to understand these issues >thru Philosophy of Science classes and so forth.... Precisely -where- is >the beef with a "proof by an (unverified.by.hand.calculation) computer >program?" > ... It seems to me that a Philosophy of Science class should address this issue, but ... well, here's my opinion: Presumably a "proof" of an assertion, in the general sense of the word, is a test of its truth. As used by mathematicians, philosophers, and logicians, a "proof" is an argument which convinces a person knowledgeable in the subject matter of the assertion in question that the assertion follows from some set of hypotheses by a series of steps of reasoning which are generally accepted as valid. This is normally done by stating some series of steps in the chain of reasoning and either directly or indirectly alluding to some rule by which that steph should be considered to be valid; usually many steps or rules are omitted as being "obvious" but which in principle can be provided by those reasonably knowledgeable in the field in question. For example, few proofs will cite "modus ponens" every time it is used (in fact few will cite it at all) but a mathematical proof might well cite the Baire category theorem or Poincare's lemma or Gauss' Theorema Egregium. The point of this is that a "proof" is in principle something to be understood by human beings. If noone understands the chain of reasoning sufficiently well to be convinced that all steps are correct, then in a certain very real sense it is not really a proof. The question for a proof in which the output of a computer program is used as one or more critical steps in the reasoning, is whether or not the output of the program is correct. If the correctness of the program is not "proven", then at least in principle the correctness of the proof citing its output is in doubt. If the output of the program is itself intended to be a "proof", then in principle it can be checked by humans but if it is preposterously long -- say thousands of pages -- then it is unclear that anyone will ever really understand it all, so it is unclear that any human being can really be satisfied that all steps in the proof are "correct", hence it is not certain that the proof can be really accepted as "correct". Thus a practial approach to the problem might be to put the onus of proof back on the program itself. If the program is small enough to be amenable to an acceptably short proof (i.e., short enough to be understood by a human being) then perhaps its output and its proof could be accepted as a valid part of the larger proof. Now it might be that what is actually proven is not the program itself but rather the algorithm used. Then the question is whether the program actually used is a valid implementation of the algorithm. This can be addressed in an experimental sort of way by having different researchers independently implement the algorithm, then compare results. However, the results may still be in doubt since conceivably the independent researchers may still have a common error. Whether these issues have been adequately addressed in a way acceptable to the mathematical community in the case of the Four-Color problem is beyond my realm of expertise; however I believe this to be a valid statement of the issues involved. Jeff Radick software engineer and math student jeffr@sco.com or uunet!sco!jeffr or radick@ucscb.ucsc.edu
yodaiken@chelm.cs.umass.edu (victor yodaiken) (07/15/90)
In article <1233@s8.Morgan.COM> amull@Morgan.COM (Andrew P. Mullhaupt) writes: >In article <9649@hubcap.clemson.edu>, steve@hubcap.clemson.edu ("Steve" Stevenson) writes: >> amull@Morgan.COM (Andrew P. Mullhaupt) writes: >> > >I am not aware of any reason that the computer part of the FCT proof >should not be proven; what I mean here is that the source for the >program can (and should) be equipped with a proof of partial correctness. The reason appears to be that any such "proof", using current techniques, would be less obviously correct than the program itself. Are there examples of partial correctness proofs of substantive programs?