Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 19 Sep 2006 12:26 Patricia Shanahan wrote: > Don't forget the possibility of symbolic mathematical languages, in > which numbers like the square root of 2 have representations and can be > used in expressions. Here is a fragment of a Matlab session: As I said, it depends. With respect, Steven
From: Steven Zenith on 19 Sep 2006 12:38 Patricia Shanahan wrote: > Steven Zenith wrote: > > Charlie-Boo wrote: > > > >>> 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. > >> You said (about 10 times) that the function doesn't terminate. How > >> do you define a function terminating? > > > > Perhaps I was unclear. A function terminates when it produces a result > > (and one might possibly add "and performs no further action"). > > > > In CSP/Occam, it is when any construction is complete (i.e., computed) > > or it could be stated as when any subsequent behavior in the trace of > > the function is SKIP, not STOP. > > I think you and Charlie-Boo are using the same term, "function", for two > very different things. I am using the term function in the computer science sense since the question has to do with the formalization of computer science and we are discussing functions in programs. In any case, a computer science function and a function in the mathematical sense (a map) are formally equivalent in that a CS function is the map of the arguments to the results. Formally, all functions should be side effect free. Whether in a mathematical equation or a computer program, functions that actually compute contributing values to a result have terminating characteristics. Yes, I understand that one can represent the root of 2 symbolically, but in practice we do not and instead we tolerate rounding errors. With respect, Steven
From: Steven Zenith on 19 Sep 2006 12:42 Charlie-Boo wrote: .... > > Formal methods in computer science and electrical engineering have been > > used extensively, and continue to be used (esp. in EE), in the > > verification that certain transformations are consistent: specification > > - software implementation - platform, for example. I gave a clear > > example of work completed in the late 1980s, by a team of which I was a > > member, in which the implementation of a floating point unit was > > formally shown, proven, to meet the specification of the IEEE standard. > > We already went through this. You are talking about individual > problems that were supposedly solved manually using formal means - > like a Mathematician proves a theorem. Computer Programmers make > formal deductions concerning programs all day. But they don't have a > method of automating those conclusions (other than CBL if they read > Google Groups.) > > I am talking about a formalization of not one process, but entire > branches of Computer Science. I apologize if I was not sufficiently clear. This proof was an example of a general technique and the formal tools we had available. With respect, Steven
From: Steven Zenith on 19 Sep 2006 12:59 Charlie-Boo wrote: .... > I'm talking about Computer Science, ok? I listed 4 branches: Program > Synthesis, Theory of Computation, Recursion Theory and Incompleteness > in Logic. (For that last one, maybe I should call it Computing > Science?) This seem to me to be a very incomplete view. You have not mentioned computer architecture or typing theory - which reveals much of the reason you are having problems, since you do not appear to appreciate that real programs are typed do not use real numbers and execute on machines that have varying architectures. When you say "Program Synthesis" I assume you mean transformation from one language into another by a process of formal equivalence. I think you should leave Godel out of it. With respect, Steven
From: stephen on 19 Sep 2006 13:22
In sci.math Steven Zenith <stevenzenith(a)gmail.com> wrote: > Patricia Shanahan wrote: >> Steven Zenith wrote: >> > Charlie-Boo wrote: >> > >> >>> 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. >> >> You said (about 10 times) that the function doesn't terminate. How >> >> do you define a function terminating? >> > >> > Perhaps I was unclear. A function terminates when it produces a result >> > (and one might possibly add "and performs no further action"). >> > >> > In CSP/Occam, it is when any construction is complete (i.e., computed) >> > or it could be stated as when any subsequent behavior in the trace of >> > the function is SKIP, not STOP. >> >> I think you and Charlie-Boo are using the same term, "function", for two >> very different things. > I am using the term function in the computer science sense since the > question has to do with the formalization of computer science and we > are discussing functions in programs. In any case, a computer science > function and a function in the mathematical sense (a map) are formally > equivalent in that a CS function is the map of the arguments to the > results. No, they are not formally equivalent, as there exist uncomputable functions. A mathematical function is a mapping from one set to another set. Not all mappings are uncomputable. The Halting Function is the classic example. There is no computer science function that is equivalent to this mathematical function. Stephen |