The clocked program's whole run, and its clock #
The two halves are counted separately – the opening and the evaluation
(DescriptiveComplexity.Draw.Data.nexEval_reachesIn) – and this file puts
them together and compares the sum with the clock.
The opening is DescriptiveComplexity.Draw.Data.reachesIn_openingRegion,
here: the approach walk up to the file's base, the file-laying sweep, and the
guess along the region below the file – one bit per address, which is what the
guessed relations are – for
2·R + 2·base + (the guessed stretch out and back) + 4, and openingRegion_le
bounds that
by the number of addresses.
Two things are worth naming. The presentation bridge: the opening is stated
with the tape walked along the mirror track and the evaluation along VAL, and
the two are the same tape whenever both marks are the background's own
(DescriptiveComplexity.Draw.trackTape_of_back), so the caller hands that
equality over rather than either run being restated. And the arithmetic:
the total is «opening + rounds × width», which is mul_add_lt_two_pow's shape –
so what the clock asks is that the opening and each of the evaluation's two
factors fit the region, with one surplus block of slack for the additive term.
The opening is a bare number there
(nexTotal_lt_two_pow), so either shape of it is compared the same way.
The initial end is here as well, and it is three small facts.
DescriptiveComplexity.Draw.Prog.trackTapeAt_initBack says the all-blank tape is
the pass-layer presentation at any file – which a clocked program needs,
because its file does not exist at time zero – and
DescriptiveComplexity.Draw.Data.startBack with startBack_frame /
startBack_wr is the background the opening's first step leaves: the one it
started from with the marker planted, which is the frame condition and the write
that step asks for.
The forward direction lands here too (nexProg_wideAccept): an accepting run
of fewer than 2 ^ n steps from the initial configuration is a yes-instance of
DescriptiveComplexity.WideAccept. Two of its hypotheses are rfl at the
assembled program, and that is the point of the program declining the input
channel's marks: with mark the blank, the tape is blank everywhere at time
zero and the channel's ruler is not there to be mistaken for a register
(trackTape_blank_congr for the presentations).
The backward direction's foundation is here as well: nexProg_sepOn – the
program separates at every post-guess phase, across sites by the owner map and
within a site by nexSep_postGuess – and nexProg_uniqueFrom, which is what a
reduction reads its certificate off an arbitrary accepting run with. The fact
it stands on – that the evaluation's rules never leave the post-guess phases –
is proved, not assumed:
nexEvalRuleF_postGuess, and under it a chain of «this machinery leaves only
into its own phases or its exit» lemmas, one per builder, down to the trips.
The clocked program's run, summed: the opening, the evaluation and the
step that leaves it. Nothing here is about the program – the three legs are the
caller's – and what it records is the arithmetic: an opening of o, an
evaluation of e, and one step to accept.
Dependency graph
Two presentations of one tape: a run stated along a track whose digits the background already carries is the same tape as one stated along another such track, so a leg walking the mirror composes with a leg walking VAL without either being restated.
Dependency graph
The mirror and VAL presentations agree: the opening walks the mirror and the evaluation walks VAL, and both marks are the state's own, so the two runs compose with no rewriting in between.
Dependency graph
The opening leaves the tape the evaluation starts from: the opening
walks the mirror at the empty mark, the evaluation walks VAL at the state's own,
and the state whose mirror is empty presents the same tape either way. This is
the one rewrite between reachesIn_openingRegion and
DescriptiveComplexity.Draw.Data.nexIxEvalB_reachesIn.
Dependency graph
The opening's last configuration is the evaluation's first: same phase,
same head, and the same tape – the opening presents it along the mirror at the
empty mark, the evaluation along VAL at the state's own, and a state whose
mirror is empty presents both the same way. This is the junction of the two
legs: with it the whole run is hopen.trans heval, and
DescriptiveComplexity.Draw.Data.nexProg_wideAccept_of_legs does the clock.
Dependency graph
A blank tape is any presentation of the blank background: a program that
declines the input channel's marks starts with every cell blank, and that tape
is what a run stated along any clear track begins from. This is the bridge
between the initial configuration
(DescriptiveComplexity.Draw.Prog.wideAccept_prog presents it along the
channel's file) and the opening's own presentation along the mirror.
Dependency graph
A tape walked along an empty track does not depend on which file presents
it: the only cell-dependent part of the presentation is the bit at the walked
mark, and an empty mark has none. This is the bridge a program handed its file
needs, where trackTape_blank_congr is the one a program starting on a blank
tape needs: there the background is the blank, here it is the channel's own
marks, and neither is read by the presentation.
Dependency graph
The opening, with the guess over the region #
The background the opening's first step leaves: the one it started from,
with the marker planted at the address the head is on. A clocked program starts
on a blank tape, so this – with DescriptiveComplexity.Draw.Prog.initBack for the
background – is what its opening runs from.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
Planting the marker changes nothing elsewhere: the frame condition of the opening's first step.
Dependency graph
Planting the two marks is the write the opening's first step makes: at the address the head is on, the presentation with them is the presentation without them, updated at the marker slot and at the bottom mark's.
Dependency graph
The state a clocked program starts in #
Its first step plants the marker at the empty address and nothing else has been
written, so the state is clear but for the marker – and its background is the
blank tape everywhere off the file, which is what the opening's frame
hypotheses (hbelow, habove, hwr) ask of the caller.
The state a clocked program enters its opening in: every register and every track clear, the marker and the bottom mark at the address the head stands on – the two the opening's first step writes, and the two the evaluation's walks read.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The clocked program's opening: the opening step, the approach walk up to the file's base, the file-laying phase, the walk home with the turn into the guess, the region-wide guess with its stop and its own walk home, and the dispatch into the evaluation.
The file is laid above the program's data and the certificate is guessed below it, which is what lets a stage atom seek to a dictionary entry: the entry is a logical address and every logical address is below every register. The approach is the price of that arrangement – the base is not the marker's neighbor, so getting there is a walk and not a step – and where it stops is the program's choice, a machine having no landmark but the cell it started on.
Dependency graph
What the guess writes #
The stage tracks a clocked program guesses are an assignment's, restricted to
the stretch the guess sweeps – the file's first register up to the end marker.
Restricting them is what makes the opening's frame condition true (outside that
stretch the tracks are the entry state's, which is empty), and it costs the
dictionary nothing, since every entry the evaluation reads is inside the stretch
(a track marks no empty address, nonempty_of_trackOf).
The tracks the guess writes: an assignment's, inside the swept stretch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
Outside the swept stretch the guess writes nothing – the opening's
hout, at tracks that are an assignment's inside it.
Dependency graph
Below the guess's top the tracks are the assignment's, and nothing has to
be said about the bottom: a track marks no empty address
(nonempty_of_trackOf), so an address it marks is at or above the marker's
neighbor by wmSetLe_succ_bot_of_nonempty, which is where the guess begins.
This is the hdict an evaluation asks for, and it asks of the data only what
wmSetLt_ixStageTgt_logicalTop already proves: that a dictionary address is
below the last logical one.
What it asks of the reduction is that every fixed-point variable have an argument. A nullary one has the empty address for its entry, which is the marker's own cell and below every stretch the machine writes; padding its relation with a dummy argument costs nothing and is the intended reading.
Dependency graph
The dictionary the evaluation reads, off a tape state: the same reading
as guessTracks_iff_of_lt, at a state whose stage tracks are the guess's. Every
leg of the spine leaves them alone (ixSpineStOfB_old), so this is what the
evaluation's hdict is discharged by, at whatever program and whatever rule
names the reduction runs – nothing here mentions either.
Dependency graph
The opening of a program that is handed its file #
A program handed its file has nothing to lay: its file-laying phase is the two
steps of nullSpec and the rest of the opening is the same. So the whole
opening is stated here at an arbitrary file – the five steps of
NexBuild's AnyFile section, the sweep that is over at once, the two walks
home and the guess, which was generic already. Nothing of the file is read but
its cells.
The whole opening of a program that is handed its file: plant the two marks, walk up, run the sweep that lays nothing, turn round, walk home, guess the certificate over the stretch, walk home again, and step into the evaluation. Its cost is the two walks up and back, the guess's stretch out and back, and six single steps.
Dependency graph
The tail of the opening, from the walk home after the guess. The whole
opening is a forward run, but a backward reading of an accepting run does not
get the opening: it gets the first configuration the machine cannot leave, which
is where the guess stopped and the walk home begins
(DescriptiveComplexity.Draw.Data.exists_postGuess_shaped). From there on the
run is forward again, and this is that piece: walk down to the marker from
wherever the guess stopped, and step into the evaluation.
Nothing of the guess is read here – the tracks are whatever the sweep left – so the same lemma serves the forward opening's last two steps and the backward reading's first.
Dependency graph
The clock comparison: an opening of o steps, an evaluation of at most
a · b, and the accepting step come to fewer than 2 ^ ((k + j) · m) as soon as
each of a, b and o + 1 is at most 2 ^ (k · m) and j outruns k by two.
The opening is left abstract: the file-laying one and the region-guessing one
differ, and both are bounded by the number of addresses.
Dependency graph
The clock comparison, with the opening at twice the region: the shape a
program that lays a file and guesses over the region actually meets – its
opening is two sweeps, not a fraction of one. One working block is enough
(1 ≤ k), and the rest is mul_add_lt_two_pow'.
Dependency graph
The opening fits the region a few times over: the approach, the file's
own stretch and the guess all stay inside the region, so with each of the
program's numbers below the region's size 2 ^ (k · m) and a block worth at
least eight addresses (3 ≤ m), the whole opening and the step that follows it
are below 2 ^ ((k + 1) · m) – which is what
DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow' asks of it. The region
bound on a rank is wideRank_lt_two_pow_supported; the base is bounded the same
way, being an address of the region like any other.
Dependency graph
The region-guessing opening is bounded by the addresses: its two sweeps
are each shorter than the number of addresses, so the whole of it is
2 · R + base + 2 · N + 4 for N that number. This is the crude reading, above
the clock; openingRegion_le_two_pow is the one a clocked program can pay.
Dependency graph
The forward direction at the assembled program #
A clocked program starts on a blank tape: it declines the input
channel's marks – its mark is the blank – so its initial background is the
constant blank, and the tape it starts on is the one its opening runs from
whatever file it means to lay.
Dependency graph
The clocked program's run makes its instance a yes-instance: an
accepting run of fewer than 2 ^ n steps from the initial configuration – the
head on the empty address, the tape blank because the program declines the
channel's marks – is what DescriptiveComplexity.WideAccept asks for.
Well-formedness comes free with the table and determinism is not asked for,
which is exactly what a program that guesses needs.
Dependency graph
The clocked program accepts, from its three legs: the opening, the
evaluation and the step that leaves it, with the clock's arithmetic done once.
What the two strands above owe is exactly what this asks: an opening of o
steps with o + 1 below 2 ^ ((k + 1) · m) – two sweeps of the region, which
is what laying the file and guessing over it costs – an evaluation of at most
a · b with both factors below 2 ^ (k · m), and k + 1 < j with one working
block; then the whole run is below 2 ^ ((k + j) · m), hence below the number
of addresses (DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow').
Dependency graph
The clocked program accepts, from its opening and its evaluation: the
two legs as they are actually proved – the opening from the state the program
starts in, presented along the mirror at the file it lays, and the evaluation
from the state the opening leaves, presented along VAL – with the two
adjustments between them done here. There are exactly two: the initial tape is
the blank one whatever track and whatever file it is presented along
(trackTape_blank_congr at nexProg_initBack), and the opening's last
configuration is the evaluation's first, because the state the opening leaves
has an empty mirror (config_openingEnd_eq_evalStart). The clock is
nexTotal_lt_two_pow', one step of slack over the run since the evaluation
already ends in the accepting phase.
Dependency graph
Determinism after the guess #
The clocked program separates after its guess: two of its rules firing
in the same post-guess phase on the same data are the same rule. Across sites
that is the owner map (nexOwner_nexRule); within a site it is
nexSep_postGuess, and the guess site is where the two are allowed to differ –
which is why the phase restriction is there.
Dependency graph
The clocked program is deterministic after its guess: from any configuration whose phase is post-guess, every reachable configuration has at most one successor. This is what a reduction reads its certificate off an arbitrary accepting run with – determinism where it is needed and nondeterminism where the guess is, which is the whole of the polarity.
Dependency graph
No rule of the clocked program fires from its accepting phase: the
accepting phase is owned by the accepting site (nexOwner), and that site has
no rules at all – its shape is Empty.
Dependency graph
An accepting configuration of the clocked program is stuck: no rule
fires from the accepting phase, so the run that reached it is the whole run.
This is what a backward reading needs of the verdict: an accepting run ends
where the evaluation's own run ends, and the two are the same run by
nexProg_uniqueFrom.