Where a backward reading of an accepting run starts #
A run that accepts ends in NexPh.acceptP, which is one of the phases the
program can never leave (NexPh.PostGuess). So somewhere along the run there is
a first configuration in a post-guess phase, and this file finds it and
recognizes its tape.
Two facts do it. The phases before it are all the outer layer's, so the rules
fired up to that point keep the file, keep the addressed tracks and write bits
(nexRule_keepsFile_of_ne_eval and its two siblings) – which is exactly what
DescriptiveComplexity.Draw.Data.ShapedAt propagates along a run. And an accepting
configuration is in a post-guess phase, so the search has something to find.
What comes out is a configuration whose tape is an ixBack of some tape state
and whose phase is post-guess: the point where the machine's nondeterminism is
spent, the guess is written on the tape, and the rest of the run is the
evaluation's – deterministic, and read forward.
The first time a property holds #
A property that holds at some time holds first at some time, with
nothing before it. This is Nat.find in the form a run's reading wants: the
index, that it is no later than the one it was given, and that every earlier
index misses.
Dependency graph
Every rule the machine can fire outside the post-guess phases keeps the
file, keeps the addressed tracks and writes bits. The evaluation's rules fire
from an evaluation phase (nexEvalHosrcF), and those are post-guess – so a rule
whose source phase is not is one of the outer layer's, where the three facts are
nexRule_keepsFile_of_ne_eval and its siblings.
Dependency graph
An accepting configuration is in a post-guess phase, and its state is a
phase state: the accepting predicate names NexPh.acceptP, and an accepting
state is canonically padded, so it is stateElt of its own pointer. This is
what gives the search for the entry something to find.
Dependency graph
No rule enters the start phase. The machine is in it at time zero and never again – which is what tells a reading that every step after the first fires a rule that keeps the marker rather than writing it.
Dependency graph
The start step writes the marker and the bottom mark, and it is the only rule that fires from the start phase.
Dependency graph
Every other rule of the outer layer keeps the marker and the bottom mark: the evaluation's fire from a post-guess phase and the start step from the start phase, so a rule whose source phase is neither leaves them where they are.
Dependency graph
The one way into the post-guess phases is the guess's stop, and it lands
in the walk home. The sweep over the region is never done – where it stops is
the program's choice, so GuessSpec.Done is False and the exit that would land
in NexPh.guessDoneP can never fire – so a rule that leaves the pre-guess phases
leaves them for NexPh.homeGuessP. That is the phase a backward reading finds at
its entry, and it is the one reachesIn_homeGuessTail runs from.
Dependency graph
The first post-guess configuration of a run, with its tape recognized.
Every step before it fires a rule of the outer layer, and those keep the file –
so the shape the channel wrote at time zero is still there, and the tape is an
ixBack of a tape state (exists_ixBack_of_shape). The phase at that time is
one the machine never leaves, which is what
DescriptiveComplexity.Draw.Data.not_acc_of_verdict_false_of asks of its entry.
This is where a backward reading starts: the guess is on the tape, the run from here on is the evaluation's, and it is deterministic.
Dependency graph
The run from the entry, forward again #
From the entry to the evaluation, at the handed program: the walk home
and the dispatch (reachesIn_homeGuessTail) with the program's rules discharged
(nexProgHanded_rules), over the file the channel hands it. The tape is
whatever the guess left – the lemma reads none of it but the marker – so this is
the step a backward reading takes from the configuration
exists_postGuess_shaped hands it.
Dependency graph
The tape state the entry carries #
The entry's tape, read as a tape state. The channel's tape is
recognizable (tapeShape_initBackReg), the reading survives to the first
post-guess time (exists_postGuess_shaped) and there the tape is an ixBack
(exists_ixBack_of_shape) whose mirror, target, saved mirror and valuation are
empty. The marker is the one write of the opening the reading has to read: the
start step sets it at the cell the head began on and no later rule touches it
(track_set_of_seq, nexProgHanded_setsSlot_wk, nexProgHanded_keepsSlot_wk),
so the state's working track marks that cell alone.
That is every hypothesis the evaluation's entry state is asked for except the
stage tracks, which are the guess's and are read off the same ixBack.
Dependency graph
No acceptance, from a false verdict at the entry #
An entry whose verdict is false accepts nothing. From the configuration a
backward reading finds – the walk home, at the tape state it recovered – the
machine's run is forced: the walk home and the dispatch
(nexProgHanded_reachesIn_homeGuessTail), then the evaluation, which ends in the
accepting phase with the bit the sentence's own value. If that bit is clear the
run is a dead end, and from a post-guess configuration the machine has only one
run (not_acc_of_verdict_false_of) – so nothing below the entry accepts.
This is the backward direction's last step: the reading supplies the entry, the evaluation supplies the verdict, and the false verdict of a no-instance closes it.