Simulating a Turing machine with a tableau [cpsc/tm-tableau]

Main idea: an algorithm can be converted to a Boolean circuit

…table…

M accepts w if and only if the tableau can be filled such that:

  • The first row is the starting configuration of M on input w
  • (i+1)st\left( {i + 1} \right)^{\text{st}} configuration follows from the ithi^{\text{th}} configuration
  • Eventually reach an accepting configuration

So how can this tableau be converted into a boolean formula? We’ll come up with some boolean variables to represent what is happening in the cells.

Let cell[i,j]\text{cell}\left\lbrack {i,j} \right\rbrack refer to the according tableau entry.

  • Note: row i: time step, column j: head position, i,j≤nki,j \leq n^{k}
  • Our cell entries are not boolean values: but we still want to encode them as such!
  • Create boolean variables xi,j,sx_{i,j,s} where i,j≤nki,j \leq n^{k} and s∈γ∪Qs \in \gamma \cup Q
  • cell[i,j]=s⇔xi,j,s=true∧xi,j,s=false∀s≠s\text{cell}\left\lbrack {i,j} \right\rbrack = s\Leftrightarrow x_{i,j,s} = \text{true} \land x_{i,j,s} = \text{false}\ \forall s \neq s

For a nondeterministic Turing machine:

  • The same table as the deterministic Turing machine:
  • only the (i+1)st\left( {i + 1} \right)^{\text{st}} configuration follows from the ithi^{\text{th}} configuration using some nondeterministic choice

φ=φcell∧φstart∧φmove∧φaccept\varphi = \varphi_{\text{cell}} \land \varphi_{\text{start}} \land \varphi_{\text{move}} \land \varphi_{\text{accept}}

  • φcell=∧i,j(∨s∈Γ∪Q(xi,j,s∧¬(∨t≠sxi,j,t)))\varphi_{\text{cell}} = \land_{i,j}\left( {\vee_{s \in \Gamma \cup Q}\left( {x_{i,j,s} \land \neg\left( {\vee_{t \neq s}x_{i,j,t}} \right)} \right)} \right)
  • φstart=x1,1,#∧x1,2,q0∧x1,3,w∧x1,4,w…\varphi_{\text{start}} = x_{1,1,\#} \land x_{1,2,q_{0}} \land x_{1,3,w} \land x_{1,4,w}\ldots
  • φaccept=∨i,jxi,j,qaccept\varphi_{\text{accept}} = \vee_{i,j}x_{i,j,q_{\text{accept}}}: check if any cell is accepting

Window[i,j]: six cells of the table (six cells is convenient: 3x2, we need three to read the current, state, and next items)

  • i.e. the window is size 3x2 because that’s exactly what we need to check that it is valid

φmove=∧1≤i≤nk−1,1≤j≤nk−2(Window[i,j]is legal)\varphi_{\text{move}} = \land_{1 \leq i \leq n^{k} - 1,1 \leq j \leq n^{k} - 2}\left( {\text{Window}\left\lbrack {i,j} \right\rbrack\ \text{is legal}} \right)

note: pull examples, when there is no head the last two columns cannot change

… online lecture …