The six questions a machine playing a second-order game must answer

DescriptiveComplexity.Exponential.AltQuant and DescriptiveComplexity.Exponential.BlockClaim are the two normal forms; this file applies them to an DescriptiveComplexity.SOGameSpec and packages the result as the interface a machine consumes.

The six questions

A machine playing the game of a specification has to decide six sentences, not four: the three one-copy sentences won, univ, start, the two-copy sentence move, and the negations of univ and of move. The negations are not a redundancy – a sentence is always used in the positive direction, an existential branch that proves it and gets stuck otherwise, so refuting one means proving another (DescriptiveComplexity.GameQuestion).

DescriptiveComplexity.SOGameSpec.question reads all six in the same language, the two-copy one, the one-copy sentences traveling along FirstOrder.Language.LHom.sumInl; that uniformity is what lets the machine's tag be a plain product rather than a dependent sum.

What the interface says

DescriptiveComplexity.QuestionData is what the machine's control needs about one question:

• vars and pol – the length of the alternating prefix and whose turn each variable is, so a prefix phase is an index and a tuple coordinate;
• atoms – the occurrences of block atoms in the matrix, each an address on the tape;
• sub – for each vector of claimed truth values, the residual formula over the base vocabulary, which the interpretation writes into a transition guard.

DescriptiveComplexity.QuestionData.Plays states that this data decides the sentence, and DescriptiveComplexity.exists_questionData produces it. The matrix condition is stated as DescriptiveComplexity.QuestionData.MatrixHolds – there is a vector of correct claims whose residual formula holds – which is literally the round the machine plays: the existential player claims the whole vector in one move, the universal player challenges one claim by a tape lookup or lets the residual formula be evaluated.

Reading a one-copy sentence in the two-copy language

theorem DescriptiveComplexity.realize_sumInl_two {K : FirstOrder.Language} {B : SOBlock} {A : Type} [K.Structure A] (ρ σ : B.Assignment A) (ψ : (K.sum B.lang).Sentence) : A ⊨ FirstOrder.Language.LHom.sumInl.onSentence ψ ↔ A ⊨ ψ

A sentence over one copy of the block, read in the two-copy language, says the same thing of the first copy.

The six questions

inductive DescriptiveComplexity.GameQuestion : Type

The six sentences a machine playing a second-order game must decide. The two negations are separate questions because a machine only ever proves: an existential branch that fails to prove its sentence runs out of transitions, so refuting a sentence has to be proving another one.

• won : GameQuestion

  The current position wins outright.

• univ : GameQuestion

  The current position belongs to the universal player.

• notUniv : GameQuestion

  The current position belongs to the existential player.

• move : GameQuestion

  The move from the current position to the candidate is legal.

• notMove : GameQuestion

  The move from the current position to the candidate is illegal.

• start : GameQuestion

  The current position starts the game.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqGameQuestion : DecidableEq GameQuestion

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeGameQuestion : Fintype GameQuestion

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.SOGameSpec.twoLang {L : FirstOrder.Language} (spec : SOGameSpec L) : FirstOrder.Language

The two-copy language of a specification: the base vocabulary and the order, expanded by two copies of the block.

Equations

• spec.twoLang = ((L.sum FirstOrder.Language.order).sum spec.B.lang).sum spec.B.lang

def DescriptiveComplexity.SOGameSpec.question {L : FirstOrder.Language} (spec : SOGameSpec L) : GameQuestion → spec.twoLang.Sentence

The sentence a question asks, all six read in the two-copy language.

Equations

• spec.question DescriptiveComplexity.GameQuestion.won = FirstOrder.Language.LHom.sumInl.onSentence spec.won
• spec.question DescriptiveComplexity.GameQuestion.univ = FirstOrder.Language.LHom.sumInl.onSentence spec.univ
• spec.question DescriptiveComplexity.GameQuestion.notUniv = FirstOrder.Language.BoundedFormula.not (FirstOrder.Language.LHom.sumInl.onSentence spec.univ)
• spec.question DescriptiveComplexity.GameQuestion.move = spec.move
• spec.question DescriptiveComplexity.GameQuestion.notMove = FirstOrder.Language.BoundedFormula.not spec.move
• spec.question DescriptiveComplexity.GameQuestion.start = FirstOrder.Language.LHom.sumInl.onSentence spec.start

def DescriptiveComplexity.SOGameSpec.QuestionHolds {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (q : GameQuestion) (ρ σ : spec.State A) : Prop

What a question asks, semantically: a condition on the current position and the candidate.

Equations

• spec.QuestionHolds DescriptiveComplexity.GameQuestion.won ρ σ = spec.IsWon ρ
• spec.QuestionHolds DescriptiveComplexity.GameQuestion.univ ρ σ = spec.IsUniv ρ
• spec.QuestionHolds DescriptiveComplexity.GameQuestion.notUniv ρ σ = ¬spec.IsUniv ρ
• spec.QuestionHolds DescriptiveComplexity.GameQuestion.move ρ σ = spec.Move ρ σ
• spec.QuestionHolds DescriptiveComplexity.GameQuestion.notMove ρ σ = ¬spec.Move ρ σ
• spec.QuestionHolds DescriptiveComplexity.GameQuestion.start ρ σ = spec.IsStart ρ

theorem DescriptiveComplexity.SOGameSpec.realize_question {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (q : GameQuestion) (ρ σ : spec.State A) : A ⊨ spec.question q ↔ spec.QuestionHolds q ρ σ

The sentence of a question says what the question asks.

What the machine needs to know about one question

structure DescriptiveComplexity.QuestionData (K : FirstOrder.Language) (B : SOBlock) : Type

The machine-ready form of one sentence: an alternating prefix, and a matrix presented as finitely many block-atom addresses together with, for each vector of claimed truth values, the residual formula over the base vocabulary.

• vars : ℕ

  The number of variables of the prefix, and of the matrix.

• pol : ℕ → Bool

  Whose turn each variable of the prefix is.

• natoms : ℕ

  The number of block-atom occurrences in the matrix.

• atoms : Fin self.natoms → BlockAtom B self.vars

  The occurrences, each an address on the tape.

• sub : (Fin self.natoms → Bool) → K.BoundedFormula Empty self.vars

  The residual formula, over the base vocabulary, of a vector of claims.

def DescriptiveComplexity.QuestionData.MatrixHolds {K : FirstOrder.Language} {B : SOBlock} (d : QuestionData K B) {A : Type} [K.Structure A] (ρ σ : B.Assignment A) (w : Fin d.vars → A) : Prop

The matrix, as the machine settles it: there is a vector of correct claims about the block atoms whose residual formula holds. The existential player claims the vector in one move; each claim is challengeable by a single tape lookup, and the residual formula guards the transition that concludes.

Equations

• d.MatrixHolds ρ σ w = ∃ (b : Fin d.natoms → Bool), (∀ (j : Fin d.natoms), b j = true ↔ (d.atoms j).Holds ρ σ w) ∧ (d.sub b).Realize default w

def DescriptiveComplexity.QuestionData.Plays {K : FirstOrder.Language} {B : SOBlock} (d : QuestionData K B) (φ : ((K.sum B.lang).sum B.lang).Sentence) : Prop

The data decides the sentence: the sentence is the alternating prefix of the data, played over its matrix. The initial tuple is arbitrary – the prefix overwrites every coordinate it reads.

Equations

• d.Plays φ = ∀ (A : Type) [inst : K.Structure A] [Nonempty A] (ρ σ : B.Assignment A) (v : Fin d.vars → A), A ⊨ φ ↔ DescriptiveComplexity.altQuantFrom d.pol (d.MatrixHolds ρ σ) 0 v

theorem DescriptiveComplexity.exists_questionData {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} (φ : ((K.sum B.lang).sum B.lang).Sentence) : ∃ (d : QuestionData K B), d.Plays φ

Every sentence over two copies of a block has machine-ready form. This is the composite of the two normal forms, and it is everything a machine's finite control needs in order to decide the sentence: a prefix of moves, a finite set of tape addresses, and a family of transition guards over the base vocabulary.