Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 14 Sep 2006 12:34 Rupert wrote: > 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. The merit in being completely formal is that it accomplishes the above. C-B
From: Charlie-Boo on 14 Sep 2006 12:47 Snis Pilbor wrote: > 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. Does that provide a formal means of creating those results (as I asked for)? > 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. That's only because Dedekind didn't come up with a very good formalization. Consider: Finite set {true, false} Infinite set N = {0 , 1, 2, 3, . . .} Operator => : Map from one set to another. Then we can formally define: Natural Numbers: N Rational Numbers: {true, false} => N Real Numbers: N => {true, false} Since we need the above concepts anyway (in lots of contexts), then formalizing the Rational Numbers and the Real Numbers this way is done without adding ANYTHING to our system. As Occam would be happy to see, we merely used existing principles. Now isn't that better? We also find greatly simplified proofs using CBL e.g. the proof (one of many, actually) of Rosser's 1936 extension to Godel's 1931 paper: "If an axiomatic system is consistent and complete, then the refutable sentences coincide with the unprovable ones, but the former set is r.e. while the latter is not." Have you ever seen such a simple proof of Rosser's result? > 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. But do you have a formal system for generating Recursion Theory theorems? C-B
From: Charlie-Boo on 14 Sep 2006 12:56 abo wrote: > 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. What is your definition of Programming Language? C-B
From: abo on 14 Sep 2006 13:29 Charlie-Boo wrote:> > What is your definition of Programming Language? I don't have one. You see, I can know how to use a word or word grouping without coming up with a definition. So I am able to say whether such and such is a programming language, and based on this I can telll that your claim that "All programming languages are..." is false, using the standard meaning.
From: Steven Zenith on 14 Sep 2006 13:38
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 |