The nodes of an interpreted AND/OR graph, as states of a game

The road from DescriptiveComplexity.EXPTIME to SO-GAME reads a PTIME inner problem as the AND/OR graph an interpretation draws on the expanded universe, and plays that graph. A node of the graph is a tagged tuple of points, so a node is a state of a second-order game – that correspondence is what this file builds.

Two things are settled here.

The interpretation may be taken non-relativized. GAME is PTIME-hard under ordinary ordered reductions (DescriptiveComplexity.game_hard_ordered): the composite of the Horn discharge with the unit-propagation game is a plain ≤ᶠᵒ[≤], and DescriptiveComplexity.game_PTIME_hard only widens it to ≤ʳᶠᵒ[≤] at the very end. That matters here: a definable domain would have to be checked by a formula over the expansion, i.e., by a whole sub-game, whereas a non-relativized interpretation leaves the nodes guarded by nothing but “each slot is a point”.

A node is a guarded assignment. The state block is DescriptiveComplexity.ExpExpansion.nodeBlock: the d rounds of DescriptiveComplexity.repMerged, each holding one point of the expanded universe (DescriptiveComplexity.ExpExpansion.pointBlock), extended by tag bits for the interpretation's tag. DescriptiveComplexity.ExpExpansion.nodeGuardF says exactly that a guessed state is such a tuple (DescriptiveComplexity.ExpExpansion.realize_nodeGuardF), so quantifying over nodes of the graph is quantifying over guarded states (DescriptiveComplexity.ExpExpansion.exists_node_iff).

GAME is PTIME-hard under ordinary ordered reductions

theorem DescriptiveComplexity.game_hard_ordered {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) (hQ : SigmaSOHornDefinable Q) : Nonempty (OrderedFOReduction Q GAME)

GAME is PTIME-hard without a definable domain: the reduction of DescriptiveComplexity.game_PTIME_hard is an ordinary ordered one, and only becomes relativized when DescriptiveComplexity.ComplexityClass.Hard asks for it. Playing the graph an interpretation draws needs this form, since a definable domain would itself have to be decided by a sub-game.

Splitting a merged round assignment

theorem DescriptiveComplexity.repBlockAssign_split (B : SOBlock) (A : Type) (k : ℕ) (ν : (repMerged B k).Assignment A) : ∃ (ρs : Fin k → B.Assignment A), ν = repBlockAssign B A k ρs

Every assignment of the merged rounds is one assignment per round.

The block a node is guessed in

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.nodeBlock {L : FirstOrder.Language} (X : ExpExpansion L) (T : Type) [Finite T] (d : ℕ) : SOBlock

The block of a node of an AND/OR graph interpreted over the expansion: d rounds, each holding a point, and tag bits naming the interpretation's tag.

Equations

• X.nodeBlock T d = (DescriptiveComplexity.repMerged X.pointBlock d).withTag T

def DescriptiveComplexity.ExpExpansion.nodeAssign {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (n : T × (Fin d → X.Map A)) : (X.nodeBlock T d).Assignment A

The state carrying a node: its tag in the tag bits, its points in the rounds.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.nodeGuardF {L : FirstOrder.Language} (X : ExpExpansion L) (T : Type) [Finite T] (d : ℕ) : ((L.sum FirstOrder.Language.order).sum (X.nodeBlock T d).lang).Sentence

The guard saying a guessed state is a node: its tag bits name a tag and each of its rounds is a point.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_nodeGuardF {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (σ : (X.nodeBlock T d).Assignment A) : A ⊨ X.nodeGuardF T d ↔ ∃ (n : T × (Fin d → X.Map A)), σ = nodeAssign n

The guard is exactly “this is a node”.

theorem DescriptiveComplexity.ExpExpansion.exists_node_iff {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (P : (X.nodeBlock T d).Assignment A → Prop) : (∃ (σ : (X.nodeBlock T d).Assignment A), A ⊨ X.nodeGuardF T d ∧ P σ) ↔ ∃ (n : T × (Fin d → X.Map A)), P (nodeAssign n)

Quantifying over nodes is quantifying over guarded states.