Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!lll-winken!elroy.jpl.nasa.gov!ncar!midway!midway!stephen From: stephen@estragon.uchicago.edu (Stephen P Spackman) Newsgroups: comp.lang.misc Subject: Re: Halting Problem Solved! Film at 11! (Was Re: Message-ID: Date: 10 May 91 08:04:59 GMT References: <2953@optima.cs.arizona.edu> <1991May9.205401.12382@auto-trol.com> Sender: news@midway.uchicago.edu (NewsMistress) Organization: University of Chicago CILS Lines: 36 In-Reply-To: davgot@auto-trol.com's message of 9 May 91 20: 54:01 GMT In article <1991May9.205401.12382@auto-trol.com> davgot@auto-trol.com (David Gottner) writes: |PRACTICAL computers may be FSM's but programming languages are not. Nowhere |in the ANSI C standard does it give a maximum amount of memory that a C |program can run in. Thus your program checker must assume that the program |that it is analyzing will never run out of tape, which means that the analyzer |must assume that the program will run on a Turing Machine, and the |undecidability theorem applies. I never disagreed. But. First of all, I would be more interested in a verifier that told me about what my programme would do *if compiled* than one that told me what it would do if run on a non-realisable machine. Secondly, your argument applies to languages as they are presently defined; personally I wouldn't BOTHER writing a verifier for C (though if I had one there are times when I'd use it). A *new* type system, for instance, might be able to get very good mileage out of the assumption that resources are finite (though I'd be very unhappy if it assumed any PARTICULAR bound, I think). I wouldn't know, of course; I'm no theorist. But I grant your point: a C programme could consume an unbounded amount of stack and still be correct by the standard (though it would take a VERY imaginative implementation to get the heap to contain more than ULONG_MAX distinct objects, whatever ULONG_MAX is). But frankly, I think I'd rather have that flagged as an error, even if that's technically wrong! (Not that this invalidates your point.) Honestly I didn't think this was what we were talking about.... ---------------------------------------------------------------------- stephen p spackman Center for Information and Language Studies systems analyst University of Chicago ----------------------------------------------------------------------