I'm seeking explanation on how one could prove that two models of computation are equivalent. I have been reading books on the subject except that equivalence proofs are omitted. I have a basic idea about what it means for two models of computation to be equivalent (the automata view: if they accept the same languages). Are there other ways of thinking about equivalence? If you could help me understand how to prove that the Turing-machine model is equivalent to lambda calculus, that would be sufficient.

  • $\begingroup$ I guess you have chosen the wrong books. $\endgroup$
    – Raphael
    Aug 13, 2012 at 22:25
  • $\begingroup$ @Raphael What's a good book on the subject? $\endgroup$
    – mrk
    Aug 14, 2012 at 4:00
  • $\begingroup$ I'd like to say "any book about automata", but apparenty that's now true. Unfortunately, I don't have any fitting English books at hand, sorry. $\endgroup$
    – Raphael
    Aug 14, 2012 at 6:36
  • 1
    $\begingroup$ A book on just automata won't suffice. $\endgroup$ Aug 14, 2012 at 7:16
  • $\begingroup$ What books are you using? $\endgroup$
    – mrk
    Aug 14, 2012 at 12:58

3 Answers 3


You show that either model can simulate the other, that is given a machine in model A, show that there is a machine in model B that computes the same function. Note that this simulation does not have to be computable (but usually is).

Consider, for example, pushdown automata with two stacks (2-PDA). In another question, the simulations in both directions are outlined. If you did this formally, you would take a general Turing machine (a tuple) and explicitly construct what the corresponding 2-PDA would be, and vice versa.

Formally, such a simulation may look like this. Let

$\qquad \displaystyle M = (Q,\Sigma_I,\Sigma_O,\delta,q_0,Q_F)$

be a Turing machine (with one tape). Then,

$\qquad \displaystyle A_M = (Q \cup \{q^*_1,q^*_2\},\Sigma_I,\Sigma_O', \delta', q^*_1, Q_F)$

with $\Sigma_O' = \Sigma_O \overset{.}{\cup} \{\$\}$ and $\delta'$ given by

$\quad \displaystyle (q^*_1,a,h_l,h_r) \to_{\delta'} (q^*_1,ah_l,h_r)$ for all $a \in \Sigma_I$ and $h_r,h_l \in \Sigma_O$,
$\quad \displaystyle (q^*_1,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,h_l,h_r)$ for all $h_r,h_l \in \Sigma_O$,
$\quad \displaystyle (q^*_2,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,\varepsilon,h_lh_r)$ for all $h_r,h_l \in \Sigma_O$ with $h_l \neq \$$,
$\quad \displaystyle (q^*_2,\varepsilon,\$,h_r) \to_{\delta'} (q_0,\$,h_r)$ for all $h_r \in \Sigma_O$,
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',\varepsilon,h_la) \iff (q,h_r) \to_\delta (q',a,L)$ for all $q \in Q$ and $h_l \in \Sigma_O$,
$\quad \displaystyle (q,\varepsilon,\$,h_r) \to_{\delta'} (q',\$,\square a) \iff (q,h_r) \to_\delta (q',a,L)$ for all $q \in Q$,
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',ah_l,\varepsilon) \iff (q,h_r) \to_\delta (q',a,R)$ for all $q \in Q, h_l \in \Sigma_O'$,
$\quad \displaystyle (q,\varepsilon,h_l,\$) \to_{\delta'} (q,h_l,\square\$)$ for all $q \in Q$ and $h_l \in \Sigma_O'$, and
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',h_l,a) \iff (q,h_r) \to_\delta (q',a,N)$ for all $q \in Q,h_l\in\Sigma_O'$

is an equivalent 2-PDA. Here, we assume that the Turing machine uses $\square \in \Sigma_O$ as blank symbol, both stacks start with a marker $\$\notin \Sigma_O$ (which is never removed) and $(q,a,h_l,h_r) \to_{\delta'} (q',l_1\dots l_i,r_1\dots r_j)$ means that $A_M$ consumes input $a$, switches states from $q$ to $q'$ and updates the stacks like so:

stack update

It remains to show that $A_M$ enters a final state on $x \in \Sigma_I^*$ if and only if $M$ does so. This is quite clear by construction; formally, you have to translate accepting runs on $M$ into accepting runs on $A_M$ and vice versa.

  • $\begingroup$ @frabala You were right, I had the initial states the wrong way around. Fixed now, thanks! $\endgroup$
    – Raphael
    Apr 13, 2019 at 17:38

At the beginning of Communicating and Mobile Systems: the Pi-Calculus by Robin Milner, there is a introduction on automata and how they can simulate each other so that they cannot be distinguished : Bisimulation. (cf Bisimulation on wikipedia)

I don't remember well, I should re-read the chapter, but there was a trouble with simulation and bisimulation that made them not sufficient for computational equivalences.

Thus Robin Milner introduces his Pi-Calculus and exposes it for the rest of the book.

Ultimately, in his last book The Space and Motion of Communicating Agents, you could have a look at Robin Milner's Bigraphs. They can model Automata, Petri nets, Pi-Calculus and other computational methodologies.


As far as I know, the only (or at least most common) way to do this is to compare the languages the machines/models accept. That's the whole point of Automata theory: it takes the vague concept of a problem or algorithm and turns it into a concrete mathematical set (i.e. a language) which we can reason about.

The easiest way to do this is, given an arbitrary machine/function from one model, to construct a machine from the second model that computes the same language. Odds are you'll use induction in the length of the expression, states in the machine, rules in the grammar, etc.

I haven't seen this done with Lambda and TMs (though I'm 99% sure it's possible), but I have definitely seen this kind of thing for proving equivalence of NFAs and Regular expressions. First you show a NFA which can accept any atom, then using induction, you make NFAs which accept the union/concatenation/Kleene-star of any smaller NFAs.

Then you do the opposite, to find an RE for any NFA.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.