RG <rnospa...@flownet.com> writes: > There are only two possibilities: either you have a finite-state > machine, or you have a Turning machine. (Well, OK, you could have a > pushdown automaton, but there are no programming languages that model a > PDA.
The point is that the halting problem for general Turing machines is undecidable, but there is a subset of the Turing machines, in which the halting problem is decidable. And it turns out that the decidable subset is substantial enough to write almost every program anyone usually wants to write in practice. > Well, OK, there's Forth, but AFAIK there are no static type > checkers for Forth. http://home.vrweb.de/stephan.becher/forth/ but anyway, Forth is Turing-complete. > If you have a finite state machine everything is trivial. If you have a > Turing machine everything is generally impossible. This is an > oversimplification but not far from the fundamental underlying truth. I'm sorry, but I don't think you understand the actual situation enough to be making pronouncements like that. The stuff about finite-state machines isn't even slightly relevant. > The Turner paper is right on point: there's a fundamental distinction > between the (known) finite and the (potentially) infinite. In my > experience most of the cool interesting stuff has been found in the > latter domain, and trying to shoehorn the latter into the former is more > trouble then it's worth. The point of the Turner paper is that you can design a language with separate types for finite data (like arrays) and "infinite" data (like an endless stream of requests going into a server). Such a language can restrict you to writing provably halting programs on the finite data, and provably non-halting programs on the infinite data. That is, the language doesn't let you write infinite loops on finite data or break out of infinite loops on infinite data (you can only shut down your server by "unplugging the computer", e.g. by killing the process externally). The claim is that these two classes of programs are enough for most purposes. The third possible class, the programs like the Collatz searcher where you can't tell by static analysis whether the program halts, just isn't that important. The paper argues that by giving up the ability to express those undecidable programs, a language can gain other advantages that make up for the loss of Turing-completeness most of the time. I don't think anyone has suggested languages like that are a great idea for everyday programming, but obviously there can be metholodogies that use such approaches for special purposes. -- http://mail.python.org/mailman/listinfo/python-list
