Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 17 Sep 2006 15:06 Charlie-Boo wrote: > Steven Zenith wrote: > > > 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." > > That is not a complete English sentence. It is "If ..." with no > conclusion, nor a subject and verb to make it an English sentence. Apologies the "if" is a typographic error, a remnant. Steven
From: Steven Zenith on 17 Sep 2006 15:13 Charlie-Boo wrote: > You are continuing to confuse abstract functions with concrete > programs. Whether f(x) equals 2 or the square root of 2 is immaterial > as far as functions are concerned. The function is defined in either > case. The square root of 2 is a specific mathematical object, not a > process that terminates or not. My apologies, I thought that you were talking about formalizing computer science. In computer science the specification of such functions are constrained by pragmatics. In computer science programs executing such functions have desirable formal properties - termination is one of them. With respect, Steven
From: Steven Zenith on 17 Sep 2006 15:16 Jack Campin - bogus address wrote: > > 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. > > You seem to be thinking of conventional imperative implementations. > There's nothing very implementation-specific about a lazy functional > version of square root - it will generate as many places of precision > as the caller asks for, and you need know nothing about the hardware > or the compiler technology to know what answers you'll get. That is a fair observation. What do you plan to do with your arbitrary precision value of root 2 when you have it? Are you going to use it in an operation? If so, will you be able to maintain the specified accuracy? With respect, Steven
From: Steven Zenith on 17 Sep 2006 15:31 BTW: That root 2 does not terminate - is not computable - is an issue in pure mathematics and the foundations of mathematics also since no formula that uses the root of 2 is strictly computable. Sincerely, Steven
From: zzbunker@netscape.net on 17 Sep 2006 22:24
Charlie-Boo wrote: > zzbunker(a)netscape.net wrote: > > 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. > > > > Programs that output themselves are quite trivial, > > since it's what the assembler instruction NOP does, > > > > Which isn't the same thing as programs that > > copy themselves. > > You are proving that there is a programming language in which there is > a program that outputs itself, but the theorem is that there is such a > program in all programming languages (C++, Algol, et. al.) Well, for the theorem even to make sense, you have to define "all programming language" better than just a recurive language. Since that's nothing but Peano Axioms. And you can easily prove that in the Peano System, since it has no axioms of comphrension. > > C-B > > > > 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 |