Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 13 Sep 2006 20:53 Alec McKenzie wrote: > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > Alec McKenzie wrote: > > > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > > What do you call a system that contains a representation for every > > > > recursive function? > > > > > > I would not dream of trying to call it anything. Does it have > > > some bearing on programs that output themselves? > > > > Yes. It is what is often called a "Base of Computing" or a > > "Programming Language", and is the context in which we can show there > > is a program that outputs itself. > > > > Actually, using CBL we can see the exact sufficient condition that a > > Programming Language meets: Substitution is recursive. > > > > A. Let M # f(I) mean program M outputs the value of function f applied > > to input I. > > > > B. Define function s11(I,J) as M # f(I) => s11(M,N) # f(N). (S11 > > substitutes a constant J for the single input variable in program I.) > > > > C. Let f(I) mean f is recursive. Then the axiom is s11(I,J), > > substitution is recursive. > > > > D. By definition, we have f(I) <=> (eM) M # f(I) > > > > Thm. N # N There is a program that outputs itself. > > 1. s11(I,J) Axiom C - Substitution is recursive. > > 2. s11(I,I) Subtitution, 1 > > 3. M # s11(I,I) Rule D, 2 > > 4. s11(M,M) # s11(M,M) Rule B, 3 > > 5. N # N Substitution, 4 > > qed > > > > And of course the real test of the validity of any formal system is its > > ability (or inability) to generate lots of useful theorems, both known > > and new. CBL can prove not just the existance of a self-outputting > > program, but also the Fixed Point theorem, the Recursion theorem, and > > more complex theorems involving multiple functions and conclusions - > > i.e. Recursion Theory. For example, if f(I) and g(I) then there is an > > M,N such that M # f(N) + N # g(M). > > I see you are back to the existence of "*a* self-outputting > program", the proof of which is trivial (i.e. a single example > will do it). No, you have to prove the program exists for every programming language, not just one. > Why you should need CBL to generate a "useful > theorem" of that kind?. CBL proves it and a whole slew of other theorems from Recursion Theory. People argue over the exact conditions under which Godel's theorems apply, or what is The Fixed Point Theorem vs. The Recursion Theorem. CBL gives exact answers to these questions. C-B > -- > Alec McKenzie > usenet@<surname>.me.uk
From: Snis Pilbor on 13 Sep 2006 22:30 Charlie-Boo wrote: > Do we all agree that Computer Science definitely should be formalized? > I'm not certain what you think is still in need of formalizing. At least the books I've read (which are aimed at mathematicians, not computer scientists) are perfectly rigorous. Most books will liberally use the Church Thesis to avoid hashing out explicit proofs that functions which are obviously effectively computable are recursive--- but this is harmless because in each such case any monkey could write the proof, but it would be exceedingly tedious and ugly and boring--- and even if you aren't happy with this, older books even go through these details explicitly. And let me tell you -- it's UGLY. Ever read an advanced math text? Ever read a stranger's sourcecode? Imagine combining the worst parts of both worlds. The only nonrigorous comp sci I've run into was "geometric algorithms", where they implicitly assume lots of nontrivial topological facts like Jordan curve theorem. But if you would write a fully rigorous geometric algorithms textbook, it would require a Ph.D. in topology to understand. And anyone with that level of training can just look at a nonrigorous geometric algorithms book and fill in the details anyway. As a matter of fact, there's much overlap between comp sci and logic, where you often find the most pedantic mathematicians of all! (I love logic:)
From: Charlie-Boo on 14 Sep 2006 00:56 Snis Pilbor wrote: > Charlie-Boo wrote: > > Do we all agree that Computer Science definitely should be formalized? > I'm not certain what you think is still in need of formalizing. All of Computer Science - Program Synthesis, Theory of Computation, Recursion Theory, Incompleteness in Logic. None of the theorems are generated by an axiomatic system - despite the best efforts of Mathematicians (e.g. Hilbert) and Logicians (e.g. Godel.) The development of mathematics towards greater exactness has, as is well-known, lead to formalization of large areas of it. But this is not so of Computer Science. > At > least the books I've read (which are aimed at mathematicians, not > computer scientists) are perfectly rigorous. Do you know of any system that systematically created more than one theorem from Computer Science? (I say "more than one" when in fact the truth is they haven't mechanically generated anything. But if you want to quote papers, then they will sometimes claim to have generated one famous theorem, but even they don't claim their system generates more than one. In other words, you don't have to just do better than what they do, you have to do better than what they claim - because people will cite a paper that is only attempting to do something as an example of "It's already been done before." But they don't even try to claim to have produced a multitude of famous (significant) theorems from one branch of Computer Science from one system.) It is quite sad. They write BS papers and when someone does solve the problem, they say "It's been done before.", but have no explanation as to why what is written really does solve the problem. The standard is, if it has been published, then it is true and they solved every problem that they described as being what they were trying to solve. It is so pathetic. The result is that Computer Science has been stuck in the mud for decades. I read a book, something like, "Formal Programming in the 1990's" in a bookstore once, and the entire book did not contain a single example of a program being created or analyzed using formal methods. Pitiful. Would you like a system that mechanically created the theorems that you studied, and more? > Most books will liberally > use the Church Thesis to avoid hashing out explicit proofs that > functions which are obviously effectively computable are recursive--- > but this is harmless because in each such case any monkey could write > the proof, but it would be exceedingly tedious and ugly and boring--- > and even if you aren't happy with this, older books even go through > these details explicitly. And let me tell you -- it's UGLY. Ever > read an advanced math text? Ever read a stranger's sourcecode? > Imagine combining the worst parts of both worlds. Ever followed my description of CBL? Why not? Then how can you say that what I am talking about has the negative properties that you describe? http://groups.google.com/group/sci.logic/msg/72ad665ae0b5e28a?hl=en& > The only nonrigorous comp sci I've run into was "geometric algorithms", > where they implicitly assume lots of nontrivial topological facts like > Jordan curve theorem. It wouldn't be Mathematics or Computer Science if it weren't rigorous. Books that explain famous theorems for the general ("retail") audience can be incomplete or informal, but that is not really Mathematics or Computer Science - and would never do as the original proof of the theorem. I am simply talking about a system that creates these results using exact rules. That is what axiomatic systems do. That is the goal of any reasonable Mathematician, and of any proficient Logician. Mathematicians would never get away with what Computer Scientists do. Can you imagine Chaitin's grandiose claims ever appearing in a respectable journal of Mathematics? > But if you would write a fully rigorous > geometric algorithms textbook, it would require a Ph.D. in topology to > understand. And anyone with that level of training can just look at a > nonrigorous geometric algorithms book and fill in the details anyway. > > As a matter of fact, there's much overlap between comp sci and logic, > where you often find the most pedantic mathematicians of all! (I love > logic:) Great! And CBL shows us exactly what that overlap is. An axiom of logic is an assertion (wff) known to be true. (People who consider arbitrary axioms are exploring the possibilities that go outside of meaningful axiomatic systems.) An axiom of Computer Science is a wff whose value can be calculated. Do you see the relationship? Do you see that the Computer Science axiom is a generalization of the axiom of logic? C-B
From: Steven Zenith on 14 Sep 2006 04:06 Charlie-Boo wrote: > I am very interested in any examples of this. Can you give one, > including: > > 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. I encourage you to review the sources I mentioned - these questions of yours are meaningless without context. The Oxford Programming Research Group - now under Bill Roscoe - has done extensive work in this area. I am most familiar with their work but this type of effort is expanded elsewhere. At least look at Bill's book on the subject. What are the important properties of computer programs that you wish to develop theorems and proofs for? Do you know? At INMOS in the 1980s the team I was a part proved that the implementation of the IEEE floating point standard on the Transputer microprocessor met the formal specification of that standard. For such standards, proofs of such transformations would appear to be "meaningful", would they not? Today, however, it is hard to find a standard with an adequately formal specification - so start right there perhaps. I've tried, you won't get much sympathy from me. Roscoe and others dealt with desirable properties of programs in general, such as proofs that programs terminate or are deadlock free. The result are in the literature. Roscoe, Goldsmith and others in a company called Formal Methods Inc. built tools of program transformation so that programs could be mapped to implementation architectures. I simply think that you are poorly informed - and need to review the literature to identify which properties of computer programs are interesting - and I've pointed to only a few. It is not that these projects did not produce compelling results - we did, and to international acclaim - it is that it demands a level of engineering discipline today that - for one reason or another - software engineering has not been prepared to accept and is now simply absent. The problem is one of business economics. A quick and dirty solution today for which I can charge endless consulting fees to maintain, versus the up front one time cost and lengthy process of deliberate and well considered implementations using tools that ensure the rigor that you seek. The other issue is pragmatic. You can't do any of this with today's mainstream programming languages because you need languages with a mathematical basis - like the languages we used and one in particular, to which I was a principal contributor, Occam - a language based on the process algebra of CSP devised by Tony Hoare. This means that we have to re-educate programmers. I tried to sell that horse in the 1980s. We fully expected programmers to become logicians, not undisciplined hackers capable of navigating the inspired sloppiness of others. Tell me things can change. Sincerely, Steven > > What I have discovered is that the manner in which these problems are > formulated is faulty, resulting in a lot of energy being spent (as you > describe) wasted. > > For example, much work has been spent trying to construct programs by > building the flowchart. This is at the wrong level of abstraction. > The details are unimportant - only the fact that the program as a > whole computes a particular result is relevant. Working at this higher > level of abstraction, we can manipulate programs as units, rather than > trying to make sense out of their internal structure. > > Similarly, in Proof Theory the characterization of relations using > systems of logic has focused on particular bases for that > characterization: expressible, representable, contrarepresentable. > However, what is needed is a more general model in which the base is a > variable. > > > I am personally aware of a number of proofs that illustrate interesting > > formal properties of programs - including properties such as deadlock > > freedom and that programs meet their specifications - and of the tools > > that enabled the demonstration of same. > > > > That these tools have not continued to be widely developed, have only > > had limited availability and have not been broadly applied is, frankly, > > deplorable. > > It is because nobody has ever shown these approaches to produce > anything. Give a single simple example of solving a programming or > theoretical problem using formal methods as taught in universities. > (Note A-F above.) > > C-B > > > With respect, > > Steven > > > > -- > > Dr. Steven Ericsson-Zenith > > IASE, Sunnyvale, California
From: Alec McKenzie on 14 Sep 2006 05:05
"Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > > > I see you are back to the existence of "*a* self-outputting > > program", the proof of which is trivial (i.e. a single example > > will do it). > > No, you have to prove the program exists for every programming > language, not just one. Which cannot be done, since the program does *not* exist for every programming language, as can be very easily shown. -- Alec McKenzie usenet@<surname>.me.uk |