# How to show two models of computation are equivalent?

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.

• I guess you have chosen the wrong books. – Raphael Aug 13 '12 at 22:25
• @Raphael What's a good book on the subject? – mrk Aug 14 '12 at 4:00
• 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. – Raphael Aug 14 '12 at 6:36
• A book on just automata won't suffice. – reinierpost Aug 14 '12 at 7:16
• What books are you using? – mrk Aug 14 '12 at 12:58

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: [source]

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.

• @frabala You were right, I had the initial states the wrong way around. Fixed now, thanks! – Raphael Apr 13 '19 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.