[Solved]: Is there an algorithm for converting Turing machines into equivalent Lambda expressions?

Problem Detail: 

We know that Turing machines and Lambda Calculus are equivalent in power. And There are proofs for that, I'm sure.

But is there an algorithm, a systematic way for us to convert a Turing machine into a Lambda Calculus expression? Is it impossible to have such algorithm? (meaning does it go down to undecidability or NP-Completeness?) if not, are there any papers or algorithms for doing so?

Asked By : Ashkan Kzme

Answered By : Anton Golov

Sure there is. I'm going to assume you can figure out how to convert Haskell into the lambda calculus; for a reference, look at the GHC implementation.

Now just to be clear: a Turing Machine is a (finite) map from (State, Token) pairs to (State, Token, Direction) triples. We'll represent the states as integers (this is okay by the finiteness of the map) and represent the tokens by the values True and False. The directions will be L and R.

The state of the machine is represented by a four-tuple (State, LeftTape, Head, RightTape), where LeftTape and RightTape are lists of tokens and Head is a token.

The initial state for input n is (1, [], True, replicate (n-1) True). The machine halts if it enters state 0. The result is the number of symbols on the tape.

Now it is easy to see that the following defines an interpreter:

data Direction = L | R type Configuration = (Integer, [Bool], Bool, [Bool]) type TM = Map (Integer, Bool) (Integer, Bool, Direction)  tail' :: [Bool] -> [Bool] tail' (_:xs) = xs tail' [] = []  head' :: [Bool] -> Bool head' (x:_) = x head' [] = False  step :: TM -> Configuration -> Configuration step tm (s, lt, h, rt) = (s', lt', h', rt')      where (s', t, d) = tm ! (s, h)            (lt', h', rt') = case d of                L -> (tail' lt, head' lt, t:rt)                R -> (t:lt, head' rt, tail' rt)  run :: TM -> Int -> Int run tm n = go (1, [], True, replicate (n-1) True)     where go (0, lt, h, rt) = length . filter id $ lt ++ [h] ++ rt           go c = go (step tm c) 

(This implementation may have bugs, but a correct implementation is not far.)

Now simply take your favourite Turing Machine, partially apply the run function to it, and convert the resulting Int -> Int term into the lambda calculus.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/48622