Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site wdl1.UUCP
Path: utzoo!linus!decvax!decwrl!greipa!pesnta!hplabs!hpda!fortune!wdl1!jbn
From: jbn@wdl1.UUCP
Newsgroups: net.ai
Subject: Re: AI and Turing's Thesis
Message-ID: <441@wdl1.UUCP>
Date: Fri, 24-May-85 01:21:20 EDT
Article-I.D.: wdl1.441
Posted: Fri May 24 01:21:20 1985
Date-Received: Mon, 27-May-85 03:13:46 EDT
Sender: notes@wdl1.UUCP
Organization: Ford Aerospace, Western Development Laboratories
Lines: 26
Nf-ID: #R:nvuxf:-11300:wdl1:1100016:000:1482
Nf-From: wdl1!jbn    May 23 18:37:00 1985


     Undecidability is confusing to many people.  It helps to remember that
formal undecidability can only arise for machines which are either 
nondeterministic or have infinite memory.  This follows from the observation 
that a machine with finite memory and deterministic state transitions must 
eventually either repeat a previous state, there being a finite number of
such,  or halt.  So this is a total nonissue for all real computers.
     Second, Turing's proof that the halting problem is undecidable implies
only that there exist SOME programs for which the halting problem is
undecidable.  For most programs, the question can be decided, even assuming
infinite memory.
     There are practical methods for proving that a program halts.  The
usual approach is to have a single value associated with each loop which
is derived from the values that change in the loop in some way, and can
be shown to never go negative while decreasing by at least 1 every time
through the loop.  If you can construct such an expression for each
loop and each recursion in a program, then the program must eventually
halt.  If you can't find such an expression, your program has a very good
chance of containing a bug.  Steve German did his PhD thesis at Stanford
on mechanical methods for finding such expressions by automatic examination
of Pascal programs.  
     The whole issue of undecidability is a red herring in the AI and computer
field, and should be put to rest.

					John Nagle