Iterating a polynomial-time function in polynomial space #
⚠️ Unreviewed by Bolton
A language decided by iterating a polynomial-time function on a polynomially
bounded state is in PSPACE, however many iterations it takes: the state is the
only thing that has to be stored, and the iteration count lives in a binary
counter of polynomially many bits. This is the machine-independent way into
PSPACE, the counterpart of what Cobham's theorem does for P — and it is what
Savitch's theorem needs, since Savitch's recursion is a stack machine whose step
is polynomial-time and whose stack is polynomially bounded.
The machine reuses the iteration machinery of
Complexitylib.Classes.P.Cobham.Internal.Iterate wholesale, on that file's own
layout: Cobham.iterSetup puts pair [] x in place, Cobham.iterTail builds
the entry shape, and Cobham.iterBody applies the function once and restores
it. Only the loop driver changes. TM.forRegTM counts in unary, which cannot
reach 2 ^ poly, so the loop here is TM.loopTM, as in PP ⊆ PSPACE and
PH ⊆ PSPACE.
No tape is added #
Two of the layout's tapes are free for the loop's own use, so the machine needs
no tapes beyond the ones Cobham.iterBody already has — and therefore no
placement, and no parking of tapes a placement would freeze.
Cobham.resIdx, the result tape, is blank at the start of every iteration:TM.applyPreputsparkedBlankthere. That is the source the verdict cell is cleared from.Cobham.rfIdx, the fuel register of the unary loop that is not running here, is held fixed byCobham.iterBodywhatever it contains. That is where the iteration counter lives.
The machine never reads the counter: it is there so that
TM.loopTM_hoareTime_indexed can read the iteration index off the tapes for its
termination measure, which is why it may be binary and cost only polynomially
many cells.
The loop's shape #
The programmed function signals completion by putting a 1 at the head of its
state, and the loop's test is TM.writeOutputBitTM reading the state tape's
first cell — so the loop runs until the computation says it is done, and the
number of iterations never has to be represented. One more application after the
loop puts the verdict at the head of the state, and a second
TM.writeOutputBitTM publishes it.
Main definitions #
Complexity.SpaceIter.slotOf— the verdict cell as a tapeComplexity.SpaceIter.headSym— the symbol at the head of a stateComplexity.SpaceIter.iterBank— the tape family of an iterationComplexity.SpaceIter.bodyTM,testTM— the loopComplexity.SpaceIter.prologueTM,epilogueTM— the two endsComplexity.SpaceIter.spaceIterTM— the whole machineComplexity.SpaceIter.windowBound— the polynomial window it keeps
Main results #
Complexity.SpaceIter.bodyTM_hoareTime— one pass applies the function onceComplexity.SpaceIter.testTM_hoareTime— the test publishes the state's headComplexity.SpaceIter.loop_hoareTime— the loop runs until the state is doneComplexity.SpaceIter.loop_keepsWindowOn— one pass' width bounds the whole loopComplexity.SpaceIter.spaceIterTM_hoareTime— the machine publishes the answerComplexity.SpaceIter.spaceIterTM_keepsWindow— and keeps a polynomial windowComplexity.SpaceIter.mem_PSPACE_of_iterate— so the language it decides is inPSPACE
The verdict cell #
The output tape holding s in its verdict cell.
Equations
Instances For
The symbol at the head of a state #
The symbol at the head of a state tape: the state's first bit, or blank.
Equations
Instances For
Reading the iteration index off the tapes #
TM.loopTM_hoareTime_indexed needs the iteration index as a function of the
configuration, for its termination measure. The counter carries it; this is the
ghost read, and nothing computes it.
The value a canonical binary register holds.
Equations
- Complexity.SpaceIter.ctrValue t = if h : ∃ (v : ℕ), t = Complexity.natTape v then h.choose else 0
Instances For
The loop's index function: how far the counter has advanced past start.
The input and output tapes are ignored, but TM.loopTM_hoareTime_indexed takes
the index as a function of the whole configuration, so they have to be there.
Equations
- Complexity.SpaceIter.loopIdx k start x✝¹ work x✝ = Complexity.SpaceIter.ctrValue (work Complexity.rfIdx) - start
Instances For
The tapes of an iteration #
The tape family at an iteration: the entry shape for y on the application
block, the counter on the fuel register, and the two fixed tapes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A block family is the iteration bank as soon as it has the right tapes.
The machine #
The loop body: clear the verdict cell, apply the function once, bump the counter.
Equations
Instances For
The loop test: publish the head symbol of the state.
Instances For
The body's contract #
Clearing the verdict cell, from the blank result tape.
Applying the function once.
Bumping the counter.
The loop body's contract.
The test's contract #
The loop's test. It publishes the state's first symbol; the programmed
function signals completion by putting a 1 there.
The loop #
The verdict cell at the start of a pass: blank before the first test, the previous test's verdict afterwards.
Equations
Instances For
The tapes between the body and the test of a pass: the entry shape for the next state, with the verdict cell cleared.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The body of a pass applies the function once and bumps the counter.
The tapes between the body and the test are parked.
One pass of the loop. The body applies the function once, and the test finds the state not yet done, so the loop comes back to its start state one iteration on.
The last pass of the loop. The body applies the function one final time, and the test finds the state done, so the loop halts.
The loop's contract. The loop runs until the state says it is done: N
passes, each applying the function once.
The loop's window. Every configuration the loop passes through lies within one pass of an indexed state, and each indexed state has every head parked at cell one, so a window one pass wide holds for the whole run — however many passes it takes.
The prologue #
Cobham.iterSetup puts pair [] x on the result tape with the bookkeeping
registers loaded, and Cobham.iterTail turns that into the entry shape the loop
starts from — exactly the two phases Cobham.iterTM opens with.
The prologue: the setup, then the tail that builds the entry shape.
Equations
Instances For
The prologue's running time, which is also the width its window needs.
Equations
- Complexity.SpaceIter.proBound k p H n = Complexity.setupBound p n + 1 + Complexity.tailBound k H (n + 2)
Instances For
The counter's starting value. Cobham.iterSetup leaves |x| in unary on the
fuel register, and a unary register of n ones read as a binary numeral is
2 ^ n - 1.
Equations
- Complexity.SpaceIter.startCount n = 2 ^ n - 1
Instances For
The prologue's contract. From the initial configuration's tapes it reaches
the loop's entry state for pair [] x, with the counter at startCount |x|.
The epilogue #
The loop leaves the state saying it is done; one more application turns that state into the one whose head is the answer, and one more publication puts it in the verdict cell.
The epilogue: one more application, then publish the state's head.
Equations
Instances For
The epilogue's contract.
The whole machine #
The iteration machine: prologue, loop, epilogue.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole machine's contract. From the initial tapes on x it halts with
the head symbol of Y (N + 1) in the verdict cell, where Y is the orbit of the
programmed function through pair [] x and N is the first positive index at
which the state says it is done.
The machine's window #
The prologue and the epilogue are short, so their windows come from their running times. The loop's does not — it runs for as long as the programmed computation does — but every configuration it passes through is within one pass of an indexed state whose heads are all parked, so one pass' width is enough.
A halting contract, read as a reachability fact about a configuration already in the machine's start state.
The whole machine's window.
Iterating a polynomial-time function in polynomial space #
Everything above is stated for an explicit H, N and per-pass bound b. Here
they are supplied: H is the padding polynomial of Cobham.iterTM, b is one
pass' running time, and the window is their sum — a polynomial, because the only
unbounded quantity, the iteration count, enters only through the number of bits
of the counter.
One pass' running time, as a function of the input length: an application of
the programmed function, the tail that restores the entry shape, and an increment
of a counter of n + w(n) + 1 bits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The machine's window: the prologue, and one pass.
Equations
- Complexity.SpaceIter.windowBound k tp p r w n = Complexity.SpaceIter.proBound k p (Polynomial.eval n p) n + 1 + Complexity.SpaceIter.passBound k tp p r w n
Instances For
Iterating a polynomial-time function on a polynomially bounded state is in
PSPACE, however many iterations it takes. The function is applied to
pair [] x over and over; it signals completion by putting a 1 at the head of
its state, and the head of the state one application later is the answer.