lemmaroutine

Fixed interpreter with enforced resource bounds

A fixed randomized interpreter enforces time and space limits on encoded machines
universal machine for padding and library arguments
Lemma·lem:compiler-interpreter·§13.1 One fixed interpreter with enforced resource bounds

Statement (paper)

There is one fixed randomized Turing machine UU with polynomial worst-case running time and O(log⁡(m+2))O(\log(m+2)) counted work bits on every binary input of length mm, with the following behavior. Set λm=⌈log⁡2(m+2)⌉,R(m,dcode)=⌊λm100(dcode+1)3⌋. \lambda_m=\lceil\log_2(m+2)\rceil, \qquad R(m,d_{\mathrm{code}}) =\left\lfloor\frac{\lambda_m} {100(d_{\mathrm{code}}+1)^3}\right\rfloor. On an input with prefix 1dcode0 z 1n0 Edcode(x), 1^{d_{\mathrm{code}}}0\,z\,1^n0\, E_{d_{\mathrm{code}}}(x), it first requires 1≤dcode≤λm1\le d_{\mathrm{code}}\le\lambda_m and R(m,dcode)≥1R(m,d_{\mathrm{code}})\ge1. It then simulates the encoded machine for at most mm transitions, allowing each counted work tape only coordinates in [−R,R][-R,R]. It rejects malformed data, a requested move outside these bounds, or failure to halt by the end of the transition budget. Otherwise it returns the encoded machine's decision. The suffix after the complete prefix has no parsing significance.

In plain English

There is a single fixed randomized machine UU, running in polynomial time and using O(log⁡(m+2))O(\log(m+2)) work bits on inputs of length mm, that reads a prefix 1dcode0 z 1n0 Edcode(x)1^{d_{\mathrm{code}}}0\,z\,1^n0\,E_{d_{\mathrm{code}}}(x), checks 1≤dcode≤λm1\le d_{\mathrm{code}}\le\lambda_m and R(m,dcode)≥1R(m,d_{\mathrm{code}})\ge1, and simulates the encoded machine for at most mm steps with each counted work tape confined to coordinates in [−R,R][-R,R]. It rejects on malformed data, out-of-bounds moves, or failure to halt in time, and otherwise outputs the encoded machine's decision; anything after the prefix is ignored.

Why it's here

This gives one universal machine whose time and space limits are enforced by the interpreter itself, not assumed of the encoded machine. Later results can therefore treat any encoded machine as a resource-bounded computation of UU, which is what the padding and fixed-library arguments need.
Classified routine:
This is a standard universal Turing machine with clocked time and space bounds, the usual simulation used in hierarchy theorems and padding arguments (e.g. Arora–Barak textbook). Here it is adapted to a specific input encoding and work-tape cap.

Uses

Nothing else in the paper

Used by

claimFixed deterministic library decides interpreter promiseclaimPadding preserves acceptance probability exactly

Sources

PaperOpen
Section
§13.1 One fixed interpreter with enforced resource bounds
Page
—
Label
lem:compiler-interpreter
Line
sections/compiler.tex:112
Leannot aligned

Phase 2 aligns this node to a Lean declaration.