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 14:07 Jan Burse wrote: > It is a proof system which can be mechanized, > and not a manual informal example. Prove it. Show it. It's YOUR claim so give us a couple of simple examples. C-B > Bye
From: Charlie-Boo on 16 Sep 2006 14:10 Jan Burse wrote: > BTW, from descriptive complexity theory > it should be clear that one can proof > termination of programs. > > For example if a program is in P, then you > have a polynomial upper bound for the > number of steps the programm does. But who will bell the cat? C-B
From: Jack Campin - bogus address on 16 Sep 2006 14:20 > 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 seem to be thinking of conventional imperative implementations. There's nothing very implementation-specific about a lazy functional version of square root - it will generate as many places of precision as the caller asks for, and you need know nothing about the hardware or the compiler technology to know what answers you'll get. ============== j-c ====== @ ====== purr . demon . co . uk ============== Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760 <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975 stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
From: Charlie-Boo on 16 Sep 2006 14:30 abo wrote: > Charlie-Boo wrote: > > abo wrote: > > > > > I'm interested in the axioms you need to prove Godel's first > > > Incompleteness Theorem (in 10 steps). Please include the statement of > > > the Theorem in your system, as well as an explanation of any > > > idiosyncratic symbolism. > > > > Great! (These are good questions as well.) Ok, how about if you start > > a new thread that asks for the above and post the subject here (or I'll > > just see it myself.) A deal? > > > > > I thought your claim was that your axioms are "intuitively obvious". > > > > They are. You mean that it's not intuitively obvious that a UTM > > exists? Maybe not to us, but ask a child of the computer age if there > > are programs that run programs. The tottlers will ask you if you > > prefer Windows or UNIX. > > I'm afraid that's more bullshit. (That = "They are" and the > explanation you give.) Here's one axiom from the Theory of Computation: YIT(I,J,K)* where YIT(a,b,c) means "Program a with input b halts yes at iteration c." and the axiom states that (in standard terminology) the relation YIT is recursive. You will find an analogous truth in many bases of computing (computer programs and systems of logic.) Are you saying that this axiom is bullshit? How about if I had 2 axioms and 3 rules, all very short and simple, and from that I generated convincing representations of 20 different useful theorems. Would you argue that there is something wrong with the axioms because you didn't consider them intuitively obvious? C-B > > C-B
From: Charlie-Boo on 16 Sep 2006 14:37
Jack Campin - bogus address wrote: > > 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 seem to be thinking of conventional imperative implementations. > There's nothing very implementation-specific about a lazy functional > version of square root - it will generate as many places of precision > as the caller asks for, and you need know nothing about the hardware > or the compiler technology to know what answers you'll get. You're too kind. (1) Why does being an imperative implementation matter? (2) Where is a "function terminates" defined? C-B > ============== j-c ====== @ ====== purr . demon . co . uk ============== > Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760 > <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975 > stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557 |