Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 15 Sep 2006 05:09 Some further observation: Formally, the second argument does not help you much since there is no guarantee the underlying architecture can support the (arbitrarily) requested precision or complete such a request in a timely manner. >From a practical point of view - I've thought about this problem before - storing values and operating upon them as continuous fractions would solve the problem I think. Then you only have to verify the implementation of these operations, which is a tractable problem. Sincerely, Steven 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. 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: Charlie-Boo on 15 Sep 2006 10:00 Steven Zenith wrote: > For further clarification: With all due respect, I think it's hopeless. > A function that computes the square root of 2 is a good example of a > non-terminating function. I'm afraid you're confusing concepts. Programs terminate or not. Functions are defined or not. A function that maps to the square root of 2 is defined, just as one that maps to 3 is. It is not a "non-terminating function". Suppose we define function cb(x) as follows: cb(1) = 1 cb(2) = square root of 2 cb(3) = {1, 2} cb(4) = {0, 1, 2, 3, . . .} otherwise cb(x) is not defined Then cb(1), cb(2), cb(3) and cb(4) are all defined, and cb(5) is undefined. It doesn't matter whether the value returned is an integer, an irrational number, a finite set or an infinite set. These are all mathematical objects that can be in the range of a function. > In what formal computational sense can it be > said to terminate? Logically, none. Not so. cb(2) is in fact defined. It doesn't matter whether its value is a rational number or an irrational number or any other mathematical object. > However, pragmatically, we know that implementations terminate by at > some point producing an approximation of the function - these > pragmatics will vary from implementation to implementation. Programs > dependent on such results will vary in their behavior. No. The process is well-defined. If we write a subroutine to output the first 10 decimal digits of the square root of it's input, we will get the same result on any implementation of that programming language. If two implementations give different results, then at least one of them is faulty. You are confusing (1) whether a function has an output (for a particular input) with whether its output (if it has one) is finite or infinite, and (2) faulty specifications for software that don't say how many decimal places to use, with faulty implementations that use a different number of decimal places than has been specified. Your understanding of both Mathematics and of Computer Programmer seems quite weak. Your claim to have produced a wonderful result, but computer programmers reject it only because companies would rather implement faulty software requiring high-priced maintenance to repair, is unsubstantiated and quite dubious. (Actually, most bug fixing is done under a maintenance contract that charges by the month, not by the time expended. Can you imagine a user organization receiving a high bill and the vendor says they have to pay lots of money because the software that the vendor sold them is full of bugs? How many organizations would put with such a double whammy?) Speaking of dubious, if you think that you or your friends have formalized some branch of Computer Science, can you at least tell us (in lieu of criteria A-F) what branch of Computer Science they formalized, and 3 or 4 results that are generated by their formalism? Sorry, but I seriously doubt that you can. Feel free to prove me wrong. C-B > Sincerely, > Steven > > > Steven Zenith wrote: > > I meant to say "functions of the kind you describe terminate" - > > obviously, recursive functions - such as those that may produce > > irrational numbers - do not necessarily terminate. This "determinism," > > or lack of it, is another subject covered by Roscoe and co. in the > > 1980s. > > > > Sincerely, > > Steven > > > > > > Steven Zenith wrote: > > > Charlie-Boo wrote: > > > > ... > > > > > It is not that these projects did not produce compelling results - we > > > > > did, and to international acclaim > > > > > > > > What is the significance of "acclaim"? > > > > > > Merely in the sense that the results were widely recognized. > > > > > > Before judging this work, and much like it, that took place in the > > > formal methods community at least between 1950 and 1990, I suggest that > > > you read some of it. > > > > > > No one is suggesting that not to use these techniques is corrupt - it > > > has simply an associated economic pragmatic that has been important > > > during a very competitive era. When time to market is no longer > > > important companies will be prepared to spend the upfront time to > > > formally engineer their code. And there is the rub in much of your > > > comments. I don't really see what you are after in the computer science > > > sense if you are not after the application of formal methods to > > > engineering. If you are rather looking for abstract principles of > > > computational theory, that seems to be less an engineering task as a > > > general task in logic and there is plenty on literature in that domain. > > > > > > Formal methods very often deal with the obvious. In logic of course a > > > function terminates, that assumption cannot be made in computer science > > > since one needs to understand the implementation and the machine > > > architecture. > > > > > > When I refer to Standards - I am referring to industry standards for > > > protocols and interfaces - few of which provide a formal specification. > > > To verify an implementation of such a standard I not only need a > > > formal spec but also a formally verified target platform. > > > > > > That you do not understand this about termination and that you cannot > > > readily identify issues that prevent the ready application of formal > > > methods to conventional languages - side effect free functions perhaps > > > being the most obvious - I again suggest you read the literature. > > > > > > With respect, > > > Steven
From: Charlie-Boo on 15 Sep 2006 11:40 abo wrote: > Does *your* system only have a small number of > intuitively obvous axioms? If so, what are they? The first few for each branch of Computer Science are: Program Synthesis: ADD(I,J,X)*, MUL(I,J,X)*, LT(I,J)* Theory of Computation: YIT(I,J,K)*, TRUE(x), LT(x,I)* Recursion Theory: M#f(I)=>s11(M,N)#f(N), s11(I,J) Incompleteness in Logic: -~P/P If you'd like more details for any of these branches of Computer Science, I'd be glad to give it. > > The question was, where is the BS? > It's in your "yes" - when you replied that your 5- or 10-step proof has > any particular significance. You don't see any significance to reducing a 15 page proof down to 10 formal steps? Do you subscribe to Occam/C-B's Razor? C-B
From: abo on 15 Sep 2006 12:42 Charlie-Boo wrote: > abo wrote: > > Does *your* system only have a small number of > > intuitively obvous axioms? If so, what are they? > > The first few for each branch of Computer Science are: > > Program Synthesis: ADD(I,J,X)*, MUL(I,J,X)*, LT(I,J)* > Theory of Computation: YIT(I,J,K)*, TRUE(x), LT(x,I)* > Recursion Theory: M#f(I)=>s11(M,N)#f(N), s11(I,J) > Incompleteness in Logic: -~P/P "First few"? Sorry, I would need a complete list. I would also need either an explanation of what the terms mean or an explanation of the axioms. > > If you'd like more details for any of these branches of Computer > Science, I'd be glad to give it. > > > > The question was, where is the BS? > > > It's in your "yes" - when you replied that your 5- or 10-step proof has > > any particular significance. > > You don't see any significance to reducing a 15 page proof down to 10 > formal steps? I'd answer like this: I'd be more interested if you had claimed that you had managed to reduce Godel's First Theorem down to a formal proof with 1000 steps than with 10.
From: ?a/b on 15 Sep 2006 13:08
On 14 Sep 2006 12:38:03 -0700, george wrote: > >Charlie-Boo wrote: >> You have to tell in advance an exact algorithm that creates every >> proof. > >That this is trivial is PRECISELY what Godel's proof proves. >1st-order consequence is recursively enumerable. >There is an algorithm that (your choice) recursively enumerates >proofs (there are only a finite number of proofs of length n, false >for any n), or confirms that a candidate proof submitted as input >is in fact elected when it is in fact a proof (if it's not a proof, the >algorithm might not terminate). > >> You are saying that it can be formalized, but Godel didn't. > >Yes, he did -- didn't you read the other replies. >He didn't say he could or was doing it, but he did say >it was doable. Hilbert and Bernays in fact shortly >thereafter did it. IT HAS been done. The question is >not whether it's been formalized; it's just whether it is >computer science. |