theoremroutinestructure_uncertain

Effective compiler from randomized to deterministic logspace

Computes from M,a,bM,a,b a deterministic machine in Klog⁡(n+2)K\log(n+2) space deciding L(M)L(M)
explicit uniform form of the derandomization
Theorem·thm:effective-simulation·§13 The effective compiler

Statement (paper)

There is a terminating algorithm which, given a finite randomized machine description MM and positive integers a,ba,b, emits a deterministic machine DMD_M and positive integers K,H,cK,H,c with the following guarantee. If, on every input of length nn and every random tape, MM halts within (n+2)a(n+2)^a steps, uses at most b⌈log⁡(n+2)⌉b\lceil\log(n+2)\rceil work bits, and has acceptance probability at most 1/31/3 on no inputs and at least 2/32/3 on yes inputs, then DMD_M decides the same language. On each input, that same execution uses at most Klog⁡(n+2)K\log(n+2) work bits and H(n+2)cH(n+2)^c elementary bit operations.

In plain English

There is a terminating algorithm that, given a randomized machine description MM and integers a,ba,b, outputs a deterministic machine DMD_M and constants K,H,cK,H,c. If MM halts within (n+2)a(n+2)^a steps, uses at most b⌈log⁡(n+2)⌉b\lceil\log(n+2)\rceil work bits, and has two-sided error 1/31/3 on every input, then DMD_M decides the same language using at most Klog⁡(n+2)K\log(n+2) work bits and H(n+2)cH(n+2)^c bit operations.

Why it's here

This is the paper's explicit, uniform form of the derandomization: the machine DMD_M and its constants are computed from M,a,bM,a,b. The proof pads the input so a fixed interpreter simulates MM exactly, applies the fixed-accuracy library algorithm from the fixed-precision theorem to the padded input, compiles reads of the virtual padded input as callbacks, and bounds total space and time by configuration counting.
Classified routine:
This is a uniform, effective repackaging of the fixed-precision approximation theorem (thm-fixed-precision). It uses standard padding, a fixed interpreter, logspace composition via callbacks, and configuration counting for the space and time bounds.

Uses

thmDeterministic logspace approximation of acceptance probability

Used by

Nothing in the paper

Inside the proof

claimFixed deterministic library decides interpreter promiseclaimPadding preserves acceptance probability exactlyclaimCallback compiles virtual padded input readsclaimSimultaneous work-space bound on all tapesclaimBit-time bound by configuration counting

Sources

PaperOpen
Section
§13 The effective compiler
Page
—
Label
thm:effective-simulation
Line
sections/compiler.tex:8
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    structure_uncertain
    The proof environment is only a 25-line 'Completion'; the substantive argument is spread over Sections 13.2–13.5 (compiler.tex 193–530), outlined here under this label.
  • info
    structure_uncertain
    claim "Fixed deterministic library separating interpreter thresholds" (sections/compiler.tex:193-251) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Padding preserves acceptance probability exactly" (sections/compiler.tex:256-312) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Callback compiles virtual padded input reads" (sections/compiler.tex:353-429) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Simultaneous work-space bound for all tapes" (sections/compiler.tex:452-471) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Bit-time bound by configuration counting" (sections/compiler.tex:473-530) lies outside the recorded proof; a second proof or an appendix