Machines that respect a space window #
A TM.HoareSpace contract bounds every configuration reachable from a start state, which makes
it awkward to compose: the body of a loop is entered again and again, never from its own start.
The step-local strengthening below composes freely. A machine respects a window when one step
from any configuration inside the window lands inside the window again — regardless of where in
its own execution it happens to be.
Respecting a window immediately gives a space contract, and the property is inherited by the loop
combinator from its body and test, because every phase loopTM interposes between them idles the
input and work tapes (TM.loop_head_bound). This is what lets a loop run for as long as it likes
without its space bound growing.
TM.RespectsWindow is the step-local form, convenient when it applies. It is too strong for a
machine that simulates another one, whose own space bound holds only along its own run, so the
weaker TM.KeepsWindow — started anywhere inside the window, everything reached stays inside —
is the notion the composition rules are stated for. Every entry into a loop body is at its start
state, so this is exactly as much as a loop needs.
A subroutine that simulates another machine is not robust even in that sense: run from a start
whose scratch tapes hold garbage, the simulated machine is not on any run its own space bound
covers. TM.KeepsWindowOn therefore carries a precondition on the starting tapes, which a
composition rule must re-establish at each entry from the previous stage's postcondition —
and TM.halted_unique is what makes such a postcondition usable, since it says the halted
configuration a stage reaches is the only one.
The two forms meet at TM.seqTM_keepsWindow_of_post: a stage that needs blank scratch, prefixed
by a stage that clears it, is robust again. So a loop body assembled that way satisfies the plain
TM.KeepsWindow hypothesis of TM.loopTM_keepsWindow, and no precondition-carrying loop rule is
needed.
Main definitions #
TM.RespectsWindow— one step from inside the window stays inside itTM.KeepsWindow— from any windowed start, every reachable configuration is windowedTM.KeepsWindowOn— the same, restricted to starts satisfying a precondition
Main results #
TM.hoareSpace_of_respectsWindow— respecting a window is a space contractTM.decidesInSpace_of_respectsWindow,TM.decidesInSpace_of_keepsWindow— a window turns a decider into a space-bounded deciderTM.halted_unique— a deterministic run reaches at most one halted configurationTM.keepsWindowOn_of_haltsIn,TM.keepsWindowOn_of_hoareTime,TM.keepsWindowOn_of_hoareTime_pinned— any time-bounded subroutine, and anyTM.HoareTimecontract, acquires a window contractTM.KeepsWindowOn.hoareSpace,TM.KeepsWindow.hoareSpace— a window contract is aTM.HoareSpacecontract, so the two styles interoperateTM.seqTM_respectsWindow,TM.loopTM_respectsWindow— the step-local form composesTM.seqTM_keepsWindow,TM.ifTM_keepsWindow,TM.loopTM_keepsWindow— and so does the usable form, for all three control-flow combinatorsTM.seqTM_keepsWindowOn— and the precondition-carrying form, for sequential compositionTM.seqTM_keepsWindow_of_post— the bridge: prefixing a precondition-needing stage with a robust one yields a robust composite, which the unconditional loop rule accepts
The tapes of a configuration all carry their left-end markers.
Equations
- Complexity.TM.CfgStartInvariant c = (c.input.StartInvariant ∧ (∀ (i : Fin n), (c.work i).StartInvariant) ∧ c.output.StartInvariant)
Instances For
The machine respects a space window: one step from any configuration inside the window
lands inside the window again — including the output head, so the discipline is the one
TM.DecidesInSpace asks for. Unlike TM.HoareSpace this says nothing about where the machine
started, so it survives being re-entered, which is what a loop body needs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The start-marker invariant is preserved by a step.
Respecting a window is a space contract.
Sequential composition inherits the window. The one step interposed between the two machines idles every tape, so it cannot push a head outward.
The loop inherits its window from its body and test. Every phase loopTM interposes
between the two idles the input and work tapes, so the interposed steps cannot push a head
outward; the simulated steps are covered by the parts' own contracts. The bound is therefore
independent of how many iterations run.
Determinism at the halt #
A deterministic run reaches at most one halted configuration: the halt is the run's endpoint, whichever way it is reached. This is what lets a stage's postcondition be used — the configuration a composition rule meets at the phase boundary is the one the stage's Hoare triple describes.
Keeping a window along a run #
The machine keeps its window: started anywhere inside the window with its left markers
intact, every configuration it reaches is still inside the window. This is weaker than
TM.RespectsWindow — it says nothing about configurations the machine cannot reach from a
windowed start — and it is what a subroutine that simulates another machine can actually
satisfy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A machine that never steps out of the window certainly keeps it.
Sequential composition keeps the window. Each phase is entered at its machine's start state with windowed tapes, and the single interposed step idles every tape.
The loop keeps the window, however many iterations it runs. Body and test are each entered at their own start state with windowed tapes, and every step the loop interposes between them idles the input and work tapes, so nothing accumulates across iterations.
The conditional keeps the window. Test and branch are each entered at their own start state with windowed tapes, and the steps between them idle every tape.
The machine keeps its window on runs that start from a configuration satisfying pre.
The precondition is what a subroutine simulating another machine needs: its space bound only
covers runs whose scratch tapes started blank, so a composition rule has to re-establish that at
every entry.
Equations
- tm.KeepsWindowOn pre inputLength space = ∀ (c : Complexity.Cfg n tm.Q), pre c → ∀ (c' : Complexity.Cfg n tm.Q), tm.reaches c c' → c'.WithinDecisionSpace inputLength space
Instances For
Keeping the window unconditionally is keeping it on any precondition that pins the start state and the window.
Weakening the precondition of a windowed contract.
Sequential composition keeps the window, with preconditions. The second machine's
precondition is re-established from the first machine's postcondition: TM.halted_unique says the
configuration met at the phase boundary is the very one the first machine's Hoare triple
describes, and the interposed step transforms its tapes in the fixed way transitionTape records.
A sequential composition is robust as soon as its first stage is. This is what makes the
unconditional rules usable in practice. A subroutine that simulates another machine needs its
scratch tapes blank, so it only satisfies the precondition-carrying contract; but prefix it with a
stage that clears the scratch — one that is robust — and the composite is robust too, because
the first stage's postcondition supplies the second stage's precondition. The composite can then
be dropped straight into TM.loopTM_keepsWindow, whose body hypothesis is the unconditional one.
Time-bounded subroutines keep a window #
A subroutine that halts in t steps keeps a window t cells wider than its start.
Every head moves at most one cell per step, and a deterministic run cannot outlast its halt, so a
configuration starting with its heads inside h can only have pushed them to h + t.
This is the bridge from the library's existing time contracts: any subroutine with a
TM.HoareTime-style halting bound acquires a window contract, with no new tape analysis.
Every TM.HoareTime contract yields a window contract. The library's subroutines are
specified by halting-time triples; this converts any of them, with no tape analysis, provided the
precondition pins where the heads start. The window is the starting bound plus the running time,
since a head moves at most one cell per step.
The pinned form, matching how the library states its framed subroutine contracts: the precondition names the three tapes exactly, so the head bounds are three facts about literals.
The unconditional form: a machine that halts within t steps from every configuration
inside the window keeps the widened window.
Interoperation with the library's space contracts #
A window contract is a TM.HoareSpace contract. TM.HoareSpace is the library's own
anchored space judgement; it bounds Cfg.WithinAuxSpace, which ignores the output tape, whereas
a window additionally bounds the output head as TM.DecidesInSpace requires. So a window is the
stronger statement, and anything established with the composition rules above can be handed to
TM.seqTM_hoareTimeSpace and TM.computesInSpace_of_hoareTimeSpace.
The unconditional form likewise yields a TM.HoareSpace contract, on any precondition that
pins the window and the left markers.
From a window to a space-bounded decider #
The initial configuration parks every head at the left end, so it sits inside every window.
Every tape of the initial configuration carries its left-end marker.
A machine that respects its window and decides L decides L in that space. This is the
landing gear: a construction assembled from TM.seqTM_respectsWindow and
TM.loopTM_respectsWindow needs only its correctness proof to become a DSPACE membership.
A machine that keeps its window and decides L decides L in that space.
A loop keeps a window one iteration at a time. The loop's total run is exponentially
long when the counter is, so no bound of the form "space ≤ time" can help. What is true is that
every configuration the loop passes through lies within one iteration of some indexed state, and
each iteration is short: hiter asks only that a single iteration stay inside the window.
Determinism is what makes the reduction work. A run that leaves the current iteration must pass through the next iteration's start configuration, because two runs from the same configuration are prefixes of one another.
A loop whose indexed states are parked keeps a window of one iteration's width. Inside a
single iteration no head can travel further than the iteration is long, and each indexed state
has every head at cell one, so 1 + b cells suffice — for the whole run, however many iterations
it takes.
Widening the window of a conditional window contract. Composing stages of different widths means widening each to their maximum first.
The tape conditions a loop configuration must satisfy for the phase-based window rule: the body and the test are entered on tapes their own window rules accept, and the bookkeeping phases between them on tapes that carry those conditions along.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A loop keeps a window, given windows for its phases. TM.loopTM_keepsWindow asks each
phase to keep the window from any windowed configuration, which a phase that simulates another
machine cannot promise: started anywhere, such a machine need not even halt. This rule asks
instead for a window on the states each phase is actually entered at, plus three obligations
saying that the loop's own steps between phases carry those states along.
PB and PT describe the tapes the body and the test are entered with, PL those of the
rewind-and-check phases between them.
A bookkeeping step of a loop moves only the output head. Between the test and the next iteration the loop rewinds its output tape and reads one cell; the work tapes and the input are idled, and the output's contents are written back unchanged.
Where a rewind step goes. It keeps rewinding until the output head reads the marker, and then moves on to the check.
A check step leaves every tape exactly as it found it, when the output head is off the marker — which it is, since the rewind has just put it at cell one.