Clocked universal simulation with time and space bounds

Fix the input syntax first. A model tag distinguishes the published one-tape code from its following multitape extension. For the latter, encode the tape count $k\ge 1$, states $0,\dots ,m-1$ with start/accept/reject $0,1,2$, alphabet $0,\dots ,r-1$ with blank0, and input alphabet $1,\dots ,s$, where $m\ge 3$ and $0\le s<r$. List the transition entries in lexicographic order of $(q,a_1,\dots ,a_k)$ for nonhalting $q$. Each entry records one next state, $k$ written symbols and $k$ directions. Apply the tuple blocks from F2 to these canonical numerals. A tagged old code is the case $k=1$ with its original interpretation. The tag changes its length by a constant. For either tagged form, define the initial multitape configuration to have state0 and every head at cell0, with $x$ in cells $0,1,\dots$ of the first tape and every other cell of every tape blank; each tape uses F5's clamped left boundary. Encode the word $x$ by its tuple of canonical symbol numerals, explicitly allowing arity zero with code $0$ for the empty word. The outer tuple contains the program, word and canonical $\mathrm{bin}(b)$; its self-delimiting syntax is included in the input-length accounting. These explicit extensions do not reinterpret any published one-tape code.

A finite parser reads unary lengths and the indicated blocks, verifies canonical numerals, the model tag, symbol/state ranges and the table's actual entry count, and rejects extra or missing bits. To check the expected count $(m-2)r^k$ against an actual count $a$, use integer arithmetic saturated at $a+1$: when $r\ge 2$ stop exponentiation as soon as it exceeds $a$, and when $r=1$ the power is one. Thus an enormous malformed tape-count numeral cannot force an enormous allocation. All malformed inputs halt rejecting by finite scans and finite arithmetic loops. On valid inputs for a fixed $M$, the whole program, $k$, alphabet widths and table length are constants. Scan the word blocks once, consuming their unary length headers on spare tapes and checking each symbol against the fixed alphabet; copy the decoded word to a sequential archive. Validate/copy the binary clock by one scan. These routines cost $O_M(n+\log (b+2))$ time and space: every input bit is traversed a bounded number of times, except scans of fixed $M$-data. The theorem claims no uniform time bound on malformed descriptions.

For the time interpreter, give each virtual tape a centre record and two ordered stacks of records extending outwards. Each record stores a tape symbol and an immutable origin bit, initially1 exactly at cell0. Writing changes only the symbol. The positive stack initially contains input cells1,2,... and then blanks on the first tape, and blanks on the others; the negative stacks initially contain blanks. Put $h_i=2^i$, $i\ge 0$. On each side zone $i$ has capacity $2h_i$, with occupancy in $\{0,h_i,2h_i\}$; holes use a distinct code, and ordinary blank symbols count as genuine records. Genuine records are packed at the near end in stack order. The two occupancies at each level sum to $2h_i$. Initially both are $h_i$, and the centre is the initial scanned cell. Ignoring holes and concatenating the zones gives the exact two stacks. The base zone has capacity2 and half-occupancy1.

Construct $U_{\mathrm{s}\mathrm{p}\mathrm{a}\mathrm{c}\mathrm{e}}$ separately. Use the same validated finite program and input archive, but store the $k$ virtual tapes as delimited rows of fixed-width symbol records with one head flag per row. Include cells through the larger of the last initially occupied input cell and the furthest cell so far visited. Other tapes start blank. Sweeps locate the $k$ flags and read their symbols; a scan of the fixed program table selects the transition. Further sweeps write the symbols and move each flag to its adjacent record, clamping at zero and appending a blank record when needed. Inserting a record can shift a finite suffix from its right end with one temporary record, or copy the rows to a spare tape of their total length. Update the state only after all rows' actions. These operations produce exactly the next configuration and keep no history. No fast-time bound for the sweeps is asserted.

For a move towards the positive stack, first write the old centre $c$ as prescribed and choose the least $i$ with nonempty right zone. All lower right zones are empty and their left partners full. Remove the first $h_i$ records from right zone $i$. The first becomes the new centre; distribute the remaining $h_i-1={\sum }_{j<i}{h}_j$ in order into the lower right zones, with $h_j$ records in zone $j$. Right occupancy at $i$ decreases by $h_i$, from $h_i$ or $2h_i$ to0 or $h_i$. Prepend $c$ to the concatenated lower left zones. This list has $1+2{\sum }_{j<i}{h}_j=2h_i-1$ records. Keep its first $h_i-1$ in the lower left zones, half in each, and prepend the remaining $h_i$ to left zone $i$. Its old occupancy was0 or $h_i$, hence its new occupancy is $h_i$ or $2h_i$. Order and complementary occupancy are preserved; every lower zone ends half-full. At $i=0$ the lower lists are empty and these formulas simply transfer one record to the centre and prepend the old centre on the other side.

Realize the buffers on a fixed number of physical tapes over a fixed alphabet of binary digits and finitely many marker codes. The interpreter does not acquire $k$ physical tapes or an alphabet ${\mathrm{\Gamma }}^k$. Instead a physical slot is a delimited block of $k$ fixed-width symbol/origin-or-hole fields. For fixed $M$ its width and the saved program-table length are constants. Two tapes store the outward left/right zone sequences; other fixed tapes store centres, table, archive, countdown and scratch lists. A zone has endpoint and midpoint markers and one three-valued occupancy flag per virtual tape. Scanning through zone $i$ traverses $O_M({\sum }_{j\le i}2h_j)=O_M(2^i)$ physical cells. If binary level labels are used their total length $O({\sum }_{j\le i}\log (j+2))$ is also $O(2^i)$.

Interchange left and right for the negative-stack move. When a requested left move has the origin bit in its centre, perform the write but no stack move. Records retain their origin bits, so this is exactly the clamped convention and no auxiliary negative cell is scanned. A suitable source zone always exists, since untouched higher zones are half-full. Select the simulated transition from the original tuple of $k$ centre symbols, store its instructions, then process the $k$ buffer operations successively and update the state. Thus each completed simulated transition has exactly the writes, movements and state of $M$; one tape's redistribution does not alter another tape's fields.

Fix one virtual tape and $i\ge 1$. Let $q_i$ be total right occupancy below level $i$, and $H_i={\sum }_{j<i}{h}_j=2^i-1$. Initially $q_i=H_i$. Every operation at level at least $i$ resets these lower zones to half-full, again leaving $q_i=H_i$, including operations strictly above level $i$. Between these resets, a positive-stack move at a lower level decreases $q_i$ by exactly1, a negative-stack move increases it by exactly1, and a clamped move leaves it unchanged: redistribution conserves all lower right records except the single transfer through the centre. An operation at level at least $i$ requires all lower source zones empty, so immediately before it $q_i=0$ or $q_i=2H_i$. Reaching either endpoint from $H_i$ needs at least $H_i$ preceding lower-level moves, followed by the triggering move.

Find the least nonempty source zone by scanning its occupancy flags. Copy the affected genuine sublists of the chosen virtual field to scratch in stack order, then scan back to distribute the explicit lists from step 4.1. Preserve other virtual fields, write holes in unoccupied slots, and update occupancy flags. Midpoint and endpoint markers determine all half-capacities without per-record unbounded arithmetic. A fixed number of copying/writing/return scans of this prefix and its scratch lists implements the redistribution, costing $O_M(2^i)$. To extend the allocated prefix, copy a unary marker of the previous zone's capacity twice, putting a midpoint between the copies. Each copy and return is linear, and writing the fields and updating the unary marker costs the new zone's length. The first zone is a literal layout. Thus allocation also costs $O_M(2^i)$. These are fixed finite-state scan/copy routines with saved finite program data; no random access or unit-cost large-integer operation is assumed.

Maintain a binary countdown initially $b$. At each simulated configuration, test the state first and report its acceptance/rejection if halting. Otherwise reject if the countdown is zero; otherwise simulate one transition, decrement, and repeat. A whole-clock scan costs $O(\log (b+2))$ per transition, sufficient here without an additional amortization. A halt on the $b$th transition is reported, while a still-nonhalting configuration at expiry rejects. At $b=0$ the nonhalting initial state rejects before simulation; at $b=1$ exactly one transition is allowed. A zero clock occupies one digit.

Consequently each event at level at least $i$, including the first, is separated from the previous reset or the start by at least $H_i+1=2^i$ simulated transitions. Among $b$ transitions there are at most $\lfloor b\mathrm{/}{2}^i\rfloor$ such events, and in particular at most that many events exactly at level $i$. Higher resets are themselves counted events and cannot bypass this argument. There are at most $b$ level-zero events, and no level with $2^i>b$ is reached. This count applies separately to each of the fixed $k$ virtual tapes.

The convenient physical scan routines may use stationary heads. Compile this fixed physical machine to the left/right-only model by storing logical cell $j$ at physical cell $2j$. Implement each logical step by two physical steps: a right request uses $R,R$, a left request $L,L$, and a stationary request $R,L$. On the first step write the desired logical symbol and retain the finite tuple of pending moves in finite control; on the second preserve the currently scanned symbol and complete the movement. Intermediate odd cells have no logical role. A left request at zero clamps at zero on both steps. All heads again lie at the prescribed even cells, including mixed moving/stationary requests. The fixed number of physical heads makes the pending tuple finite-control data. This initial spacing also has a left/right-only linear implementation: process two input symbols per four steps, with source moves $R,R,L,R$ and destination moves $R,R,R,R$. Read the first symbol in the first step and the second in the second step, and write them at the destination even positions in the first and third steps. Ignore intermediate reads and preserve odd cells. One temporary symbol fits in finite control; an odd final symbol is paired with blank. The input delimiter detects the end, and a return sweep to marked cell zero is linear. Other unused heads oscillate in a four-step $R,L,R,L$ cycle. A spare tape receives the spaced input; the original raw-input tape is thereafter ignored. Thus initial spacing does not assume the stationary-head capability that is being compiled away. This compilation changes time and visited space by constant factors, plus input preparation.

Initialize only the centres, retaining the archive head at input position1; do not distribute the whole word into buffers. Unallocated zones mean their untouched initial half-full lists. On first reaching a new global level $i$, initialize its right half-list for the first virtual tape from the next $h_i$ archive symbols, then blanks if the archive is exhausted; all other tape fields and the left halves initially receive blanks. Fill unused halves with holes. Initially that right zone represents positions $2^i,\dots ,2^{i+1}-1$. Operations below it leave this suffix unchanged, and new levels are allocated in increasing order, so the archive is exactly at the next untouched interval. If another virtual tape forces allocation first, initialize all fields of that zone then. Each symbol is read from the archive at most once and no scan back through the long input is needed. Allocation is charged to the first event reaching that level as in step 6.2. For $b\ll \mathrm{\mid }x\mathrm{\mid }$ there is only the initial $O_M(n)$ archive scan plus the lazily reached buffer prefix, not $O_M(n\log n)$ preprocessing.

If $v_j$ is the visited extent on tape $j$, the first row has at most $\mathrm{\mid }x\mathrm{\mid }+v_1+1$ records and every other row at most $v_j+1$. Including fixed-width symbols, delimiters, saved code/input and scratch copies gives $O_M(n+{\sum }_j{v}_j)$ visited cells. Since a head starts at zero and moves by adjacent steps, its visited cells form this initial interval; their sum is the statement's $S$, up to the harmless fixed endpoint convention. Add the $O(\log (b+2))$-cell countdown and use the test-before-expiry loop of step 6.3. The finite valid-input decoder and saved tables use $O_M(n+\log (b+2))$ space by step 2.1. Spacing and the two-step physical compilation of step 7.2 change only constants. Hence this distinct interpreter uses $O_M(n+S+\log (b+2))$ visited space.

For $b\ge 1$, steps 7.1 and 6.2 bound the total buffer work on all virtual tapes by $C_{M}b+C_M{\sum }_{i=1}^{\lfloor {\log }_{2}b\rfloor }{2}^i\lfloor b\mathrm{/}{2}^i\rfloor \le C_{M}b(1+\lfloor {\log }_{2}b\rfloor )\mathrm{.}$ Initialization costs $O_M(n+\log (b+2))$, table/centre processing $O_M(b)$, and clock work $O(b\log (b+2))$. Including the fixed compilation gives $O_M(n+b\log (b+2))$. At $b=0$ no buffer or transition work occurs and the constant clock length is absorbed by the nonempty encoded-input syntax. This constructs $U_{\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}}$. No linear visited-space claim for its buffers has been used or proved.

Both interpreters halt rejecting malformed encodings, and reproduce the same bounded acceptance/rejection behavior on valid inputs by the configuration invariants and expiry test. Neither interpreter's resource proof is imported into the other. If the clock is produced by a constructor rather than supplied, add that constructor's separately declared time/workspace. All choices above are explicit finite scans and prescribed lists; no choice axiom is used.