Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 18 Sep 2006 03:24 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. With respect, Steven
From: Steven Zenith on 18 Sep 2006 03:29 Charlie-Boo wrote: > How about zero times the square root of 2? That is an interesting case. And the answer in practice will be, it depends (an optimizer may remove the expression, an interpreter may disregard the function root 2 - all on the basis of the zero). But the answer formally is no, it does not terminate - because the function that computes the root of 2 does not terminate. With respect, Steven
From: Steven Zenith on 18 Sep 2006 03:32 Charlie-Boo wrote: > Steven Zenith wrote: > > > I have referred you to the relevant literature that more than > > adequately explains the formalism and methods of transformation. > > No it doesn't. It is your responsibiity to prove your point. It is not my responsibility to do your work for you. Following references is a well established and practical convention. I simply do not have the time to teach you. With respect, Steven
From: Steven Zenith on 18 Sep 2006 03:39 Charlie-Boo wrote: > Steven Zenith wrote: > > > 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? > > Do you understand how to calculate real number arithmetic to an > arbitrary number of decimal places? Are you aware that floating point units exist and that most language libraries use the standards that they implement? None of them do real number arithmetic and over the years those standards have changed. They will again. You are boring me now. With respect, Steven
From: Steven Zenith on 18 Sep 2006 04:24
Charlie-Boo wrote: > Every programming language can implement a function to calculate square > root to a given number of places. It has nothing to do with > "performance constraints". I used a function that calculates the root of 2 as a simple example of a formally non-terminating function. The root of 2 is not a real number, so in most languages direct use of the number would formally produce a type error, so the function would need to produce a real number approximation to be type compatible. Formally, such a number would require a pragmatic, by convention it would be to some number of decimal points. I did then observe that even if we picked a number of decimal points, either implicitly or explicitly, there was no guarantee that the value could be computed on any computer - and you would require a formal specification of the particular platform to know. Now we live today with wide standardization so this issue may not be as clear today as in the 1980's when there was greater diversity in computer architecture. Whatever. You still need a formal specification of the platform to verify that one can map to the other. Your informal approach to this is not sufficiently rigorous. If you choose, as you suggest, to implement root 2 in a particular way I would have to ask you if that way meets the pragmatic understanding of the programmer - an arbitrary selection of precision may not be compatible with the programmer's expectation. That's why a formal pragmatics is something that should be known to programmers - or should be specified by programmers. The trouble is, few programmers can predict the behavioral implications of such a pragmatic. The fact that this function is trivial example is not the point here - it raises important questions. I previously mentioned that I have considered that a continuing fraction representation may be a practical solution - but this requires a math unit able to manipulate all operations as continuing fractions and almost all non-trivial results will end up irrational. Which is a definite issue with the solution. For an explanation of termination and other properties of formal interest see Bill Roscoe's book on the theory and practice of concurrency. http://www.amazon.com/Theory-Practice-Concurrency-W-Roscoe/dp/0136744095/sr=1-2/qid=1158566763/ref=sr_1_2/002-2129589-0385604?ie=UTF8&s=books It should be at a library near you. And that, I fear, is all the time I have to spare on this issue. With respect, Steven |