Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Patricia Shanahan on 18 Sep 2006 12:08 Steven Zenith wrote: > 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. Floating point arithmetic, despite its great practical utility, is of little or no relevance to the limits of computability, because every floating point number is a rational number. It is normal to assume we have an unbounded range integer representation, like java.util.BigInteger. Given that, any rational, including any floating point number, can be exactly represented as an ordered pair of integers. Even if you only assume arbitrary length decimal fractions, every floating point unit I've seen has had either radix 10 or a radix that is a positive integer power of 2, such as 2 or 16. Any number that has a finite length representation in any of those systems also has a finite length decimal fraction expansion. Patricia
From: Chris Menzel on 18 Sep 2006 15:21 On Mon, 18 Sep 2006 13:56:36 GMT, Patricia Shanahan <pats(a)acm.org> said: > 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. > > In mathematics, a function is a relation between elements of its > domain and range, such that each element of the domain relates to > exactly one element of the range. It is quite meaningless to talk > about terminating or not terminating for a mathematical function. I > think that is what Charlie-Boo means by "function". > > On the other hand, in some programming languages, "function" means a > subprogram that, if it terminates, produces a result, not just side > effects. Is that what you mean by "function"? > > The two are related, because a function (subprogram) is the natural > representation in a computer program of a recursive function > (mathematics). However, the subprogram sense includes non-terminating > subprograms that do not implement a mathematical function. The class of recursive functions includes partial functions, which correspond to programs that fail to terminate on some inputs. Maybe I'm misunderstanding you, but you seem to be denying this.
From: Patricia Shanahan on 18 Sep 2006 16:11 Chris Menzel wrote: > On Mon, 18 Sep 2006 13:56:36 GMT, Patricia Shanahan <pats(a)acm.org> said: >> 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. >> >> In mathematics, a function is a relation between elements of its >> domain and range, such that each element of the domain relates to >> exactly one element of the range. It is quite meaningless to talk >> about terminating or not terminating for a mathematical function. I >> think that is what Charlie-Boo means by "function". >> >> On the other hand, in some programming languages, "function" means a >> subprogram that, if it terminates, produces a result, not just side >> effects. Is that what you mean by "function"? >> >> The two are related, because a function (subprogram) is the natural >> representation in a computer program of a recursive function >> (mathematics). However, the subprogram sense includes non-terminating >> subprograms that do not implement a mathematical function. > > The class of recursive functions includes partial functions, which > correspond to programs that fail to terminate on some inputs. Maybe I'm > misunderstanding you, but you seem to be denying this. > I use "function" as synonymous with "total function". Perhaps I should have put the word "total" in front of each use of "function". I make the same distinction for partial functions. A partial function in mathematics is a relation that associates at most one value in its range with each element of its domain, rather than exactly one. An algorithm for evaluating the partial function would fail to terminate on some inputs in the domain, but the function itself neither terminates nor fails to terminate, because it is a relation, not an algorithm. Patricia
From: Chris Menzel on 18 Sep 2006 17:24 On Mon, 18 Sep 2006 20:11:33 GMT, Patricia Shanahan <pats(a)acm.org> said: > Chris Menzel wrote: >> On Mon, 18 Sep 2006 13:56:36 GMT, Patricia Shanahan <pats(a)acm.org> said: >>> 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. >>> >>> In mathematics, a function is a relation between elements of its >>> domain and range, such that each element of the domain relates to >>> exactly one element of the range. It is quite meaningless to talk >>> about terminating or not terminating for a mathematical function. I >>> think that is what Charlie-Boo means by "function". >>> >>> On the other hand, in some programming languages, "function" means a >>> subprogram that, if it terminates, produces a result, not just side >>> effects. Is that what you mean by "function"? >>> >>> The two are related, because a function (subprogram) is the natural >>> representation in a computer program of a recursive function >>> (mathematics). However, the subprogram sense includes non-terminating >>> subprograms that do not implement a mathematical function. >> >> The class of recursive functions includes partial functions, which >> correspond to programs that fail to terminate on some inputs. Maybe I'm >> misunderstanding you, but you seem to be denying this. > > I use "function" as synonymous with "total function". Perhaps I should > have put the word "total" in front of each use of "function". Then I'm a bit confused, as you say that a subprogram is the natural representation in a computer program of a recursive function, and you acknowledge in the preceding paragraph that a subprogram might not terminate. For that to make sense, "recursive function" has to include partial functions. > An algorithm for evaluating the partial function would fail to terminate > on some inputs in the domain, but the function itself neither terminates > nor fails to terminate, because it is a relation, not an algorithm. Well, obviously, but failure of termination in the algorithm on some inputs corresponds exactly to partiality in the corresponding function. Obviously they are different things, but it seems to me you're driving a bigger wedge between the two notions than is warranted by the context by restricting the notion of "function" to total functions. If you allow "function" to include partial functions, the correlation between the two is quite direct.
From: Charlie-Boo on 19 Sep 2006 08:10
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 > See: > http://www.cl.cam.ac.uk/~mjcg/ > > Sincerely, > Steven Thanks for the links, but honestly, they lead to either broken links or descriptions of systems without any examples of a result from Computer Science being formally generated. Can you give a single example of a result from Computer Science that is formally represented and generated? That is what I mean by a formalization of Computer Science. That is what CBL does. It represents and derives: 1. incompleteness results (Godel 1931, Rosser 1936, Smullyan 1960-2000) 2. Recursion Theory (Kleene 1950's - existance of a self-outputting program, the Fixed Point Theorem, the Recursion Theorem, and the more involved Double Recursion theorems of Smullyan), 3. Program Synthesis (Number Theory functions and Database Query Processing) 4. Theory of Computation (Turing 1937 and variations.) If anyone is interested in any particular branch of Computer Science of these 4, I will give an overview of its axioms and rules. If interested in a particular theorem, I will show in exact complete detail how it is represented and formally derived from these axioms and rules. For example, Turing's Unsolvability of the Halting Problem (and many variations) is derived from the Theory of Computation axioms: YIT(I,J,K)*, TRUE(X), not(I) and -~YES(X,X). These axioms and 8 rules (all detailed in my ARXIV paper - but I will give it here as well) formally derive these published theorems. Turing 1937 takes about 10 steps (it is also given in the ARXIV paper.) But so far, Steven, neither your words nor your links give any examples to show that what your friends are talking about accomplishes anything at all. They describe their formalisms but give no examples of results being derived. I give examples but you don't. Why is that? Is it because your systems are warm and squishy? C-B |