Time-controlled self-reference for nondeterministic machines

Define an explicit compiler f on valid two-tape codes d. Its output describes a machine which, on x on tape one and blank tape two, writes literal d on tape two, returns that head to zero, then executes the table described by d from its start state, with that nonblank second tape. The extra states are finite literal-writing and return chains. Tape one is preserved; a stay can be replaced by a right/left excursion, including at zero. Finally encode the whole finite table with F1's code scheme. This is effective specialization in the sense of F2, here implemented directly in the target syntax rather than through a semantic recognizer. Code-padding computation is allowed to be slow: f is only required to halt.

Construct a two-tape program Q which expects x on tape one and a valid d on tape two. It first computes $e=f(d)$ and $h(e)$, both terminating. It then arranges $h(e)x$ on tape one with all other tracks blank and runs the fixed interpreter of F1. These operations are effective two-tape algorithms: finite computation on d can use scratch tracks on the two tapes while preserving an input track for x; after computing the finite prefix, shift x right by its length with a reverse scan, write the prefix, and erase scratch tracks. Any temporary stay is replaced by the same two-move macro. Let q be the code of this finite Q table and put $e_0=f(q)$. Both q and $e_0$ are obtained by finite code generation.

On ordinary input x, $M_{e_0}$ first writes q on tape two and then runs Q. Q consequently computes $f(q)=e_0$ and then $h(e_0)$, and interprets precisely $H_{e_0}$ on x. The compiler calculations terminate independently of whether that acceptor has a branch which halts. F1 gives language equality in both directions, including when the language is empty. This proves the desired fixed point directly; F3's extensional theorem alone would not provide the quantitative assertion below.

All computation on q, $f(q)$ and $h(f(q))$ now concerns fixed finite strings, so takes a fixed number of steps and uses a fixed finite amount of scratch space, independent of x. Preserving and shifting x for the final fixed prefix costs at most $A(\mathrm{\mid }x\mathrm{\mid }+1)$ for a fixed A. F1 bounds the interpreter run by $B(\mathrm{\mid }x\mathrm{\mid }+{\tau }_{H_{e_0}}(x))+E$, where B and E depend only on the fixed target code $h(e_0)$. Add these costs to obtain C,D as stated. No deterministic dovetailing of branches occurs, so no exponential search has been concealed in C.

For the final specialization let $H_e$ be the finite program which prepends literal e to its input and directly runs A. This compiler is total and its per-e preprocessing is $O_e(\mathrm{\mid }x\mathrm{\mid }+1)$ on semi-infinite tapes; hence ${\tau }_{H_e}(x)\le A_e(\mathrm{\mid }x\mathrm{\mid }+1)+{\tau }_A(ex)$. Insert this estimate in step 4.1. Empty x still permits the literal-prefix writing; zero accepting time is neither needed nor manufactured. All parameters and constants are fixed by explicit compilation, with no AC.