The handed program on a no-instance #
DescriptiveComplexity.Draw.Data.wideRegAccept_of_out_of_rules is the
forward half of the machine's correctness: a sentence true at the guessed stage
makes the emitted instance a yes-instance. This file is the other half – if the
sentence is true at no stage, the machine does not accept – and it is where the
backward reading of an accepting run is used.
The shape of the argument is the yes-direction's turned round. An accepting run
starts where the channel wrote (exists_stepsIn_of_wideRegAccept); read as a
sequence, it has a first post-guess configuration whose tape is a tape state
(exists_entry_state) and whose phase is the walk home; the evaluation from
there returns the verdict as the sentence's own value at the stage the guess
left, which is assignOfTrack of the tracks the reading recovered; and a false
verdict cannot stand beside an accepting run (not_acc_of_entry_verdict).
Everything else – the marking, the file's ends, the rounds, the exits, the parked scratch and the region the atoms stay inside – is what the yes-direction supplies, and is supplied here the same way.
The handed program does not accept when no stage makes the sentence true. The backward direction of the machine's correctness, assembled: the run is read back to the configuration where the guess is spent, the evaluation is run forward from there, and its verdict – the sentence's value at the stage the reading recovered – is false, so the run cannot have accepted.
Dependency graph
The machine decides the guess-and-check, at the record #
The emitted instance is a yes-instance exactly when some stage makes the
sentence true. The two directions joined: a stage that works is run into the
accepting phase on the clock (wideRegAccept_of_out_of_rules), and if none
does, no run accepts (nexProgHanded_not_wideRegAccept_of_not_out). This is the
nondeterministic counterpart of
DescriptiveComplexity.Draw.Data.dwideAcceptSpace_iff_pfpHolds, and what a
reduction's correctness is read off.
Dependency graph
The clock, instantiated #
The clock's five numbers, from one width bound and one counting fact.
The parameters of wideRegAccept_iff_exists_out are related by nothing but
powers of two, so a single choice discharges them: take the block size m := 1,
the working exponent k as the larger of the evaluation's own width exponent
and |RegIx| + 3, and j := k + 2. Then the evaluation fits in 2 ^ k steps,
the file's stretch and the opening fit in 2 ^ k and 2 ^ (k + 1), and all the
clock asks of the drawing is that its universe have 2 k + 2 elements to
spare.
That is the shape §2.1's «|Tag| is the reduction's to choose» takes here: one
inequality between the tag count and the evaluation's width exponent, and
nothing else.
Dependency graph
The clock, with the width supplied too: the evaluation's own bound
(ixEvalWidth_le_two_pow_evalQ) put in front of
wideRegAccept_iff_exists_out_of_width, so that what a reduction owes the clock
is one inequality between the drawing's size and the exponent the record's
dimensions make.
Dependency graph
The machine decides the guess-and-check, with only the drawing's size left
to check. wideRegAccept_iff_exists_out_of_card with the clock's inequality
discharged by clock_count_of_tags: what is left is that the emitted program has
more rule names than a number built from the kernel alone – its loop budget, its
dimensions and its argument blocks – which a reduction gets by padding the
guessed block (SOBlock.pad, two_pow_card_le_card_nexRIx).