Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 2 Oct 2006 11:21 Charlie-Boo wrote: > > > > I took a closer look at this and as far as I can tell it is nonsense. > > > > > > What part seems to be nonsense and why? I'd be glad to elaborate. > > > > The burden, thankfully, is not mine. > > Do you believe that there is a burden of proof on one who makes a claim > in a scientific discussion? I do, the claims are not mine to prove. > > > > It cannot have been peer reviewed. > > > > > > That conjecture - even if true - has no relevance to anything that we > > > have discussed. > > > > Are you claiming that this paper has been peer reviewed? > > No, the above states only that your conjecture - even if true - has no > relevance to anything that we have discussed. (It is merely > prejudicial.) Is your arVix paper endorsed by any single endorser on arVix? What did the ACM reviewers say about it? With respect, Steven
From: H. J. Sander Bruggink on 2 Oct 2006 11:23 Charlie-Boo wrote: > Steven Zenith wrote: >> Charlie-Boo wrote: > >>> I gave a reference to my ARXIV paper a little earlier (and I believe >>> you and I have discussed it before, if I am not mistaken.) In any >>> case, here is the on-line version again: >>> >>> http://www.arxiv.org/html/cs.lo/0003071 >> I took a closer look at this and as far as I can tell it is nonsense. > > What part seems to be nonsense and why? I'd be glad to elaborate. I did take a somewhat closer look on that paper of yours some time ago, and -- from memory -- what's wrong with it includes the following: * You define inferences/proofs to be sequences of formulas, following from earlier formulas, and ending in the sought after theorem. Yet, in many of your examples, the last formula doesn't even resemble the sought after theorem. Either your definition is wrong, or your inferences are wrong. * Your logical language is obscure. You write logical formulas and then claim that they have some meaning. But you don't say *why*. Your language completely lacks any form of (formal) semantics. * You don't prove any properties *about* your system. * It is not immediately clear to me what the computational power is of that toy language of yours is. In particular I have doubts about the fact that IF and WHILE clauses explicitly transfer control to the next line, which makes combining these control words problematic. * Your method is to prove a specification, and then transform that proof into a program. This is not a novel path. Yet, you don't even mention earlier comparable work. Yes, I know you think your work is superior, but if you want people to accept it, you have to write *in your paper* why that is so. Some of the above problems may be easily repaired. Some may not. But, anyway, I have no reason at all to think your paper contains anything even remotely interesting. > >> It cannot have been peer reviewed. > > That conjecture - even if true - has no relevance to anything that we > have discussed. > > In fact, I am being kind in characterizing it as a "conjecture" - it is > more an unsubstantiated (and irrelevant) assertion. Of course it's relevant. Errors are sometimes made, obviously, but in general papers in peer reviewed journals and conference proceedings are of higher quality than than an obscure Arxiv paper. And if your paper did pass some peer reviewing process, which journal did it appear in, then? groente -- Sander
From: Steven Zenith on 2 Oct 2006 12:07 Charlie-Boo wrote: > > The > > termination problem that I highlighted in functions that compute the > > root of 2 remains - the typing error is merely a matter of convention. > > What typing error is that - what did you mean to type instead? The error I made was in the convention of typing the reals - I apologize for the confusion that it introduced. I essentially advocated - because in my current work includes developing a rational point theory - that rational and irrational numbers are distinct types. It is preferable, I believe, to exclude irrational numbers from the reals because they do not terminate. That is, strictly, computations of equations that include reductions to irrational values are not computable. The typing convention simply finesses a fundamental problem. In terms of applied mathematics my approach would not be at all practical, I understand, but I remain disturbed by equations that include the computation of irrational values. Computer science does not, in practice, deal with irrational values since machines are incapable of computing them - it deals with rounding errors. This, BTW, is a limit of computer science not a limit of the world as some seem to think. We need a new way to deal with value relations since it is they that produce these problems. With respect, Steven
From: Charlie-Boo on 2 Oct 2006 12:42 H. J. Sander Bruggink wrote: > Charlie-Boo wrote: > > Steven Zenith wrote: > >> Charlie-Boo wrote: > > > >>> I gave a reference to my ARXIV paper a little earlier (and I believe > >>> you and I have discussed it before, if I am not mistaken.) In any > >>> case, here is the on-line version again: > >>> > >>> http://www.arxiv.org/html/cs.lo/0003071 > >> I took a closer look at this and as far as I can tell it is nonsense. > > > > What part seems to be nonsense and why? I'd be glad to elaborate. > > > I did take a somewhat closer look on that paper of yours > some time ago, and -- from memory -- what's wrong with it > includes the following: > > * You define inferences/proofs to be sequences of formulas, > following from earlier formulas, and ending in the sought > after theorem. Yet, in many of your examples, the last > formula doesn't even resemble the sought after theorem. > Either your definition is wrong, or your inferences are > wrong. No. Give an example. > * Your logical language is obscure. You write logical > formulas and then claim that they have some meaning. > But you don't say *why*. Your language completely > lacks any form of (formal) semantics. No. Section I: "While the standard syntax of the Predicate Calculus is used (~ not, ^ and, v or, (e) there exists, (a) for all, A B C ... variables, "..." literals), we extend the semantics of wffs by giving special meaning to certain variables: Unquantified input variables I, J, K, ... represent values that must be supplied to the program as input. Unquantified output variables x, y, z, ... represent values that are output by the program. We use single letter names P, Q, R ... to represent arbitrary relations, and multiple letter names to represent specific relations that we define. Thus, to solve P(I) a program would have to take in a value I and output a value of true or false. To solve Q(I,x) a program would take in a value I and output every value for x. Note that in general I and x represent a tuple of any number of individual values. Furthermore, additional input variables, not explicitly represented, may be present without altering the general principles and manipulations being discussed. A subscripted H is added to a wff containing output variables, as in Q(I,x)H, to indicate that the program must always halt. (The set of values output must necessarily always be finite.) For any wff W, the expression -W means that no program can exist that solves W." > * You don't prove any properties *about* your system. Read Section III. Rules of Inference. For example, the NOT Rule is P => ~P. Remember that this means that if a set P is recursive then the set ~P is recursive, and we can construct a program to decide ~P from a program to decide P. Then I give a procedure for creating that program: "NOT: Change each write (true) to write (false) and vice-versa." Do you doubt that the resulting program decides ~P? Does that not prove that the complement of a recursive set is recursive? > * It is not immediately clear to me what the computational > power is of that toy language of yours is. Look at the example programs and those constructed. Do you doubt that they calculate what I say? > In particular > I have doubts about the fact that IF and WHILE clauses > explicitly transfer control to the next line, which makes > combining these control words problematic. They don't and there is no WHILE. > * Your method is to prove a specification, and then > transform that proof into a program. This is not a novel > path. No. It is novel because it works. It is not a proof of a statement. It follows the form of a proof (Axioms and Rules) and you prove that the resulting program satisfies the specification. But people (e.g. Curry-Howard) who say that you can construct programs by proving (aX)(eY)R(x,y) where R(x,y) means input x produces output y in the specification, are wrong. I don't use anything at all like that. And mine works and theirs doesn't. And again we are back to the point where NOBODY EVER GIVES ANY EXAMPLES OF THEIR SYSTEM SYNTHESIZING ANY PROGRAMS. (Excuse me for shouting, but people always ignore that fact - which is the whole problem: produce the program, already.) > Yet, you don't even mention earlier comparable > work. Yes, I know you think your work is superior, > but if you want people to accept it, you have to > write *in your paper* why that is so. Because nobody has shown a Program Synthesis system before. Nobody can show that theirs works. People on this site have given examples (reluctantly - after many requests) and every time it required the user to type in the program, rather than the system creating a program. (More recently, I expanded CBL to generate results from other branches of Computer Science, and again nobody else has ever shown a system to do that. It's just a fact of life. Without examples, you have nothing. I give numerous examples of Program Synthesis and the formal derivation of theorems from the Theory of Computation. I will assume that you are honest. But why do you believe things that are not substantiated? Nobody has ever shown that their systems work. Computer Science publishing is full of bullshit. That is the absolute truth. I can give many examples. And if anyone would like to give here a complete example of any result from Computer Science being formally derived, I will prove it bullshit, too, as I have ever other time.) > Some of the above problems may be easily repaired. Some > may not. But, anyway, I have no reason at all to think > your paper contains anything even remotely interesting. > > > > > >> It cannot have been peer reviewed. > > > > That conjecture - even if true - has no relevance to anything that we > > have discussed. > > > > In fact, I am being kind in characterizing it as a "conjecture" - it is > > more an unsubstantiated (and irrelevant) assertion. > > Of course it's relevant. Errors are sometimes made, > obviously, but in general papers in peer reviewed journals > and conference proceedings are of higher quality than > than an obscure Arxiv paper. That is meaningless. That is just their opinion. This is SCIENCE. "in general", "higher quality", "obscure" - what do they mean? Not that I really have to engage in this m
From: Charlie-Boo on 2 Oct 2006 13:00
Steven Zenith wrote: > Charlie-Boo wrote: > > > > > I took a closer look at this and as far as I can tell it is nonsense. > > > > > > > > What part seems to be nonsense and why? I'd be glad to elaborate. > > > > > > The burden, thankfully, is not mine. > > > > Do you believe that there is a burden of proof on one who makes a claim > > in a scientific discussion? > > I do, the claims are not mine to prove. Excuse me? You said that "it is nonsense." That is your claim. Prove it. You haven't cited a single word from my paper (nor any other paper.) > > > > > It cannot have been peer reviewed. > > > > > > > > That conjecture - even if true - has no relevance to anything that we > > > > have discussed. > > > > > > Are you claiming that this paper has been peer reviewed? > > > > No, the above states only that your conjecture - even if true - has no > > relevance to anything that we have discussed. (It is merely > > prejudicial.) > > Is your arVix paper endorsed by any single endorser on arVix? What did > the ACM reviewers say about it? What does that have to do with anything? (There is no reason for me to tout those who have complemented my work.) You are attacking the messenger, the oldest trick in the book. Have you no shame? The only thing relevant here is: 1. People who make an assertion have to prove it. 2. What should society do with people who give a reference and claim that it contains a result that it does not, as you have (see details in my other post). 3. People who throw around names of organizations, people, papers, books and awards (and other bravado) when none of it is relevant to the discussion. 4. How I should be compensated for going through your bullshit references. 5. How society can rid itself of bullshitters who stand in the way of honest people who have so much to contribute but are held back by politics and corruption in publishing. Any suggestions? Your friend, C-B > With respect, > Steven |