Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 16 Sep 2006 04:28 Charlie-Boo wrote: > Why do you say that I need to read "some of it"? Because "some" is better that "none." With respect, Steven
From: Steven Zenith on 16 Sep 2006 04:43 Charlie-Boo wrote: > > 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". Indeed, however, I was talking about the property of termination, not definition. There are functions that are defined but clearly do not terminate. A function that computes the root of 2 is one of them. A program is merely the instance of a defined function. So, from a formal point of view, no program that uses a function that computes the root of 2 terminates. Any function using such a function that does terminate is employing a pragmatic that results in implementation specific behavior. With respect, Steven
From: Steven Zenith on 16 Sep 2006 05:47 Steven Zenith wrote: ...Any function using such a function > that does terminate is employing a pragmatic that results in > implementation specific behavior. It is perhaps more important to say here, again formally, that if "such a function that does terminate is employing a pragmatic that necessarily results in *instance* specific behavior." Such behavior maybe irrelevant in practice. In Microsoft Excel it *may* not present a problem. OTOH if you are doing something economically critical, like computing the trajectory of a space vehicle, then it may. This highlights the need for a distinct formal pragmatics that can be applied to each instance of a formally specified program. This non-terminating property of computing irrationals has implications in the foundations of mathematics and the question of what is computable - especially as it relates to the pragmatic aspects of applied conventional mathematics. There are clearly many conventionally defined functions, any that include or produce irrationals, that do not formally terminate. This all assumes that the terminating properties of programs in computer science are properties that are interesting formally - I'd suggest that they are. The issue can, perhaps, be glibly ignored by mathematics, but it certainly cannot be ignored by a formal consideration of computer or computational science. With respect, Steven -- Dr. Steven Ericsson-Zenith IASE, Sunnyvale, California
From: Steven Zenith on 16 Sep 2006 06:31 Charlie-Boo wrote: > The truth of the matter is, there are all sorts of people claiming to > have formalized various parts of CS, but none of them carries any > weight - simply because they don't show how to crank out results using > a set of formal rules. That's what formalizing is all about. This is simply wrong, I have already referred you to examples. Start here: http://web.comlab.ox.ac.uk/oucl/publications/prgtr/index.html In 1990, INMOS and Oxford shared a Queens Award for Industry for formally demonstrating that the Transputer microprocessor floating point unit met the IEEE floating point standard. The proof was actually performed by a colleague of mine, David Shepherd. Now I have no time for such awards myself, but it is proof of the case. This demonstration showed formally (i.e., it proved) that the IEEE spec could be translated formally into Occam and that the intermediate Occam could be formally translated into the machine implementation. In addition to demonstrating the specific case, this also demonstrated the general case that the formal system we had designed was robust. In following years these tools were strengthened and developed as commercial enterprises but they failed for the economic reasons I have already described. > .. It's a hell of a lot of fun to play > with CBL and see what kinds of theorems you can produce in just a few > minutes. Now I get it. CBL is "Charlie Boo's Language" - so this entire discussion is some propaganda exercise. I wish I had spotted that earlier. There are, BTW, several theorem provers around that are used in hardware verification - especially see Mike Gordon's HOL (High Order Logic), which is available in Open Source. See: http://www.cl.cam.ac.uk/~mjcg/ Sincerely, Steven
From: Charlie-Boo on 16 Sep 2006 11:02
Jan Burse wrote: > For a start, try: > > Thompson, S.: Type Theory and Functional Programming, > Addison-Wesley Publishing Company, 1991 > > He gives a definition of quicksort and then > proofs its termination and correctness. There are plenty of instances of people taking a specific program and showing exactly how to verify what it is doing. Programmers (like me) do that for a living. The only difference is that the articles spell out exactly how it is verified: "Consider variables A and B. Note that at every point A<B. Now, also note that every iteration through this loop decreases B. . . ." Programmers make observations like this constantly. But that is not a general formal method of verifying programs. Each step is a true Mathematical fact, of course. But a general method for determining the observations and facts (e.g. as described in the above hypothetical example) is what is needed and is missing. [ This actually brings up a good point that helps to explain why they have not succeeded in developing a general means of Program Verification or Program Synthesis. The individual commands and arguments of a program are not a reflection of the logic that is used to create a program that meets the given specification. They are the implementation of parts of the algorithm that is being used to satisfy that spec. In other words, a programmer does not conclude that he has to first initialize A to 0, then figures out what he has to do next to A or other variables etc. He determines higher level processes that must be done. For example, he may decide to (1) set A equal to the maximum array subscript defined, then (2) find the sum of the array element, etc. The first command was not constructed to solve the original problem, but rather to solve the first subproblem. Then any verification of the program needs to show the higher level processes that occur (1 and 2.) We need to address the logic of the program at a higher level. This is what has been missing from attempts to formalize Program Analysis since the 1950's. And in fact we don't ever have to consider the individual commands, bur rather individual subroutines that are known by axioms or inference to produce a particular functionality. That is how CBL synthesizes computer programs (as illustrated repeatedly in my ARXIV paper.) ] > From this follows that one can in theory also > do programm synthesis: > > Just generate programms and pick those > that you proofed termination and correctness. > > But there are some interesting approaches in > inductive logic programming to do synthesis. > Try googling the terms "machine learning" and > "inductive logic programming". But nobody has published a general method for doing that. If you think that I am wrong, then please give the general rules and show a few simple examples of programs formally generated or verified using these rules to illustrate that. The examples can be trivial programs, as long as they are all formally generated or verified by the same set of general rules. C-B > Bye > > 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. > > > > 4. Incompleteness in Logic: A formal derivation of Godel's > > Incompleteness theorems or Rosser's improvement or Smullyan's Dual > > Form theorem. > > > > Any formalization would include: > > > > A. A formal statement of the theorem or result. > > B. The meaning of any such statement. > > C. How A corresponds to the statement of the theorem. > > D. An algorithm for generating formal statements such as A. > > E. A demonstration that D generates A. > > F. A demonstration that D generates only true statements. > > > > Curry-Howard, Manna/Waldinger, Boyer/Moore, Modal Logic, Prologue and > > TPTP all attempt to do this, but nobody has ever shown any examples of > > anything near A-F. > > > > Would we say that formalization is the ultimate goal of every branch of > > Computer Science? What problem is not enhanced when expressed > > formally? > > > > C-B > > |