Documentation

DescriptiveComplexity.Exponential.GameGraph

The six questions an interpreted AND/OR graph asks, and their kernels #

The road from DescriptiveComplexity.EXPTIME to SO-GAME plays the AND/OR graph an interpretation I draws on the expanded universe. A node of that graph is a tag together with d points (DescriptiveComplexity.ExpExpansion.nodeBlock), and everything the game ever has to decide about one or two nodes is one of six first-order questions:

question	why the game asks it
`AGWon x`	the existential player claims the position wins outright
`AGUniv x`, `¬AGUniv x`	he claims the position belongs to one player, and must prove it
`AGMove x y`, `¬AGMove x y`	he proposes a move, or escapes an illegal one
`AGStart x`	the position he starts from is a marked start

DescriptiveComplexity.Sub names the six. None of them is a sentence over the base – a quantifier of I's defining formula ranges over points, so it is second-order over the base (DescriptiveComplexity.ExpExpansion.exists_translate) – and that is exactly why they become phases rather than conjuncts: DescriptiveComplexity.ExpExpansion.exists_paramKernel turns each into an alternating prefix over rounds of the point block, which a game plays one move per round.

What this file settles is the layout: the six prefixes have different lengths, and one game has one block. So the rounds are laid out as

0 ‥ d-1     the first node's points        parameters
d ‥ 2d-1    the second node's points       parameters
2d ‥ c-1    padding, points, unread        parameters of the short prefixes
c  ‥ n-1    the play rounds of this prefix

with n = 2 * d + Dm fixed by the longest prefix and c = n - D chosen per question, so that every prefix ends at the same round n - 1 and the move that fills round n - j is the same for all six (DescriptiveComplexity.ExpExpansion.exists_graphKernels). Padding at the bottom rather than at the top is what keeps every kernel a sentence over one block: no morphism between merged blocks of different lengths is ever needed.

The six questions #

inductive DescriptiveComplexity.Sub :

The six first-order questions the game asks about one or two nodes of the interpreted AND/OR graph.

won : Sub
The first node wins outright.
univ : Sub
The first node is universal.
notuniv : Sub
The first node is not universal.
mv : Sub
There is a move from the first node to the second.
notmv : Sub
There is no move from the first node to the second.
st : Sub
The first node is a marked start.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSub :

DecidableEq Sub

Equations

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

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSub :

Equations

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

Dependency graph

A node, read off the rounds #

def DescriptiveComplexity.ExpExpansion.nodeAt {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) {A : Type} [L.Structure A] [LinearOrder A] (h : 2 * d ≤ n) (t : T) (a : Fin 2) (pts : Fin n → X.Map A) :

I.Map (X.Map A)

The node whose tag is t and whose points are the argument slot a of the rounds: slot 0 is the first node, slot 1 the second.

Equations

DescriptiveComplexity.ExpExpansion.nodeAt I h t a pts = (t, fun (b : Fin d) => pts (DescriptiveComplexity.ExpExpansion.paramIx d n h a b))

Instances For

Dependency graph

def DescriptiveComplexity.ExpExpansion.SubHolds {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (h : 2 * d ≤ n) (s : Sub) (tx ty : T) (pts : Fin n → X.Map A) :

What the six questions ask, as properties of the rounds.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.ExpExpansion.SubHolds I h DescriptiveComplexity.Sub.won tx ty pts = DescriptiveComplexity.AGWon (DescriptiveComplexity.ExpExpansion.nodeAt I h tx 0 pts)
DescriptiveComplexity.ExpExpansion.SubHolds I h DescriptiveComplexity.Sub.univ tx ty pts = DescriptiveComplexity.AGUniv (DescriptiveComplexity.ExpExpansion.nodeAt I h tx 0 pts)
DescriptiveComplexity.ExpExpansion.SubHolds I h DescriptiveComplexity.Sub.notuniv tx ty pts = ¬DescriptiveComplexity.AGUniv (DescriptiveComplexity.ExpExpansion.nodeAt I h tx 0 pts)
DescriptiveComplexity.ExpExpansion.SubHolds I h DescriptiveComplexity.Sub.st tx ty pts = DescriptiveComplexity.AGStart (DescriptiveComplexity.ExpExpansion.nodeAt I h tx 0 pts)

Instances For

Dependency graph

The defining formula of each question #

noncomputable def DescriptiveComplexity.ExpExpansion.widen {L : FirstOrder.Language} {X : ExpExpansion L} {d : ℕ} (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin 1 × Fin d)) :

(X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)

A defining formula about the first node only, read as one about two.

Equations

DescriptiveComplexity.ExpExpansion.widen φ = FirstOrder.Language.Formula.relabel (fun (p : Fin 1 × Fin d) => (0, p.2)) φ

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.ExpExpansion.subFormula {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (s : Sub) (tx ty : T) :

(X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)

The defining formula of each of the six questions.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.ExpExpansion.subFormula I DescriptiveComplexity.Sub.won tx ty = DescriptiveComplexity.ExpExpansion.widen (I.relFormula FirstOrder.Language.agWon ![tx])
DescriptiveComplexity.ExpExpansion.subFormula I DescriptiveComplexity.Sub.univ tx ty = DescriptiveComplexity.ExpExpansion.widen (I.relFormula FirstOrder.Language.agUniv ![tx])
DescriptiveComplexity.ExpExpansion.subFormula I DescriptiveComplexity.Sub.mv tx ty = I.relFormula FirstOrder.Language.agMove ![tx, ty]
DescriptiveComplexity.ExpExpansion.subFormula I DescriptiveComplexity.Sub.notmv tx ty = FirstOrder.Language.BoundedFormula.not (I.relFormula FirstOrder.Language.agMove ![tx, ty])
DescriptiveComplexity.ExpExpansion.subFormula I DescriptiveComplexity.Sub.st tx ty = DescriptiveComplexity.ExpExpansion.widen (I.relFormula FirstOrder.Language.agStart ![tx])

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_won {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.won tx ty = widen (I.relFormula FirstOrder.Language.agWon ![tx])

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_univ {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.univ tx ty = widen (I.relFormula FirstOrder.Language.agUniv ![tx])

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_notuniv {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.notuniv tx ty = FirstOrder.Language.BoundedFormula.not (widen (I.relFormula FirstOrder.Language.agUniv ![tx]))

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_mv {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.mv tx ty = I.relFormula FirstOrder.Language.agMove ![tx, ty]

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_notmv {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.notmv tx ty = FirstOrder.Language.BoundedFormula.not (I.relFormula FirstOrder.Language.agMove ![tx, ty])

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExpExpansion.subFormula_st {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (tx ty : T) :

subFormula I Sub.st tx ty = widen (I.relFormula FirstOrder.Language.agStart ![tx])

Dependency graph

The formula is the question #

theorem DescriptiveComplexity.ExpExpansion.realize_subFormula {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (h : 2 * d ≤ n) (s : Sub) (tx ty : T) (pts : Fin n → X.Map A) :

((subFormula I s tx ty).Realize fun (p : Fin 2 × Fin d) => pts (paramIx d n h p.1 p.2)) ↔ SubHolds I h s tx ty pts

Each defining formula asks its question.

Dependency graph

The six kernels, at one layout #

def DescriptiveComplexity.ExpExpansion.KernelSpec {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n : ℕ} (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (h : 2 * d ≤ n) (c D : ℕ) (s : Sub) (tx ty : T) (K : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence) :

What it is for a kernel to decide a question at a layout: read against rounds whose first c hold the parameters and whose last D are quantified alternately, it is the question.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.ExpExpansion.exists_graphKernels {L : FirstOrder.Language} (X : ExpExpansion L) (T : Type) (d : ℕ) [Finite T] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) :

∃ (Dm : ℕ) (D : Sub → T → T → ℕ), (∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm) ∧ ∃ (K : Sub → T → T → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock (2 * d + Dm)).lang).Sentence), ∀ (s : Sub) (tx ty : T), KernelSpec I ⋯ (2 * d + Dm - D s tx ty) (D s tx ty) s tx ty (K s tx ty)

The six questions share one block. Every question gets the same number n = 2 * d + Dm of rounds, Dm being the length of the longest of the six prefixes; a question whose own prefix is shorter simply starts its play rounds later, at c = n - D, so that all six end at round n - 1 and the move filling round n - j does not depend on which question is being asked.

Dependency graph