0
$\begingroup$

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.

$\endgroup$

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.