Im trying to prove the correctness of the construction proposed in this site answer: a two stack PDA that simulates a Turing Machine. By "correctness" i mean to prove more or less formally that we can translate accepting sequences of steps.

Given a TM $M=(Q,\Sigma_I,\Sigma_O,\delta,q_0,Q_F)$ and a 2-PDA $A=(Q',\Sigma_I,\Sigma_O',\delta',q_0', Q_F)$ defined as the cited answer suggest.

We need to show that for all $w \in \Sigma^*$, if $w \in L(M)$ then $w \in L(A)$, i.e, if the first accepts then the other accepts.

This is for all $w \in \Sigma^*$: $$ \exists q \in Q_F: q_0\,w \Rightarrow_{\delta}^* \alpha_1\,q\, \alpha_2 \,\,\implies\,\, \exists q' \in Q_F: (q_0',w,\$,\$) \Rightarrow_{\delta'}^* (q',\epsilon,\beta_1,\beta_2) \tag{*}\label{*} $$ where:

  • $\Rightarrow_{\delta}$ is the usual step relation between machine descriptions, asume it is defined appropriately for TM and for 2-PDA based on the transition functions $\delta$ and $\delta'$ .
  • $\Rightarrow_{\delta}^*$ is the transitive-reflexive closure of step relation, also for TM and 2-PDA.
  • Descriptions for TM are noted $X_1...X_{i-1} q X_{i}... X_n$ meaning the actual tape content is $X_1...X_n$, actual state is $q$ and head is over $X_i$
  • Descriptions for 2-P2A are quadruplets $(q,w,\beta_1,\beta_2)$ meaning the actual state is $q$, remaining input is $w$, first stack content $\beta_1$ and second stack content $\beta_2$.

So $\eqref{*}$ is saying that for any word $w$, if there is in $M$ a sequence of steps in from $q_0$ to a final state $q$ then there is a sequence of steps in $M'$ from $q_0'$ to a final state $q'$.

Induction over the length of $\Rightarrow_{\delta}^*$ would be sketched as:

  1. Base case $n=1$ .....
  2. Induction Hypothesis: Asume for any sequence of length $n > 0$.
  3. Induction Thesis: Prove for a sequence of length $n+1$ where $n > 0$ .....

But... i have a problem with this approach. In the proof for the inductive step, we have a sequence of $n+1$ steps for $M$ like: $$ q_0\,w \,\Rightarrow_{\delta}\, ... \Rightarrow_{\delta}^n\, \gamma_1\,q_i\,\gamma_1 \,\Rightarrow_{\delta}\, \alpha_1\,q\,\alpha_2 \quad\text{ and } q \in Q_F $$

I cant apply here the Inductive Hypothesis because $q_i$ cant be a also a final state transitioning to $q$. Final states in TM can't have ongoing transitions ( maybe relaxed variants can be proposed but i prefer to let it be like that).

My question is, do i need to prove something stronger than $\eqref{*}$ to avoid these little technical inconveniences?. Im thinking something like: $$ \forall q \in Q: q_0\,w \Rightarrow_{\delta}^* \alpha_1\,q\, \alpha_2 \,\,\implies\,\, \forall q' \in Q': (q_0',w,\$,\$) \Rightarrow_{\delta'}^* (q',\epsilon,\beta_1,\beta_2) $$ But im not sure this logically implies $\eqref{*}$. I would like to hear general recommendations when doing this type of proofs.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.