The clocked program lays its file out #
The file-laying phase, assembled: the run
(DescriptiveComplexity.Draw.Prog.reachesIn_buildFile) at the layout of
DescriptiveComplexity.Draw.Data.blkLaid, the write and the pointer of
DescriptiveComplexity.Draw.Data.buildSpec, and the rules of
DescriptiveComplexity.Draw.Data.nexRule.
What ties them is that a sweep of the file's stretch is a walk of the file:
every address the sweep stops at is some register's cell
(DescriptiveComplexity.exists_ixSegCell_eq), and the address it moves to is
the cell of the register the pointer moves to
(DescriptiveComplexity.wmIncr_ixSegCell). So the phase and the control at an
address are read off the register that address is – the block into the phase,
the tuple into the control – and the step the sweep asks for is one of the
three rules at that phase, chosen by whether the pointer's tuple is the last of
its block.
What the run asks of the tape outside the stretch is that it be what the background says there, not that it be blank: the marker is planted before the file is laid, and the marker's cell lies below the file.
The run is DescriptiveComplexity.Draw.Data.reachesIn_buildBlkFile, and what
it costs is the stretch: one step per register, which is
(|K| + 1) · |A| ^ dd₀ of them (DescriptiveComplexity.card_blkFile).
The guessing phase is the same walk over the same registers, writing at each
the value the certificate has there
(DescriptiveComplexity.Draw.Data.reachesIn_guessBlkTracks); it exists for
every certificate, which is what makes it a guess. Only the write differs, so
the two share the pointer, the phase family and the step's case analysis.
After either sweep the machine stands one cell past the file: it steps back onto
the last register (DescriptiveComplexity.Draw.Data.step_doneBack) and walks
down to the marker (reachesIn_homeAfterBuild), which is
DescriptiveComplexity.Draw.HomeKit's walk at the file's own top.
The three chain into DescriptiveComplexity.Draw.Data.reachesIn_buildPhase,
whose budget is 2 · card + base: the stretch out and back, the turn-around,
and the descent from the file's foot to the marker.
DescriptiveComplexity.Draw.Data.reachesIn_guessPhase is the guess's copy of
that, at the same number – it is the same walk.
The three single steps that join the phases are here as well:
DescriptiveComplexity.Draw.Data.step_startBuild plants the marker and enters
the file, step_homeBuildExit turns round at the marker and re-enters it for
the guess, and step_homeGuessExit enters the evaluation. The whole opening is
those five legs, and DescriptiveComplexity.TMData.reachesIn_five adds them up:
twice a phase and three steps.
The register an address is, where it is one: what the pointer holds when the sweep stands there.
Equations
- DescriptiveComplexity.Draw.Data.regAt F dflt r = if h : ∃ (v : I), r = F.cell v then h.choose else dflt
Instances For
Dependency graph
The step the sweep asks for, at a register #
The phase and the control at an address #
The phase at an address: the sweep's phase at the block of the register it is, and the turn-around phase off the file – which is where the sweep's last step lands. Both sweeps use it, at their own two phases.
Equations
- DescriptiveComplexity.Draw.Data.phAt G blk inb done r = if h : ∃ (v : J), r = G.cell v then inb (blk h.choose) else done
Instances For
Dependency graph
The written symbol #
The run #
The clocked program lays its file out: from the first register's cell to the address one past the last, one step per register, turning the blank the tape starts with into the background of the file it has built.
The run is DescriptiveComplexity.Draw.Prog.reachesIn_buildFile's, at the layout
of a clocked program's file, with the write and the pointer of
DescriptiveComplexity.Draw.Data.buildSpec and the rules of
DescriptiveComplexity.Draw.Data.nexRule; what it costs is the stretch, one
step per register.
Dependency graph
The guessing sweep #
The same walk over the same registers, with DescriptiveComplexity.Draw.Data.guessSpec
in place of buildSpec: what changes at a cell is the stage tracks, and which
value is written there is a shape of the rule, so the sweep is the program's
one nondeterministic phase. The steps below are the build's with the guessed
value carried along.
The clocked program guesses its certificate: the same walk over the same registers as the file-laying sweep, writing at each the value the certificate has there. Which value that is, is the rule's shape, so the run exists for every certificate – which is what makes the phase a guess and the program nondeterministic exactly here.
Dependency graph
The turn-around and the walk home #
The turn-around after a sweep: standing one cell past the file in the done phase, the machine steps back onto the last register, and its walk home begins there. The step writes nothing, so both sides read the same tape.
Dependency graph
The whole opening phase: from the first register's cell with the pointer at the first register, the machine lays the file out, turns round one cell past it, and walks home to the marker – in twice the file's length and its base, which is the stretch out and back with the turn-around and the descent below the file.
Dependency graph
The whole guessing phase: the same three legs at the guess's own phases, and the same count – the guess is the file-laying walk with a different write, so it costs exactly what that one costs.
Dependency graph
The opening step: from the empty address the machine plants the marker and moves right, into the walk that takes it to the file's base. The base is above the program's data, so it is not the marker's neighbor and the walk is not a step.
Dependency graph
The opening's steps, at any file #
The five steps above read the file only through the presentation of the tape –
Prog.trackTapeAt cell … – so they hold at whatever cells a program's file has.
A program that is handed its file (DescriptiveComplexity.WideRegAccept) uses
them at the channel's cells, where a program that lays one uses them at
DescriptiveComplexity.Draw.Data.blkLaid. Nothing but the presentation
changes, and the two sweep sites the steps mention are parameters already.