Bounded Turing-computation tableaux

Use the syntax of Boolean formulas, CNF, and satisfiability. Fix a polynomial-time deterministic multitape verifier with certificates of one fixed length $p(n)$. If its original certificates have variable guarded length, first use the length-field construction in Polynomial time verifier and reduction interface; a verifier already using fixed-length certificates needs no such conversion. In particular a fixed empty certificate is permitted. Its ordinary binary input is $w=1^{n}0xz$, where $\mathrm{\mid }x\mathrm{\mid }=n$ and $\mathrm{\mid }z\mathrm{\mid }=p(n)$; verification checks the certificate's length-field syntax. Apply Every fixed multitape Turing machine has an equivalent one-tape simulation to this fixed verifier. The bound in The standard one-tape simulation of a fixed multitape machine has quadratic overhead gives an integer polynomial upper bound $T(n)\ge 2n+1+p(n)+1$ for the resulting one-tape running time. Enlarge its constant for short inputs. Thus the complete input length $\mathrm{\ell }=2n+1+p(n)$ is less than $T(n)$.

Write $T=T(n)$ and $W=T+2$. Rows are indexed $0,\dots ,T$ and cells $0,\dots ,W-1$. This is the bounded $T$-by-$T$ construction up to the necessary additive endpoint cells. Its augmented alphabet is $A=\mathrm{\Gamma }\bigsqcup (Q\times \mathrm{\Gamma })$: a marked symbol $(q,a)$ means the unique head scans symbol $a$ in state $q$. Configurations and initial/halting predicates are those of Configurations of a deterministic one-tape Turing machine and Initial tapes and machine-relative halting configurations.

For tableaux only, extend the ordinary step relation of The one-step configuration relation by leaving every halting configuration unchanged. In particular acceptance is a stationary absorbing sink. This padding relation does not give the original halted machine an extra physical transition. Unpadding means delete the repeated halting rows. A valid row has exactly one marked symbol and a blank, unmarked last cell. Since a head starts at zero, at time $t\le T$ it is at most $T$; the extra cell $T+1$ is never reached.

Here is a fully specified finite local rule. For an interior cell, inspect its old left, centre and right symbols. If the centre has a nonhalting head, write the symbol prescribed by the transition; retain the new head there only for a left move at cell zero. Otherwise retain the old underlying centre symbol. Put the new state/head at the centre if the old head in the left neighbour moves right or the old head in the right neighbour moves left. A halting head stays in place with unchanged symbol and state. At cell zero replace the absent left neighbour by a fixed exterior marker and clamp a left move there. At the last cell use a fixed exterior right marker; attempts to move out are forbidden. Windows with multiple heads, conflicting arrivals, or a head on an exterior marker are forbidden. All other windows have the output prescribed above. This defines a finite allowed relation $R_j(a,b,c,d)$ on the three old symbols and the new centre symbol; only the two boundary versions depend on $j$.

For each $t,j,a$ introduce $X_{t,j,a}$. Require at least one and at most one symbol per cell by ${\bigvee }_{a\in A}{X}_{t,j,a}$ and $\mathrm{\neg }{X}_{t,j,a}\vee \mathrm{\neg }{X}_{t,j,b}$ for $a\mathrm{\ne }b$. In row zero pin the fixed bits of $1^{n}0x$, leave each certificate position restricted to the two unmarked bit symbols, put state $q_0$ at cell zero, and pin all remaining cells blank. Row zero therefore has exactly one head even for $n=0$. For every row pin cell $W-1$ to unmarked blank. For each $t<T$, each cell, and each forbidden tuple $(a,b,c,d)$ add the clause $\mathrm{\neg }{X}_{t,j-1,a}\vee \mathrm{\neg }{X}_{t,j,b}\vee \mathrm{\neg }{X}_{t,j+1,c}\vee \mathrm{\neg }{X}_{t+1,j,d}$. At boundaries omit exterior literals and enumerate only the fixed exterior symbol. Finally add ${\bigvee }_{j,a}{X}_{T,j,(q_{\mathrm{a}\mathrm{c}\mathrm{c}},a)}$. Their conjunction is ${\mathrm{\Phi }}_{M,x}$. Fresh variable indices enumerate the triples lexicographically. No global head-uniqueness clause is needed after the initial row: correctness of the local rule on genuine rows supplies that invariant in the next lemma.