Notions of computation

From: Lauri Alanko (la_at_iki.fi)
Date: 02/25/04 

Date: 25 Feb 2004 09:29:43 GMT

[Followups to comp.theory]

Some loosely related questions on computation.

Firstly, as everybody knows, there are multiple equivalent ways of
formalizing the same notion of computation: Turing machines, partial
recursive functions, lambda calculus, combinatory logic, etc. Of
these, Turing machines are the most popular expository tool for
discussing computability theory.

Why is this? Of the above options, TMs are not only the farthest
removed from practical programming, but they are also the only ones
that don't have a convenient syntactic notion of composition. Yet such
basic facts as "the union of recursive languages is recursive" and "if
a language and its complement are recursively enumerable, then the
language is recursive" etc. are proven by composing machines that
recognize those languages.

So we usually end up with figures of boxes connected with lines, and
general handwaving about "we simulate this one on this tape, and that
one on that tape, and then these all tapes on this one tape" instead
of using precise and concise notation. In LC you could just say:

decide_L1_U_L2 = \x. or (decide_L1 x) (decide_L2 x)

and you could prove this function's totality quite as formally as for
Turing machines, and (IMHO) much easier.

Why, then, are Turing machines so often preferred? Is there some
virtue to them that I'm missing?

Second question. Though the above equivalences are well-known, I still
haven't found very concrete proofs. Only general "in principle"
-proofs that usually work by constructing horrendous Gödel numbers
that you would never want to be deal with in practice. Can someone
suggest where to look for a _fully specified_ (ie. directly
implementable) translation between Turing machines and lambda terms?
The translation between LC and combinatory logic seems to be much more
easily available. Finally, the relationship between lambda terms and
mathematical functions is studied in denotational semantics and the
model theory of LC. Is there a similar theoretical framework for TMs?
(If not, I think this is yet another argument for their
impracticality...)

Thirdly. One property of the class of computable functions is that it
includes its own universal function: there is such a thing as a
universal Turing machine, and an LC evaluator written in LC, and of
course a universal recursive function Phi(x,y)=phi_x(y) where phi_i
enumerates all recursive functions.

Are there other interesting classes of computable functions that also
include their own universal function? Ie. are there sensible
non-Turing-complete languages in which their own evaluator can be
written?

And finally. The reason why we are so interested in this particular
class of functions is that they are, well, computable. Implementable
in practice. Yet I'm not quite clear on _why_ this is so. It is clear
that Turing machine equivalents (modulo infinite tape) are
implementable in the real world: computers do exist, after all. So
this particular system we call "physics" can compute at least all the
partial recursive functions. And the Church-Turing thesis claims that
it can do no more.

But this is not yet an explanation. A physical computer is a
horrendously complicated beast, and doesn't really reveal what it is
that makes it tick.

So I'd be interested in at least a semi-formal explanation of _why_
the physical laws are a Turing-complete system. It doesn't need to go
to the details of quantum mechanics or anything, a simplified
Newtonian view of solid particles bouncing around is okay. Just as
long as it somehow corresponds with our intuitive notion of how
physical things interact.

Comments and suggestions for references are appreciated.

Lauri Alanko
la@iki.fi

Relevant Pages

  • Re: Notions of computation
    ... > formalizing the same notion of computation: Turing machines, ... > recursive functions, lambda calculus, combinatory logic, etc. ... Step 1: Representation of tape. ...
    (comp.theory)
  • Re: A qn on primitive recursive functions
    ... > discussing recursive functions BEFORE we meet Turing machines, ... > course, remember, before we've heard of Turing machines, etc.] speculate ... > that the total recursive functions are ALL the intuitively computable ... then the diagonalization trick will necessarily generate ...
    (sci.logic)
  • Re: Computable functions/reals.
    ... abstraction or extension, IMHO, by the Church-Turing thesis. ... can extend Turing machines the way Mr. Ullrich or anyone else does. ... machines are intuively computable functions on N and all intuively ... all recursive functions on N are turing machines. ...
    (sci.logic)
  • Re: Notions of computation
    ... formalizing the same notion of computation: Turing machines, ... recursive functions, lambda calculus, combinatory logic, etc. ...
    (comp.theory)
  • Re: Computable functions/reals.
    ... When we are speaking about Turing machines some other posters say we ... functions on the naturals. ... some posters avoid that restriction to reintroduce it indirectly in ... essentially recursive functions on N by the literature, ...
    (sci.logic)
Loading