A configuration of the control, and the steps out of it #
The bridge between the machine of DescriptiveComplexity.Exponential.GameMachine
and the two simulations: what it means for the machine to sit at a phase of the
control, that a step of the control graph is a step of the machine, and that
nothing else is.
The configuration #
DescriptiveComplexity.CtrlCfg bundles the four facts every phase of the
control keeps:
- the state is that phase, at a valuation it declares;
- the valuation is canonical – everything the phase does not declare is pinned,
which is what makes it unique (
DescriptiveComplexity.eq_truncTuple), and so what lets the backward reading name it; - the head is on the sentinel
DescriptiveComplexity.MachPh.parnames, which is the invariant that replaces knowing where the head is; - the tape holds the two assignments – at the positions, the only place it is ever read.
Being a conjunction of equations rather than a structure keeps it usable with
rw at the transparency the tagged-tuple types force.
The two readings #
DescriptiveComplexity.ctrlCfg_step builds a step from an edge of
DescriptiveComplexity.MachPh.CtrlStep, and
DescriptiveComplexity.ctrlCfg_cases reads every step back as such an edge –
the _det-style lemma the universal phases need, since a universal
configuration wins only when every successor does. Both are stated at an
arbitrary phase that is not a walk; the walks have their own runs.
Winning along a walk #
DescriptiveComplexity.altWin_of_guardedChain is what turns a run into a win:
a chain of steps all of whose sources are existential is won as soon as its last
configuration is. The runs of GameMachine produce exactly such a chain – the
guard being the state has not changed – which is why they carry it. Its
universal counterpart is DescriptiveComplexity.altWin_of_walk, which runs a
walk backwards: a family of configurations closed under the steps that carry
the walk on, every exit of which wins.
One move, and then the prefix #
DescriptiveComplexity.altWin_of_steps is the shape every phase of the control
has, whichever player owns it: a witness among the successors, always, and
goodness of every successor, only when the phase is universal – both read off
one Good predicate, into which the phase's own content goes.
Its first customers are here: the alternating prefix of a question, played one
variable at a time (DescriptiveComplexity.altWin_pre, with
DescriptiveComplexity.qval naming the restriction of the machine's tuple to
the question's variables), and the challenge round that settles the matrix –
altWin_claim into altWin_check into altWin_seek and altWin_conc. All of
it is parametric in concOk and isTarget; the program that supplies them is
DescriptiveComplexity.Exponential.GameAsk.
Winning along a chain of existential steps #
A chain of existential steps wins if its last configuration does. The
guard is what the walks of DescriptiveComplexity.Exponential.GameMachine
carry: a predicate true of every configuration a step is taken from.
Dependency graph
A universal walk wins if every way out of it wins. The family F is
closed under the steps that carry the walk on – each moving the head one
position – and a step that leaves it already wins; so the walk is won, by
induction on how far the head still has to go.
This is what a universal sweep needs, and it is the one place the simulation
runs a walk backwards: AltWin.all quantifies over every step, so the walk
cannot be summarized by its run.
Dependency graph
A configuration of the control #
The machine sits at a phase of the control: the phase at a canonical valuation, the head on the sentinel its parity names, and the tape holding the two assignments – at the positions, the only place it is ever read.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The head of a control configuration is a position, and it reads the left mark.
Dependency graph
Dependency graph
A phase that declares no coordinate is entered at the constant valuation – which is every phase of the game proper, and the entry of every question's prefix.
Dependency graph
An edge of the control graph is a step of the machine. The tape is untouched, the head bounces to the other sentinel, and the destination keeps the transition's tuple up to the arity it declares – so the choice of the transition is the choice of the coordinate a prefix phase writes.
Dependency graph
And nothing else is: every step out of a control configuration is such an edge. This is what a universal phase needs, since it wins only when all its successors do; the destination's valuation is forced because the domain pins whatever the phase does not declare.
Dependency graph
The two ends of a branch #
A state of the control belongs to the universal player exactly when its phase does – read at a configuration rather than at a point.
Dependency graph
The accepting phase accepts.
Dependency graph
A concluding phase whose residual formula holds wins. This is the one
place a question is settled by the source structure rather than by the tape:
concOk is a guard the interpretation writes, and a branch that fails it has
no transition at all – so it loses, the phase being existential.
Dependency graph
One move of the control, whichever player owns it #
A phase wins when the moves its owner may make win. The existential
player needs one good successor, the universal player needs every successor to
be good – so the two halves of the hypothesis are a witness, always, and
goodness of all successors, only when the phase is universal. Both are read
off the same Good predicate, which is where the phase's own content goes.
This is the shape every phase of the control has, the prefix included: a transition is a pair (destination phase, tuple), the tuple being the value a prefix move writes.
Dependency graph
The prefix, played one variable at a time #
The question's own valuation, read off the machine's tuple: the prefix
of DescriptiveComplexity.QuestionData quantifies over Fin (vars q) → A,
while the machine carries the whole tuple with junk above – which
DescriptiveComplexity.altQuantFrom_congr_val licenses.
Equations
- DescriptiveComplexity.qval hV q vv = DescriptiveComplexity.pref ⋯ vv
Instances For
Dependency graph
Dependency graph
The prefix hands over to the claim once every variable has been
written. The phase still has an owner, but only one successor, so the two
readings of DescriptiveComplexity.altWin_of_steps coincide.
Dependency graph
The alternating prefix of a question is played as moves. The phase index
is the number of variables already written, the player its polarity names
chooses the next one – which is the choice of the transition, since the
transition's tuple is the value written – and the phase declares one more
coordinate than the one before, so DescriptiveComplexity.truncTuple_succ
turns the step into a single Function.update on either side of qval.
Dependency graph
Settling a question: the challenge round #
A seek whose cell exists wins. The run either meets it – and the next state accepts – or reaches the right sentinel having found none, which the hypothesis forbids. Every configuration of the run is the same existential phase, which is what the run's guarded chain carries.
Dependency graph
The challenge round wins. check is universal: the existential player
has already claimed the whole vector of truth values, and every successor is
either a challenge – settled by a seek, which finds its cell exactly when the
claim was right – or the concluding transition, guarded by the residual
formula. So the round is won precisely when the claims are correct and the
residue holds, which is DescriptiveComplexity.QuestionData.MatrixHolds.
Dependency graph
Claiming the truth values wins, when a correct vector concludes. The
claim is one existential move – finitely many vectors, so finitely many
transitions – and it is the whole of the matrix the machine ever computes: what
follows is a challenge round, DescriptiveComplexity.altWin_check.