Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 16 Sep 2006 11:09 Steven Zenith wrote: > Charlie-Boo wrote: > ... > > Sorry, but I seriously doubt that you can. Feel free to prove me > > wrong. > > Read the literature I have referred to - which is readily available. You are not substantiating your claims, but rather are asking others to do so for you. [ Personally, I have been researching and reading about these topics for more years than I would like to admit. And none of what I have read accomplishes a formalization of any branch of Computer Science. I listed a half dozen approaches that have failed in my OP. ] If you do not substantiate it, then it is only speculation with no Mathematical significance. Here is your forum. You have used this forum to make grandiose claims. But you have declined to give any examples or details to support those claims. What should any reasonable, fair-minded person conclude? C-B > With respect, > Steven
From: Charlie-Boo on 16 Sep 2006 11:18 Steven Zenith wrote: > Charlie-Boo wrote: > > > Why do you say that I need to read "some of it"? > > Because "some" is better that "none." How do you know that I have read none of it? First you make unsubstantiated technical claims, and now you make an unsubstantiated personal attack. This is even worse, because now you are attacking the messenger. If you think that I have not read it because it contains the solution that I seek, then you have to show that a solution does in fact exist. You have not done so. You have many words claiming success at solving these problems, but are silent on substantiating these claims. C-B > With respect, > Steven
From: Charlie-Boo on 16 Sep 2006 11:25 Steven Zenith wrote: > Charlie-Boo wrote: > > > > I'm afraid you're confusing concepts. Programs terminate or not. > > Functions are defined or not. A function that maps to the square root > > of 2 is defined, just as one that maps to 3 is. It is not a > > "non-terminating function". > > Indeed, however, I was talking about the property of termination, not > definition. 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 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. In fact, a program could easily represent the square root of two with a discrete finite structure. Programs like Mathematica do exactly that. C-B > With respect, > Steven
From: Charlie-Boo on 16 Sep 2006 11:36 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. > Such behavior maybe irrelevant in practice. In Microsoft Excel it *may* > not present a problem. OTOH if you are doing something economically > critical, like computing the trajectory of a space vehicle, then it > may. This highlights the need for a distinct formal pragmatics that can > be applied to each instance of a formally specified program. Economics has nothing to do with theoretical Computer Science. > This non-terminating property of computing irrationals has implications > in the foundations of mathematics and the question of what is > computable - especially as it relates to the pragmatic aspects of > applied conventional mathematics. There is no finite decimal expansion of 1/3 either. This is a function of the base (system of notation) being used, not an inherent property of the number. In base 3 it is .1 a finite representation. C-B > There are clearly many conventionally > defined functions, any that include or produce irrationals, that do not > formally terminate. > > This all assumes that the terminating properties of programs in > computer science are properties that are interesting formally - I'd > suggest that they are. The issue can, perhaps, be glibly ignored by > mathematics, but it certainly cannot be ignored by a formal > consideration of computer or computational science. > > With respect, > Steven > > -- > Dr. Steven Ericsson-Zenith > IASE, Sunnyvale, California
From: Charlie-Boo on 16 Sep 2006 11:49
Steven Zenith wrote: > Charlie-Boo wrote: > > > The truth of the matter is, there are all sorts of people claiming to > > have formalized various parts of CS, but none of them carries any > > weight - simply because they don't show how to crank out results using > > a set of formal rules. That's what formalizing is all about. > > This is simply wrong, I have already referred you to examples. > > Start here: > > http://web.comlab.ox.ac.uk/oucl/publications/prgtr/index.html You refer to instances of people manually verifying one program, not a set of rules that verifies programs in general (with examples of how it works with specific problems.) > Now I get it. CBL is "Charlie Boo's Language" - so this entire > discussion is some propaganda exercise. I wish I had spotted that > earlier. No it isn't. It stands for "Computationally Based Logic." You just stated that, "INMOS and Oxford shared a Queens Award for Industry. The proof was actually performed by a colleague of mine. Now I have no time for such awards myself." and then accuse ME of propagating propaganda? Besides the fact that these assertions contain zero Mathematical significance. Just give the rules and some examples as to how they successfully solve the problem, ok? Otherwise you are making empty claims. C-B > There are, BTW, several theorem provers around that are used in > hardware verification - especially see Mike Gordon's HOL (High Order > Logic), which is available in Open Source. > > See: > http://www.cl.cam.ac.uk/~mjcg/ > > Sincerely, > Steven |