The machine plays the game #
The forward simulation: a winning state of an SOGameSpec is a winning
configuration of the machine. Everything it is made of is already proved – a
question holding wins from the entry of its prefix
(DescriptiveComplexity.GameProg.altWin_ask), an existential sweep writes what
its owner chooses and a universal one is answered for every assignment
(DescriptiveComplexity.altWin_sweep_ex,
DescriptiveComplexity.altWin_sweep_all) – so what is left is the control
graph, one clause of DescriptiveComplexity.SOGameSpec.Wins at a time.
The invariant #
DescriptiveComplexity.PlayCfg says the tape's region r holds the current
position and the machine is at play for that region. The candidate region is
junk: nothing reads it before it is swept.
That is where the roles swapping pays. play at !r re-enters the same
invariant with the regions exchanged, so a move of the game costs one sweep and
nothing is ever copied.
The three clauses #
Wins.won ρ ⟶ ∃ picks `verify won`
Wins.ex ρ σ ⟶ ∃ picks splitEx: ∀ { verify ¬univ ; sweep σ ; ∀ { verify move ; play σ } }
Wins.all ρ ⟶ ∃ picks splitAll: ∀ { verify univ
; sweep a witness ; verify move
; ∀-sweep ; ∃ { verify ¬move ; play } }
The last line is the one that needed the machinery: the universal sweep hands
an arbitrary candidate to allStep, where the existential player either
refutes the move – no sentence over the base could have filtered it out earlier
– or plays on, which is the induction hypothesis.
The machine sits at a position of the game: the tape's region r holds
that position, and the control is at play for that region.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
A branch that checks a question wins when the question holds.
Dependency graph
The pair of assignments that writes σ into the candidate region and
leaves the current one alone.
Dependency graph
The three clauses of Wins #
A state that wins outright: the existential player claims won.
Dependency graph
An existential state with a winning move: the existential player claims the existential clause, proves the state is its own and sweeps the move in; then the move is checked and the play goes on at the other region.
Dependency graph
A universal state all of whose moves win: the existential player claims the universal clause, proves the state is universal, certifies that a move exists at all, and then answers every candidate the universal sweep may write – by refuting the move, or by playing on.
Dependency graph
The play #
A winning state of the game is a winning configuration of the machine.
By induction on DescriptiveComplexity.SOGameSpec.Wins, one clause per lemma
above.
Dependency graph
The entry #
The machine accepts when the game does. The initial tape is empty –
Inp is total on the positions, which is what makes it functional – so the
starting position is guessed, by the very first sweep; the split that follows
checks it starts the game, and plays it.