Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Patricia Shanahan on 17 Sep 2006 12:48 Charlie-Boo wrote: > zzbunker(a)netscape.net wrote: >> Charlie-Boo wrote: >>> Do we all agree that Computer Science definitely should be formalized? >>> >>> While the definitions of common terms (e.g. recursively enumerable) are >>> formal, the manipulations of these concepts (e.g. the derivation of >>> proofs) is not. Can anybody show a single example of a formal >>> derivation of a result from any branch of Computer Science? For >>> example: >>> >>> 1. Program Synthesis: The creation of a computer program based on only >>> its specifications. >>> >>> 2. The Theory of Computation: A formal derivation of Turing's proof >>> of the unsolvability of the halting problem. >>> >>> 3. Recursion Theory: A formal proof that there is a program that >>> outputs itself, or of the Fixed Point theorem or the Recursion theorem. >> Programs that output themselves are quite trivial, >> since it's what the assembler instruction NOP does, >> >> Which isn't the same thing as programs that >> copy themselves. > > You are proving that there is a programming language in which there is > a program that outputs itself, but the theorem is that there is such a > program in all programming languages (C++, Algol, et. al.) Yet again, would an XML-based Turing machine description language that binds the tape alphabet to {'0','1',' '} be a programming language by your definition? Patricia
From: Steven Zenith on 17 Sep 2006 14:25 I have referred you to the relevant literature that more than adequately explains the formalism and methods of transformation. With respect, Steven Charlie-Boo wrote: > ... > Just give the rules and some examples as to how they successfully solve > the problem, ok? Otherwise you are making empty claims.
From: Steven Zenith on 17 Sep 2006 14:56 The dependence lies in the implementation. There is no *guarantee* that an implementation can meet the specification - that is compute to the number of specified places in a time that meets a performance constraint. Now, obviously, we can explicitly assert pragmatics on the program that causes a program to be unverifiable on platforms that cannot show that they provide the specified accuracy. To do this we will need a formal specification of the platform. Formally, without a pragmatic statement any program that uses root 2, with or without the second argument, either does not terminate, or cannot be verified without knowing the formal specification of the implementation of the function. IOW, if formally constrained the program may or may not run on a given platform. How is root 2 implemented on the machine you are currently using? Is it implemented the same way in all libraries? What does the IEEE standard say? Can you store an arbitrary precision result in a manner so that the value remains the same before and after storage? Does such storage rely upon pragmatic statements - implied? explicit? Don't get hung up on this particular example, the problem is extensive and applies to any resource or accuracy constrained platform (which is to say all platforms) to which you may wish to map a general purpose program without formal pragmatics - for both the program requirement and the platform specification. I used this example to illustrate the termination issue - there exist functions that do not terminate formally and require pragmatic statements. Those pragmatic statements may cause the program to vary its behavior when running under diverse pragmatic constraints. The reason this is an important observation is that no commercially available programs today use formal methodologies with this rigor, and few government funded programs do. I sympathize with your cause - and I think you would benefit by reading the literature I have referenced. Your comparison between languages demonstrates a lack of experience: for example, Algol 60 did not implement the IEEE floating point standard and that standard has itself evolved. Early machines that ran Algol 60 programs, or early FORTRAN programs especially, behave differently on contemporary machines. READ THE LITERATURE. With respect, Steven Charlie-Boo wrote: > Steven Zenith wrote: > > Jack Campin - bogus address wrote: > > >... > > > So you just add a second argument to the sqrt function saying how many > > > places of precision you want. That two-argument function does terminate, > > > and there's no implementation dependence about it. > > > > Well, you have now placed the implementation dependence in the new > > argument. > > Why is there implementation dependence in writing a program to > calculate square root to a given number of places? We simply perform > the calculation for the specified number of digits. (If they ask for > tons of digits, then we keep them in an array of digits and perform the > calculations on the array.) > > In fact, how could any exact specification be implementation specific? > If it can be implemented on one computer/programming language, then > obviously it can be implemented on all of them, as all programming > languages (meaning e.g. C++, Algol, etc.) implement the same functions. > > Again you are confusing ill-written (e.g. incomplete) specifications > with theoretical aspects of Computer Science. > > You are good at name dropping and referring to awards and > organizations, but your technical statements are unsubstantiated and > show a very immature understanding of both Mathematics (as regards the > concept of a function) and programming (as regards what can be > implemented.) > > C-B > > > It is better to explicitly express a pragmatic, I agree, but > > these pragmatics will play hell with the formal system unless > > differentiated from the algorithmic goals. > > > > With respect, > > Steven
From: Steven Zenith on 17 Sep 2006 14:58 Charlie-Boo wrote: > > Economics has nothing to do with theoretical Computer Science. > If only that were true :-) With respect, Steven
From: Steven Zenith on 17 Sep 2006 15:00
Charlie-Boo wrote: > You have many words claiming success at solving these problems, but are > silent on substantiating these claims. If you read the references there would be no silence. With respect, Steven |