Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Rupert on 14 Sep 2006 07:00 Charlie-Boo wrote: > Rupert wrote: > > Charlie-Boo wrote: > > > Do we all agree that Computer Science definitely should be formalized? > > > > > > > What's the merit in being completely formal, for any branch of > > mathematics? Surely it's enough to convince ourselves that we could > > formalize it. > > Why develop mathematics? > Because it's interesting. > Why have people axiomatized branches of mathematics? > To clarify the foundations of the reasoning. > Is it better to have a single representation for a theorem rather than > many equivalent representations? > Not clear to me why one should be better than the other. > C-B
From: Snis Pilbor on 14 Sep 2006 09:16 Charlie-Boo wrote: > 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. > The fields you've quoted have been studied using ZF and/or ZFC. To go deeper than that would strictly weaken the results: the results are true (if anything is true) in any set theory which satisfies ZF[C], whereas a derivation from nothing but basic logic would only show the results to be true in that specific logic. Here's an analogy. Suppose we want to make elementary calculus more rigorous. So instead of talking about "real numbers", we talk strictly about Dedekind cuts. The work becomes vastly more difficult, but we manage to pull it off. What have we gained? Nothing. The original work was true for any ordered field, and what we've now bought at such a steep price, is only true of Dedekind cuts, and we'll have to start all over again for equivalence classes of Cauchy sequences. The recursive function theory I have studied is true whether I define 0=emptyset, 1={0}, 2={1}, etc., or whether I define 0=the moon, 1={0}, 2={1}, etc., or even if I define 0=emptyset, 1={{0}}, 2={{1}}, etc. This phenomenon is called "abstraction" and it, far more than pedantic formalism, is the real virtue of mathematics.
From: Charlie-Boo on 14 Sep 2006 11:10 Alec McKenzie wrote: > "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. How do you define "Programming Language"? That's why we differ (I assume i.e. that you would agree using the same definition as I.) C-B > -- > Alec McKenzie > usenet@<surname>.me.uk
From: abo on 14 Sep 2006 12:14 Charlie-Boo wrote: > Alec McKenzie wrote: > > "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. > > How do you define "Programming Language"? That's why we differ (I > assume i.e. that you would agree using the same definition as I.) Yes well one could define 'programming language' to mean "tooth fairy". But in fact 'programming language' has a good standard meaning which people use all the time. If you're going to insist on using a non-standard meaning, maybe you should make up words instead - instead of using 'programming language' use 'gobble'. This will prevent confusion.
From: Charlie-Boo on 14 Sep 2006 12:28
Steven Zenith wrote: > 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. Not sure what you mean. I would say that the "context" is any system that purports to formalize any branch of Computer Science, in particular, Program Synthesis, Theory of Computation, Recursion Theory or Incompleteness in Logic (Proof Theory.) I am saying that within any such system there should be a formal statement of each theorem or result that it formalizes (A) etc. Is this not a meaningful assertion? Is it true (for A-F)? > 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? Expressions concerning the relation "Program X computes mathematical object Y." For example, X => Y is Program Analysis. Y => X is Program Synthesis. X,Y => {true, false} is Program Debugging. X => X is Recursion Theory. [I am sparing you the toil of seeing this formally expressed in CBL.] It is not just properties, but rather algorithms in general. As I formalize above, we need algorithms to determine the mathematical object computed by a given program, or the programs that compute a given mathematical object, or whether a given program computes a given mathematical object etc. Computer Science is actually even more general than that, as we consider systems other than Turing Machine equivalents. The complete relation is P=Q(M) for relations P,Q and individual M. What you describe is Q being "Program X halts yes on input Y" and M is a computer program. Then P is the set of inputs on which M halts yes. We also consider Q being "Wff X with Y substituted for its free variables is provable." and "Wff X with Y substituted for its free variables is true." etc. > 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? My OP refers to a general method of formally producing Computer Science results, not a single instance that is manually created. > 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. I use Predicate Calculus extended by interpreting unquantified variables I, J, K as being input and X, Y, Z as being output. For example, if FAC(a,b) means "a is a factor of b", then we have: FAC(X,I) : List the factors of a given number. FAC(I,X) : List the multiples of a given number. FAC(I,J) : Is one given number a factor of another? (eA)FAC(A,I,) : Does a given number have any factors? (eA)FAC(A,X) : List all numbers that have a factor. ~(eA)FAC(A,X) : List all numbers that have no factors. This also succinctly formally represents Database Queries e.g. "List all employees whose salary is greater than their manager's." Did INMOS consider this approach? > 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. That is a subset of Program Synthesis. For example, if a program computes the sum of two inputs, then it must terminate. Any program that always terminates computes some total function, of course. > 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. I have asked to be informed of A-F for purported formal derivations of results of Computer Science. Could you please inform me of what A-F has been developed? (I listed several efforts in the OP that I described as not being authentic. I am aware of the claims. I am looking for an authentic one.) The difference here is not whether one is aware or unaware of what people are writing. It is whether one believes that they have solved the problem as advertised. This begins with ones criteria for a solution. I give A-F as criteria. What were their criteria? What are yours? Do you believe that A-F are reasonable criteria for what constitutes a formalization of a branch of Computer Science? And did they consider Theory of Computation? Recursion Theory? Proof Theory? All of these use the same principles. (In CBL they use the same Rules of Inference.) Again, for any result to be formalized we should have: 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. > It is not that these projects did not produce compelling results - we > did, and to international acclaim What is the significance of "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. Can you show an example of a specific useful technique that they developed that would help software engineers? In my ARXIV paper I show how my methodology creates useful programs (e.g. determine if one number is a factor of another, and list all employees who earn more than their manager) as well as Theory of Computation th |