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?
Is there an algorithm for converting Turing machines into equivalent Lambda expressions?
turing machines;lambda calculus;turing completeness;church turing thesis
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 | Rtype Configuration = (Integer, [Bool], Bool, [Bool])type TM = Map (Integer, Bool) (Integer, Bool, Direction)tail' :: [Bool] -> [Bool]tail' (_:xs) = xstail' [] = []head' :: [Bool] -> Boolhead' (x:_) = xhead' [] = Falsestep :: TM -> Configuration -> Configurationstep 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 -> Intrun 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.