From: Jeremy Boden Subject: How to formally prove equivalence of Turing Machine and functional languages? Date: 30 May 2000 15:54:29 GMT Newsgroups: comp.theory,sci.math,comp.lang.ml Summary: What does Church's thesis say about computability? In article <8gkg59$r7i$1@cantaloupe.srv.cs.cmu.edu>, Leonid Portnoy writes > > Does anyone know how to prove that functional languages (like ML, >Lisp, Haskell, etc.) are equivalent in computational power to a Turing >Machine? > ... This effectively comes down to the question of whether Church's thesis is "true" (i.e. any *finite* algorithm can be expressed by a TM). A number of attempts have been made to construct models which correspond to the intuitive notion of what an algorithm but which are apparently "richer" than a simple TM. But they all (so far) turn out to be no more powerful than a TM. One such example is that of recursive functions; if a function (of several variables) can be built up from simpler functions by standard operations such as composition and ultimately built up from a small toolkit of standard functions then the function is recursive. It can be shown that this is no more (and no less) powerful than a TM. Actually, since any computer could be treated as a TM which processes an input which consists of the source code of your chosen language, it would appear that no language could be more powerful than a TM. It is of course possible to be less powerful than a TM. Since a TM can be modelled by any language which can manage simple conditional / iteration it would appear that all sensible computer languages are equivalent to a TM. -- Jeremy Boden ============================================================================== From: joe davison Subject: Re: How to formally prove equivalence of Turing Machine and functional languages? Date: 30 May 2000 15:57:51 GMT Newsgroups: comp.lang.ml,comp.theory,sci.math In article <8gkg59$r7i$1@cantaloupe.srv.cs.cmu.edu>, Leonid Portnoy wrote: > Does anyone know how to prove that functional languages (like ML, > Lisp, Haskell, etc.) are equivalent in computational power to a Turing > Machine? > > Basically, one proves that it can implement a "universal funtion". The Turing machine is "computationally complete" -- It was shown that there exists a "Universal Turing Machine" that can emulate any other turing machine -- that is, given a description of the other turing machine and it's input, the UTM will interpret the description and carry out the computations the other machine would have, producing the same results. The Lambda calculus was shown to embody "universal functions" -- given a function and it's arguments, it would evaluate that function given those arguments and produce the result. (Two particular mutually recursive functions were shown to be universal -- you may have heard of them "eval" was one, "apply" the other -- Ask any Lisp programmer). One could appeal to the lisp heritage of ML, but a more direct method would be to define a way to represent an arbitrary function and its arguments as an ML function (the usual representation would probably suffice) and then demonstrate an interpreter, written in ML, that can compute the result of applying the described function to its arguments. Note that if you use the usual ML representation for functions, that simply requires writing an interpreter for ML in ML. joe