🚀 go-pugleaf

In article <2953@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
|In article  <STEPHEN.91May7205714@pesto.uchicago.edu> Stephen P Spackman writes:
|]In article <2861@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
|]
|]|If you want to get theoretical, then you can _theoretically_ keep
|]|buying tapes...
|]
|]There is definitely and without question a finite amount of matter in
|]the universe that I am willing to make tapes out of.
|]
|]Evidently, I disagree. I am PERSONALLY willing to engineer my
|]compilers on the assumption that (a) FTL travel, (b) many-worlds
|]parallelism and (c) anything comparably revolutionary will not become
|]available within the useful lifetime of the software.
|
|Not fair, Stephen.  You took the theoretical argument and made
|practical objections to it.  Your objections do not address the issue
|of whether a computer is _theoretically_ a finite state machine -- and
|I covered the practical issues in the part you did not cite.

I wasn't cheating, I was just trying to reiterate - and defend - a
particular cut on the problem. There was a particular view given here
that it is interesting to study the THEORETICAL properties of
PRACTICAL machines.  I *could* talk about the theoretical properties
of theoretical machines or about the practical properties of practical
machines, yes, and that would be "fairer pool" in that it would
address what, perhaps, you thought I was talking about. But I
disagree!

The point is: bar some MAJOR breakthroughs in physics, the machines we
WORK with have limits. The fact that machines have limits has
potential theoretical implications. It is proposed by some to explore
them.

Objections that theoretical machines lack practical limits or that the
practical limits of practical machines are more immediate are SIMPLY
NOT GERMANE.

I addressed your comment that I understood to address my argument.

Let me try one more time. PRACTICAL computers are FSMs and not fully
general turing machines because PRACTICAL computers are finite. The
fact that PRACTICAL computers are finite is an important THEORETICAL
property of PRACTICAL computers and may need to be addressed before
certain ideas are dismissed. And this is true even if you include all
the input they're ever going to get as state space.

...I feel a bit like you're telling me that it's impossible to code a
correct sort, because you never know when your input is going to be
an infinite stream and the function just might not terminate....
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
systems analyst                                  University of Chicago
----------------------------------------------------------------------

In article <STEPHEN.91May9022258@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:

>Let me try one more time. PRACTICAL computers are FSMs and not fully
>general turing machines because PRACTICAL computers are finite. The
>fact that PRACTICAL computers are finite is an important THEORETICAL
>property of PRACTICAL computers and may need to be addressed before
>certain ideas are dismissed. And this is true even if you include all
>the input they're ever going to get as state space.

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 feel a bit like you're telling me that it's impossible to code a
>correct sort, because you never know when your input is going to be
>an infinite stream and the function just might not terminate....

Of course some simple argorithms may be proven, like a sorting algorithm,
but not >ALL<
-- 
David Gottner
davgot@auto-trol.COM                           Auto-trol Technology Corporation
{...}ncar!ico!auto-trol!younam                 12500 North Washington Street
(303) 252-2321                                 Denver, CO 80241-2404

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
----------------------------------------------------------------------