The control of a machine playing a second-order game

The phases of the machine whose tape is DescriptiveComplexity.Exponential.GameTape, and which player owns each. This file fixes the control design; the transition table that realizes it is the next step.

The play, in one block

r is the region holding the current position of the game, !r the one holding the candidate. A universal split is how a check is conjoined with a continuation: a universal state whose successors are the branches, each of which then has its own copy of the tape.

init        ∃-sweep into region 0 ; splitStart
splitStart  ∀ { verify start ; play }
play        ∃ { verify won                                    -- Wins.won
              ; splitEx                                       -- Wins.ex
              ; splitAll }                                    -- Wins.all
splitEx     ∀ { verify ¬univ ; ∃-sweep into !r ; splitMove }
splitMove   ∀ { verify move ; play at !r }
splitAll    ∀ { verify univ
              ; ∃-sweep into !r ; verify move                 -- a legal move exists
              ; ∀-sweep into !r ; allStep }
allStep     ∃ { verify ¬move ; play at !r }

Three conventions, all forced:

• play is existential and chooses which clause of DescriptiveComplexity.SOGameSpec.Wins it claims; a false claim loses because the corresponding check runs out of transitions.
• the universal clause certifies a successor before it hands over (Wins.all demands a legal move), which is the second branch of splitAll; the branches carry separate tapes, so the ∃-guess and the ∀-guess of the candidate never collide.
• an illegal universal guess is discarded by the existential player, who may refute move at allStep instead of continuing – no sentence over the base could filter it out before the guess.

play at !r swaps the roles of the two regions instead of copying one over the other; a copy would be a quadratic walk with a nested induction.

Checking a question

A check is DescriptiveComplexity.QuestionData run as a walk (DescriptiveComplexity.exists_questionData): the prefix is played one variable at a time, then the existential player claims the truth values of the block atoms in one move, and the universal player either challenges one – a walk to the cell it addresses – or lets the residual formula, which mentions no block atom, guard the concluding transition.

pre q j     the player `pol q j` names writes the j-th variable ; pre q (j+1)
            at j = vars q: claim
claim q     ∃ picks the whole vector b of claims               ; check q b
check q b   ∀ { seek q b k  (k < natoms q) ; conc q b }
seek q b k  walk to the cell of the k-th atom; accept iff its bit is b k
conc q b    accept if the residual formula holds; no transition otherwise

Two bookkeeping fields, and why

• par: DescriptiveComplexity.TMData.Step has no stay-put option, so a phase that does not touch the tape still moves the head; it bounces between the two left sentinels and par says which one it is on.
• cont: a sweep is one gadget used four times, so it carries what to do when it is over. It is followed by a rewind, a leftward walk that restores the head to the left sentinel, so that every check starts from the same end and the seek only ever walks one way.

Why a structure rather than an inductive

DescriptiveComplexity.MachPh is a flat record, with fields that are junk in the phases that do not use them. That is deliberate: Finite and DecidableEq come from the product, the tag order of DescriptiveComplexity.machTagOrder needs nothing else, and no injective numbering of constructors has to be maintained. Unreachable field combinations are harmless – no transition mentions them.

The pieces of a phase

inductive DescriptiveComplexity.SweepCont : Type

What a sweep does when it is over: the four places the control guesses an assignment.

• start : SweepCont

  The initial sweep, which guesses the starting position of the game.

• exMove : SweepCont

  The existential player's move out of an existential position.

• certify : SweepCont

  The existential player's certificate that the universal position it is about to hand over has a legal move at all.

• allMove : SweepCont

  The universal player's move out of a universal position.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSweepCont : DecidableEq SweepCont

Equations

• DescriptiveComplexity.instDecidableEqSweepCont x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSweepCont : Fintype SweepCont

Equations

• One or more equations did not get rendered due to their size.

inductive DescriptiveComplexity.PhKind : Type

The kind of a phase: what the machine is doing.

• sweep : PhKind

  Walking right, writing a guessed assignment into one region.

• rewind : PhKind

  Walking left, back to the left sentinel.

• splitStart : PhKind

  After the initial sweep: check the start condition, and play.

• play : PhKind

  A position of the game: the existential player picks a clause of Wins.

• splitEx : PhKind

  The existential clause: check that the position is existential, and move.

• splitAll : PhKind

  The universal clause: check that the position is universal, certify a successor, and answer every candidate.

• splitMove : PhKind

  After a candidate has been guessed: check the move, and play on.

• allStep : PhKind

  After the universal player's candidate: refute the move, or play on.

• pre : PhKind

  Playing the quantifier prefix of a question.

• claim : PhKind

  Claiming the truth values of the block atoms of a question.

• check : PhKind

  Challenging one claim, or concluding.

• seek : PhKind

  Walking to the cell a challenged claim addresses.

• conc : PhKind

  The residual formula decides.

• acc : PhKind

  Accepting.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqPhKind : DecidableEq PhKind

Equations

• DescriptiveComplexity.instDecidableEqPhKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypePhKind : Fintype PhKind

Equations

• One or more equations did not get rendered due to their size.

A phase

structure DescriptiveComplexity.MachPh (V M : ℕ) : Type

A phase of the control: what the machine is doing, and the bookkeeping it carries. Fields not used by a kind are junk – see the module docstring.

• kind : PhKind

  What the machine is doing.

• q : GameQuestion

  The question being checked.

• r : Bool

  The region holding the current position of the game.

• tgt : Bool

  The region a sweep is writing into; at a seek, the claimed bit.

• j : Fin (V + 1)

  The index of the prefix variable being played.

• k : Fin (M + 1)

  The index of the block atom being challenged.

• claims : Fin M → Bool

  The claimed truth values of the block atoms.

• cont : SweepCont

  What a sweep does when it is over.

• par : Bool

  Which of the two left sentinels the head is bouncing on.

theorem DescriptiveComplexity.MachPh.ext_iff {V M : ℕ} {x y : MachPh V M} : x = y ↔ x.kind = y.kind ∧ x.q = y.q ∧ x.r = y.r ∧ x.tgt = y.tgt ∧ x.j = y.j ∧ x.k = y.k ∧ x.claims = y.claims ∧ x.cont = y.cont ∧ x.par = y.par

theorem DescriptiveComplexity.MachPh.ext {V M : ℕ} {x y : MachPh V M} (kind : x.kind = y.kind) (q : x.q = y.q) (r : x.r = y.r) (tgt : x.tgt = y.tgt) (j : x.j = y.j) (k : x.k = y.k) (claims : x.claims = y.claims) (cont : x.cont = y.cont) (par : x.par = y.par) : x = y

def DescriptiveComplexity.MachPh.toProd {V M : ℕ} (p : MachPh V M) : PhKind × GameQuestion × Bool × Bool × Fin (V + 1) × Fin (M + 1) × (Fin M → Bool) × SweepCont × Bool

A phase as a tuple, for the Finite instance.

Equations

• p.toProd = (p.kind, p.q, p.r, p.tgt, p.j, p.k, p.claims, p.cont, p.par)

theorem DescriptiveComplexity.MachPh.toProd_injective {V M : ℕ} : Function.Injective toProd

instance DescriptiveComplexity.MachPh.instFinite {V M : ℕ} : Finite (MachPh V M)

instance DescriptiveComplexity.MachPh.instNonempty {V M : ℕ} : Nonempty (MachPh V M)

What a phase owns and uses

def DescriptiveComplexity.MachPh.arity {V M : ℕ} (vars : GameQuestion → ℕ) (p : MachPh V M) : ℕ

The coordinates a phase uses: the prefix has written the variables below j, and a question that has reached its matrix has written them all. Everything else carries no data, so the domain pins its whole tuple.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.IsUniv {V M : ℕ} (pol : GameQuestion → ℕ → Bool) (p : MachPh V M) : Bool

Which phases belong to the universal player. The splits are universal because they conjoin a check with a continuation; check is universal because it is the challenge; a prefix variable belongs to the player its polarity names; a sweep belongs to the player guessing the assignment, which is the universal one exactly for the universal player's own move.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_play {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.play) : IsUniv pol p = false

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_check {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.check) : IsUniv pol p = true

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_claim {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.claim) : IsUniv pol p = false

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_acc {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.acc) : IsUniv pol p = false

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_conc {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.conc) : IsUniv pol p = false

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_allStep {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.allStep) : IsUniv pol p = false

theorem DescriptiveComplexity.MachPh.isUniv_split {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.splitStart ∨ p.kind = PhKind.splitEx ∨ p.kind = PhKind.splitAll ∨ p.kind = PhKind.splitMove) : IsUniv pol p = true

The four splits belong to the universal player, which is what makes a split a conjunction: each of its branches has to win.

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_seek {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.seek) : IsUniv pol p = false

@[simp]

theorem DescriptiveComplexity.MachPh.isUniv_rewind {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.rewind) : IsUniv pol p = false

theorem DescriptiveComplexity.MachPh.isUniv_sweep {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.sweep) : IsUniv pol p = (p.cont == SweepCont.allMove)

A sweep is universal exactly when it is the universal player's own move.

theorem DescriptiveComplexity.MachPh.isUniv_pre {V M : ℕ} (pol : GameQuestion → ℕ → Bool) {p : MachPh V M} (h : p.kind = PhKind.pre) : IsUniv pol p = !pol p.q ↑p.j

A prefix phase belongs to the player its polarity names.

The phases, named

def DescriptiveComplexity.MachPh.sweepPh {V M : ℕ} (r tgt : Bool) (cont : SweepCont) (par : Bool) : MachPh V M

The phase sweeping region tgt while the game sits in region r.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.rewindPh {V M : ℕ} (r tgt : Bool) (cont : SweepCont) (par : Bool) : MachPh V M

The phase walking back to the left sentinel after a sweep.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.splitStartPh {V M : ℕ} (r par : Bool) : MachPh V M

The split following the initial sweep.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.playPh {V M : ℕ} (r par : Bool) : MachPh V M

A position of the game, in region r.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.splitExPh {V M : ℕ} (r par : Bool) : MachPh V M

The existential clause of Wins.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.splitAllPh {V M : ℕ} (r par : Bool) : MachPh V M

The universal clause of Wins.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.splitMovePh {V M : ℕ} (r par : Bool) : MachPh V M

Checking the move just guessed, then playing on.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.allStepPh {V M : ℕ} (r par : Bool) : MachPh V M

Refuting the move just guessed, or playing on.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.prePh {V M : ℕ} (q : GameQuestion) (r : Bool) (j : Fin (V + 1)) (par : Bool) : MachPh V M

Playing the j-th variable of the prefix of q.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.claimPh {V M : ℕ} (q : GameQuestion) (r par : Bool) : MachPh V M

Claiming the truth values of the block atoms of q.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.checkPh {V M : ℕ} (q : GameQuestion) (r : Bool) (b : Fin M → Bool) (par : Bool) : MachPh V M

The claims of q are b: challenge one, or conclude.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.seekPh {V M : ℕ} (q : GameQuestion) (r : Bool) (b : Fin M → Bool) (k : Fin (M + 1)) (par : Bool) : MachPh V M

Walking to the cell the k-th atom of q addresses.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.concPh {V M : ℕ} (q : GameQuestion) (r : Bool) (b : Fin M → Bool) (par : Bool) : MachPh V M

The residual formula of q under the claims b decides.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.accPh {V M : ℕ} (par : Bool) : MachPh V M

The accepting phase.

Equations

• One or more equations did not get rendered due to their size.

The control graph

def DescriptiveComplexity.MachPh.CtrlStep {V M : ℕ} (vars natoms : GameQuestion → ℕ) (p p' : MachPh V M) : Prop

Where a tape-free step may go. This is the block of the module docstring, written out: the head is on a left sentinel throughout, so every step here flips par and moves between the two.

The steps out of a walk – a sweep handing over to its rewind, a rewind handing over to its continuation – are not here: they are tape steps, and DescriptiveComplexity.MachPh.rewindTarget is where the second one lands. Nor is the guard of conc, which is a condition on the source structure and enters the transition table rather than the control graph.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.MachPh.rewindTarget {V M : ℕ} (p : MachPh V M) : MachPh V M

Where a rewind hands over: the four continuations of a sweep. The head lands on the lowest position, so par is false.

Equations

• One or more equations did not get rendered due to their size.

The phases that carry no data

@[simp]

theorem DescriptiveComplexity.MachPh.arity_sweepPh {V M : ℕ} (vars : GameQuestion → ℕ) (r tgt : Bool) (cont : SweepCont) (par : Bool) : arity vars (sweepPh r tgt cont par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_rewindPh {V M : ℕ} (vars : GameQuestion → ℕ) (r tgt : Bool) (cont : SweepCont) (par : Bool) : arity vars (rewindPh r tgt cont par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_accPh {V M : ℕ} (vars : GameQuestion → ℕ) (par : Bool) : arity vars (accPh par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_playPh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (playPh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_splitStartPh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (splitStartPh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_splitExPh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (splitExPh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_splitAllPh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (splitAllPh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_splitMovePh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (splitMovePh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_allStepPh {V M : ℕ} (vars : GameQuestion → ℕ) (r par : Bool) : arity vars (allStepPh r par) = 0

@[simp]

theorem DescriptiveComplexity.MachPh.arity_prePh_zero {V M : ℕ} (vars : GameQuestion → ℕ) (q : GameQuestion) (r par : Bool) : arity vars (prePh q r 0 par) = 0

A prefix that has written nothing declares nothing, so the phase a question is entered at carries the constant valuation.

@[simp]

theorem DescriptiveComplexity.MachPh.arity_rewindTarget {V M : ℕ} (vars : GameQuestion → ℕ) (p : MachPh V M) : arity vars p.rewindTarget = 0

A rewind hands over to a phase that carries no data: the four continuations of a sweep are all at the start of their own business, so the state a rewind enters is the constant tuple.

@[simp]

theorem DescriptiveComplexity.MachPh.par_rewindTarget {V M : ℕ} (p : MachPh V M) : p.rewindTarget.par = false

And it hands over on the lowest position, which is what its parity records.

theorem DescriptiveComplexity.MachPh.arity_seekPh {V M : ℕ} (vars : GameQuestion → ℕ) (q : GameQuestion) (r : Bool) (b : Fin M → Bool) (k : Fin (M + 1)) (par : Bool) : arity vars (seekPh q r b k par) = vars q

A seek declares the variables of its own question.

theorem DescriptiveComplexity.MachPh.arity_concPh {V M : ℕ} (vars : GameQuestion → ℕ) (q : GameQuestion) (r : Bool) (b : Fin M → Bool) (par : Bool) : arity vars (concPh q r b par) = vars q

theorem DescriptiveComplexity.MachPh.arity_prePh {V M : ℕ} (vars : GameQuestion → ℕ) (q : GameQuestion) (r : Bool) (j : Fin (V + 1)) (par : Bool) : arity vars (prePh q r j par) = min (↑j) (vars q)

A prefix phase declares the variables it has already written.

theorem DescriptiveComplexity.MachPh.arity_claimPh {V M : ℕ} (vars : GameQuestion → ℕ) (q : GameQuestion) (r par : Bool) : arity vars (claimPh q r par) = vars q

theorem DescriptiveComplexity.MachPh.arity_of_matrix {V M : ℕ} (vars : GameQuestion → ℕ) {p : MachPh V M} (h : p.kind = PhKind.claim ∨ p.kind = PhKind.check ∨ p.kind = PhKind.seek ∨ p.kind = PhKind.conc) : arity vars p = vars p.q

A question that has reached its matrix declares its whole prefix.

Sanity of the control graph

The six phases of the game proper, each with its successors named. Stated as equivalences, because the universal ones are read backwards.

theorem DescriptiveComplexity.MachPh.ctrlStep_splitStartPh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (splitStartPh r par) p' ↔ p' = prePh GameQuestion.start r 0 !par ∨ p' = playPh r !par

theorem DescriptiveComplexity.MachPh.ctrlStep_playPh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (playPh r par) p' ↔ p' = prePh GameQuestion.won r 0 !par ∨ p' = splitExPh r !par ∨ p' = splitAllPh r !par

theorem DescriptiveComplexity.MachPh.ctrlStep_splitExPh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (splitExPh r par) p' ↔ p' = prePh GameQuestion.notUniv r 0 !par ∨ p' = sweepPh r (!r) SweepCont.exMove !par

theorem DescriptiveComplexity.MachPh.ctrlStep_splitAllPh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (splitAllPh r par) p' ↔ p' = prePh GameQuestion.univ r 0 !par ∨ p' = sweepPh r (!r) SweepCont.certify !par ∨ p' = sweepPh r (!r) SweepCont.allMove !par

theorem DescriptiveComplexity.MachPh.ctrlStep_splitMovePh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (splitMovePh r par) p' ↔ p' = prePh GameQuestion.move r 0 !par ∨ p' = playPh (!r) !par

theorem DescriptiveComplexity.MachPh.ctrlStep_allStepPh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (r par : Bool) (p' : MachPh V M) : CtrlStep vars natoms (allStepPh r par) p' ↔ p' = prePh GameQuestion.notMove r 0 !par ∨ p' = playPh (!r) !par

theorem DescriptiveComplexity.MachPh.ctrlStep_prePh {V M : ℕ} (vars natoms : GameQuestion → ℕ) (q : GameQuestion) (r : Bool) (j : Fin (V + 1)) (par : Bool) (h : ↑j < vars q) (p' : MachPh V M) : CtrlStep vars natoms (prePh q r j par) p' ↔ ∃ (j' : Fin (V + 1)), ↑j' = ↑j + 1 ∧ p' = prePh q r j' !par

A prefix phase with a variable left writes it, moving to the next index. Stated as an equivalence so that the backward reading has it too.

theorem DescriptiveComplexity.MachPh.ctrlStep_prePh_last {V M : ℕ} (vars natoms : GameQuestion → ℕ) (q : GameQuestion) (r : Bool) (j : Fin (V + 1)) (par : Bool) (h : ¬↑j < vars q) (p' : MachPh V M) : CtrlStep vars natoms (prePh q r j par) p' ↔ p' = claimPh q r !par

A prefix phase with no variable left hands over to the claim.

theorem DescriptiveComplexity.MachPh.par_of_ctrlStep {V M : ℕ} (vars natoms : GameQuestion → ℕ) {p p' : MachPh V M} (h : CtrlStep vars natoms p p') : p'.par = !p.par

A control step flips the parity: the head really does bounce.