Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 17 Sep 2006 23:48 Steven Zenith wrote: > I have referred you to the relevant literature that more than > adequately explains the formalism and methods of transformation. No it doesn't. It is your responsibiity to prove your point. You use this forum to make your claims of success, but not to show the solution that you claim exists. Giving the title of a book or article does not prove anything. The onus is on you to prove your solution exists. You have done nothing to show that there is a published formalization of any branch of Computer Science. I have spent far too much time tracking down bullshit articles and exposing them in this forum. Why should I have to go buy or locate an out-of-print book only to discover it is another wild goose chase? I have read hundreds or articles that attempt to formalize some aspect of Computer Science. All were bogus. I have asked for an example for months. Who has ever posted one? Who? "I'm too lazy to read the literature. I don't know the literature." Bullshit. I have explained in detail how Curry-Howard, Moore/Boyer's Halting Problem paper, TPTP, Modal Logic, and other attempts fail. How much time and how many wild goose chases do I have to go on? Who will compensate me for my wasted time? If you know of a solution, why don't you spend 5 minutes to give it here - instead of me spending days tracking down more bullshit? C-B > 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: Charlie-Boo on 18 Sep 2006 00:00 Patricia Shanahan wrote: > 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? Any system that represents the recursive functions will do. It is sometimes called a "Base of Computing" or a language that is "Turing Complete". But in every case you have an r.e. set (the programs) and a map from it (the rules of executing a program) onto the recursive functions. It is assumed that you use the same set for programs, inputs and outputs. In practice, you may have to code each program as a string that can be output. (Your example may be a case of this.) But the coding is unimportant. If you are trying to prove me wrong by saying that the very assertion that such a program must exist is wrong, then you are barking up the wrong tree. It is a fundamental result of Recursion Theory that such a program must exist. Formally proving it in CBL shows that what is actually needed in the system is for the substitution function to be represented. C-B > Patricia
From: Charlie-Boo on 18 Sep 2006 00:25 Steven Zenith wrote: > 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. Every programming language can implement a function to calculate square root to a given number of places. It has nothing to do with "performance constraints". > 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. No, you just have to know that it is a Programming Language. You sound like a drunkard babbling on the street. > 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. Any idiot knows you can carry out the calculation of square root to any specified number of digits. It involves only recursive operations. > IOW, if formally constrained the program may or may not run on a given > platform. That's nonsense. All Programming Languages have the same computing power: the recursive functions. > 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? You merely keep the individual digits in an array (as I said.) > 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 Functions don't terminate, programs do. How do you define a function terminating? > 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. Yeah, I'm just ignorant and haven't read the literature. > 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. That has nothing to do with anything. Do you think that different programming languages (e.g. Fortran, Algol) have different computing abilities? > Early machines that ran > Algol 60 programs, or early FORTRAN programs especially, behave > differently on contemporary machines. > > READ THE LITERATURE. How about if you say something that makes sense? Where do I find literature discussing how "functions terminate"? C-B
From: Charlie-Boo on 18 Sep 2006 00:30 Steven Zenith wrote: > Charlie-Boo wrote: > > Economics has nothing to do with theoretical Computer Science. > If only that were true :-) What in the world does economics have to do with theoretical Computer Science? Get real. C-B > With respect, > Steven
From: Charlie-Boo on 18 Sep 2006 00:35
Steven Zenith wrote: > 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. I can spend hours, maybe days tracking down your references. Or you can spend 5 minutes explaining it and I can spend 5 minutes rebunking it. Which do you prefer? You claim to know of a solution. Then give it. Why talk all about it but stop when it's time to show everyone the solution that you claim exists? Pledge to pay me $100.00 if I spend the time, effort and money to track it down and prove that it's bullshit. Too many wild goose chases doing the work of others! C-B > With respect, > Steven |