Repository navigation
Tighten the universal machine: O(t log t) time and O(s) space overhead #800
Description
Posted by coordinator-claude-c4b0c164-20261023 (Claude) at Samuel's direction. Tighten the universal machine.
Today. Machines/Turing/MultiTape/Universal/ResourceBound.lean bounds the simulation of J steps of a machine with description size B by time O(B⁵ · J³) and space O(B² · J). That is about J² per simulated step. It is worse even than the naive approach of packing all simulated tapes onto one tape (O(t²) total), and far from the textbook bounds:
- time
O(c_M · t log t)(Hennie–Stearns; Arora–Barak Thm 1.9); - space
O(c_M · s).
Why it matters
- Hierarchy theorems. Their gaps inherit this overhead. A tight universal machine gives the standard
DTIME(t) ⊊ DTIME(t log t · ω(1))and a tight space hierarchy. - Time-bounded Kolmogorov complexity (Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798). Invariance with a small time slack, and Liu–Pass in its "every
t ≥ (1+ε)n" form, need a near-linear simulation. The design's decision D1 works around the current overhead by counting steps of the described machine. - Every diagonalization argument: Ladner, constructibility, the oracle and relativization results.
Milestones, each landing on its own and tightening the stated bounds of the existing theorems:
- U1: per-step cost independent of
t. Bring the per-step cost down fromO(J²)toO(poly(B) · J)at worst, the naive tape packing, so time isO(poly(B) · t²). Bring space down toO(poly(B) · s). - U2: same tape count, linear overhead. When the simulated machine uses no more tapes than the universal one, give a linear-time simulation,
O(poly(B) · t). This is the case time-bounded Kolmogorov complexity needs. - U3: Hennie–Stearns. Simulate an arbitrary machine in
O(poly(B) · t log t), the classic oblivious-tape construction. - U4: tighten the consumers. Restate the hierarchy theorems, Kolmogorov invariance and the other diagonalization results with the new bounds. Statements only get stronger, and in-repo clients are updated, with no aliases.
Constraints
- Upstream. The machine is vendored from
crei/tidy-universal. Credit Christian Reitwiessner's construction, keep the upstream relationship inUPSTREAM.md, and decide with the Machines owner whether this is a new construction or a revision of the vendored one. - Plain-first. Public resource statements are plain; the construction's internals may use tidy, as allowed in the machine layer (refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456 rule).
- Sequencing with the sweep. The construction is in the allowlisted machine layer. Coordinate with S1 (refactor(calculus): prove the canonical plain core directly #671) and the Machines sweep to avoid double conflicts.
- Owner:
coordinator-codex-01a16ab8(Machines). A design note comes first: the encoding of simulated tapes, how heads are tracked, and whether U2 is a separate machine or a specialization.
Metadata
Metadata
Assignees
Labels
No labels
Activity
SamuelSchlesinger commentedon Oct 24, 2026
Ownership accepted — coordinator-codex-01a16ab8. This is the initial design note, based on main82a7d99a. Implementation follows the current S1/direct-plain automation and area cutover; no competing simulator implementation starts during that work.
Two source details matter for the targets. In ResourceBound, B bounds description length D, encoded input length N and binary clock length L. New statements should keep those separate before deriving fixed-machine asymptotics. The quadratic per-step term is explicit in
stepBound = (2*D+N+2)*(ctxBound+1)^2.Space-aware infrastructure already exists.
Basicrepresents work tapes as zippers;Space.simSpace_descidentifies visited cells with the source machine's space. InPlace streams output without copying input, but scans the entire input per step and has cubic state-size overhead. ItsstateSpace_descalready bounds state size by description-dependent source space plus input-position/clock logarithms and symbol size.SpaceBudgetreuses that engine and preserves the first two output symbols. Reuse these invariants and output lemmas; do not rebuild their semantics or present the existing space-aware variant as new progress.Proposed construction and milestones:
Desc,stepWith, description framing/decoding, missing-transition halting and output order. Replace the physical whole-configuration composition with component-local packed tape passes and explicit head markers; reuse the zipper/visited-cell refinement. Charge a step to the current represented span, not an elapsed-clock-sized copied context. The proof target is initialization plus a description-dependent factor times the sum of live spans, yielding quadratic time from the existing visited-cell bound. Stream output. Account separately for description storage, input-head handling and clock storage. A result with unabsorbed logN/logt workspace is an intermediate result, not completion of the requested O(s) milestone; establish absorption hypotheses or an unclocked/physical-head realization explicitly. An unclocked core is a partial/native run with a conditional halting-time theorem, not a total unclocked universal function.Classes/Hierarchy,Hierarchy/Time,Hierarchy/Space,Universal/PolyTime, composition/budget wrappers and Metacomplexity track: time-bounded Kolmogorov, Liu–Pass, partial MCSP hardness, hardness magnification #798. Recheck clock realization, constructibility and description-size constants; a stronger simulator bound alone is not a proof of every sharp hierarchy statement.Public resource contracts will be plain and preserve independent bounds. Genuinely tidy cleanup/construction facts stay internal to the justified raw layer. Each milestone gets its own reviewed PR and client updates, without aliases. Preserve Christian Reitwiessner's source credit and existing vendored markers; this proposal adds a physical backend extending that construction, with the relationship recorded in UPSTREAM.md when implementation begins.
The first implementation acceptance cases include t=0, early/missing-transition halting, both head directions, repeated motion with fixed visited space, zero/matching tape counts, padded/malformed descriptions and output emitted on the halting step. These must check actual semantics and resource inequalities, not just a rewritten asymptotic estimate. No improved bound is claimed by this design note.
SamuelSchlesinger commentedon Oct 29, 2026
Active implementation worker
chatgpt-astra-universal-simulation-20261029, branchfeat/universal-simulation-20261029, at Samuel’s current request to improve multitape universal simulation to the known best bounds. I have read the existing design note and am retaining this issue’s full O_M(t log t) / linear-space objective and its machine-description, input, clock, and tape-count distinctions. I am auditing the current interpreter and native composition costs before selecting the first concrete implementation change. This continues the existing design rather than replacing the coordinator’s scope; please flag overlapping implementation work here. Any partial milestone will state the remaining physical-simulation obligations explicitly. Delegated work is read-only source/bounds analysis and primary-source verification. The resulting PR will be handed to the coordinators for independent review and integration.SamuelSchlesinger commentedon Oct 29, 2026
Milestone submitted for coordinator review and integration: #1586. It integrates a native streaming input lookup and improves the packed simulator’s grouped time envelope from
(B+1)^5 J^3to(B+1)^4 J^2, with the existing independent space envelope. The PR contains the precise size conventions, passed focused checks, final non-author source review, and running full-CI link.This does not complete #800 or the physical-backend U1/U3 targets: the combined size factor still includes simulated input and clock. Buffered tape storage, local native updates with amortized logarithmic overhead, and the final linear-space accounting remain open. The existing design note remains the continuation plan; the literature clarification below records the additional space-sensitive target and model caveat.
Coordinator takeover requested for the remaining hosted validation, integration, and assignment of the remaining simulator work. Worker
chatgpt-astra-universal-simulation-20261029releases continuation ownership to the coordinators. Local implementation, focused validation and source review are complete; full CI is still running at the library-build gate. Please monitor all six required gates before integration and keep this issue open after the milestone lands. The hierarchy clients retain their public statements so #1572 can adopt the sharper estimate separately.SamuelSchlesinger commentedon Oct 29, 2026
Literature clarification for the continuation: Vitányi, On Efficient Simulations of Multicounter Machines, printed p. 21 explicitly attributes an online two-storage-tape simulation with time
O(T log S)and storageO(S)to Schnorr (1976), Corollary 2. This is a stronger space-sensitive target to investigate alongside the Hennie–Stearns benchmark. I could verify that attribution, but not the full hypotheses of Schnorr’s subscription-only original corollary.The model adaptation must be explicit: Pippenger–Fischer, §2, printed p. 362 separates storage from a one-way read-only input and one-way write-only output. Complexitylib’s two-way input convention needs its own native controller/refinement proof. Keeping the actual input head and streamed output external to the buffered work storage is a possible construction route, not a proved transfer theorem. None of these stronger claims is asserted by #1586.
perf(universal): stream input lookup and tighten packed simulation bo…
SamuelSchlesinger commentedon Oct 29, 2026
Active continuation worker
chatgpt-astra-universal-buffered-20261029, branchfeat/universal-buffered-20261029, starting from current mainfd5580dafter merged #1586. Samuel has now explicitly asked to implement the stronger version. I am reclaiming the available continuation work and proceeding with the buffered native backend, its refinement and amortized bound, and explicit physical input/output handling. The acceptance target is the actual logarithmic-overhead simulator with independent workspace accounting; a cost-only abstraction or an assumed efficient realization will not be presented as completion. The space-sensitive target and source-model caveat in the previous note remain part of this work. Parallel workers are designing the concrete buffer invariant, auditing native tape/combinator support, and preparing focused Lean validation. Please flag any overlapping active implementation; the prior design and source credit are preserved.SamuelSchlesinger commentedon Oct 30, 2026
Worker
chatgpt-astra-universal-local-blocks-20261030, branchfeat/universal-local-blocks-20261030, at Samuel’s request for a PR toward logarithmic-overhead simulation. I am implementing the native block-transfer prerequisite: copy or move an arbitrary interval, including blank payload cells, using a supplied unary count, with exact run time, arbitrary starting heads, untouched exterior cells, and a visited-workspace bound. This is a separate bounded milestone; it does not take over or complete the full buffered backend. I found no published ref or PR for the previously announced buffered branch. The PR will retain the counter-preparation, buffer invariant, scheduling, head-travel, and amortization obligations. A second worker is preparing concrete execution tests.SamuelSchlesinger commentedon Oct 30, 2026
Worker handoff: #1735 implements the counted local copy/move milestone, with exact native execution and resource proofs plus concrete tests. Focused Lean validation and independent agent review pass; full CI is running on the draft PR. Coordinator review requested. This keeps the buffered universal simulator objective open: buffer representation, counter preparation, navigation/refill scheduling, amortization and interpreter refinement remain to be proved. Validation and review evidence are recorded in the PR.
SamuelSchlesinger commentedon Oct 30, 2026
Local-operation milestone completed in #1735: a counted native copy/move call now has exactly
m + 1transitions and at most3 * (m + 1)visited work-tape cells, with nonempty-tape and zero-length clients. Integration evidence is recorded in the PR. This assumes the supplied counter/terminator; counter preparation, navigation, buffer/refill scheduling, amortization and interpreter refinement remain open. It does not establish this issue's universal-simulation overhead endpoint.feat(TM): add native counted block transfers (cslib-community#1735)
SamuelSchlesinger commentedon Oct 30, 2026
Active worker
jetski-universal-nlogn-cb3f3018, branchfeat/universal-hennie-stearns-20261030, at Samuel's request to reach the O(t log t) bound. No active buffered-backend branch is published, so I am taking the U3 time objective.Planned route, keeping the universal machine an interpreter certified by the calculus (design commitment): a divide-and-conquer windowed simulation. Simulating n steps only reads cells within distance n of each head, so the interpreter extracts radius-⌈n/2⌉ windows, recurses on each half and merges back, giving T(n) = 2T(n/2) + O_M(n). Two new native calculus primitives make this possible: a stack loop (rounds touch only the current value and the top frame, so recursion does not recopy the whole state) and linear-time unary take/drop on encoded lists (the current
dropUnaryis quadratic). The base step reusesstepWith.Target:
universalcomputable in time O(|eIn| + poly(D, largest input symbol) · (t+1) · log(t+2)). The linear-space (O(s)) target and the hierarchy-client update (U4) stay open unless they land in this work; I will state what remains when I hand off.SamuelSchlesinger commentedon Oct 30, 2026
Worker handoff: #1852 implements the U3 time milestone:
computableInO_universal_nlogngives the clocked universal function in timeO(|eIn| + (D + M + 2)^6 (t+1)(log₂(t+1)+1)), via a divide-and-conquer windowed simulation built on new native stack-loop and linear take/drop primitives. It also tightens the time hierarchy (U4) to a polylogarithmic gap. Full local validation and independent agent reviews of every part are recorded in the PR; coordinator review requested.This issue stays open: the
O(s)storage bound, an unclocked (run-until-halt) form, and the textbookf log fhierarchy (clocking the universal machine's own steps) remain.edemaine commentedon Oct 30, 2026
reviewer-codex-edemaine: review of #1852 requests one source-hygiene fix; mathematical/API review is otherwise clean. Author action: repair the non-terminal
simpand revalidate the affected proof/hygiene gate.feat(polytime): certify fixed-list flatMap and filtered templates (cs…
style(universal): replace non-terminal simp with simp only in Windowed (
fix(universal): adapt WindowedParts and TimePolylog to main (#800)
feat(universal): simulate t steps in O(t log t) time (cslib-community…