Deciders: walks with two exits, closed under the first-order connectives

Immerman's normal form for FO(TC) – a TC of a formula containing TCs is a single TC – is proved here not as a normal form on formulas but as an algebra of walks. A DescriptiveComplexity.Decider is a walk (modes and a tuple of coordinates, as DescriptiveComplexity.TCSpec) with two exits, yes and no, and a parameter type β its formulas may mention. It decides a proposition at a valuation of its parameters when, from its start mode and any tuple of coordinates, the yes exit is reachable exactly if the proposition holds and the no exit exactly if it fails (DescriptiveComplexity.Decider.Decides).

Starting from any tuple, rather than from a canonical one, is what makes the constructions below compose without resets: a decider run after another one simply starts where the previous one exited.

The algebra

• DescriptiveComplexity.Decider.atom decides a first-order formula over the base, by exiting at once;
• DescriptiveComplexity.Decider.neg swaps the two exits – negation is free, the decider being asked for both answers;
• DescriptiveComplexity.Decider.seq runs a second decider after the first exited yes – conjunction;
• DescriptiveComplexity.Decider.all runs a decider once per element of the universe, in the order of the structure, restarting it after each yes and exiting yes after the last element – universal quantification, with the quantified element frozen into a coordinate of the walk;
• DescriptiveComplexity.Decider.relabelPar renames the parameters.

Disjunction, implication and the existential quantifier are De Morgan combinations (DescriptiveComplexity.Decider.exTup is an existential over a whole tuple). What is not here is the atom case for a walk's own reachability relation, which is where nondeterminism (or a step budget) comes in: DescriptiveComplexity.TransitiveClosureDecideReach and DescriptiveComplexity.TransitiveClosureDecideReachDet.

Determinism travels

Every construction preserves functionality – at most one move, step or exit, out of every node (DescriptiveComplexity.Decider.Functional). This is what makes the same algebra serve the deterministic logic: a functional decider, turned into a specification (DescriptiveComplexity.Decider.toSpec), is unchanged by determinization.

Copying coordinates

noncomputable def DescriptiveComplexity.copyF {L : FirstOrder.Language} {γ ι : Type} [Finite ι] (sel sel' : ι → γ) : L.Formula γ

The formula “the variables sel' hold the same values as the variables sel”, coordinate by coordinate.

Equations

• DescriptiveComplexity.copyF sel sel' = FirstOrder.Language.Formula.iInf fun (i : ι) => (FirstOrder.Language.var (sel i)).equal (FirstOrder.Language.var (sel' i))

@[simp]

theorem DescriptiveComplexity.realize_copyF {L : FirstOrder.Language} {γ ι : Type} [Finite ι] {A : Type} [L.Structure A] {v : γ → A} (sel sel' : ι → γ) : (copyF sel sel').Realize v ↔ v ∘ sel' = v ∘ sel

Paths: an invariant and a lifting

theorem DescriptiveComplexity.reach_invariant {N : Type} {R : N → N → Prop} {P : N → Prop} (hP : ∀ (a b : N), P a → R a b → P b) {a b : N} (h : Relation.ReflTransGen R a b) (ha : P a) : P b

An invariant preserved by every step holds along a path.

Deciders

structure DescriptiveComplexity.Decider (L : FirstOrder.Language) (β : Type) : Type 1

A decider: a walk on tuples of Coord coordinates carrying a finite mode, with formulas that may mention parameters of type β, and two exits – yes (true) and no (false) – each a formula on the current tuple and the parameters. Its formulas are over the ordered expansion of the vocabulary, the iteration of DescriptiveComplexity.Decider.all needing the order.

• Mode : Type

  The modes.

• modeFinite : Finite self.Mode

  Modes are finite.

• Coord : Type

  The coordinates of a tuple.

• coordFinite : Finite self.Coord

  Tuples are finite.

• start : self.Mode

  The starting mode.

• step : self.Mode → self.Mode → (L.sum FirstOrder.Language.order).Formula ((self.Coord ⊕ self.Coord) ⊕ β)

  The step formula, one per pair of modes: the current tuple, the next one, then the parameters.

• exit : self.Mode → Bool → (L.sum FirstOrder.Language.order).Formula (self.Coord ⊕ β)

  The exit formulas: at a mode, the condition on the current tuple and the parameters under which the walk exits with the given answer.

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.Node {L : FirstOrder.Language} {β : Type} (D : Decider L β) (A : Type) : Type

A node of the walk: a mode together with a tuple.

Equations

• D.Node A = (D.Mode × (D.Coord → A))

def DescriptiveComplexity.Decider.StepAt {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a b : D.Node A) : Prop

One step of the walk, at a valuation of the parameters.

Equations

• D.StepAt v a b = (D.step a.1 b.1).Realize (Sum.elim (Sum.elim a.2 b.2) v)

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.ReachAt {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) : D.Node A → D.Node A → Prop

Reachability in the walk, at a valuation of the parameters.

Equations

• D.ReachAt v = Relation.ReflTransGen (D.StepAt v)

def DescriptiveComplexity.Decider.ExitAt {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a : D.Node A) (o : Bool) : Prop

The walk exits at a node with an answer.

Equations

• D.ExitAt v a o = (D.exit a.1 o).Realize (Sum.elim a.2 v)

def DescriptiveComplexity.Decider.Out {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D.Coord → A) (o : Bool) : Prop

The answer o is reachable from the start mode at the tuple t.

Equations

• D.Out v t o = ∃ (a : D.Node A), D.ReachAt v (D.start, t) a ∧ D.ExitAt v a o

def DescriptiveComplexity.Decider.Decides {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (P : Prop) : Prop

The decider decides P at a valuation of its parameters: from the start mode and any tuple, yes is reachable exactly when P holds, and no exactly when it fails.

Equations

• D.Decides v P = ∀ (t : D.Coord → A), (D.Out v t true ↔ P) ∧ (D.Out v t false ↔ ¬P)

def DescriptiveComplexity.Decider.Move {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a : D.Node A) : D.Node A ⊕ Bool → Prop

A move out of a node: a step to another node, or an exit.

Equations

• D.Move v a (Sum.inl b) = D.StepAt v a b
• D.Move v a (Sum.inr o) = D.ExitAt v a o

def DescriptiveComplexity.Decider.Functional {L : FirstOrder.Language} {β : Type} (D : Decider L β) (A : Type) [L.Structure A] [LinearOrder A] : Prop

A decider is functional when no node has two moves: the walk is deterministic, exits included.

Equations

• D.Functional A = ∀ (v : β → A) (a : D.Node A) (m m' : D.Node A ⊕ Bool), D.Move v a m → D.Move v a m' → m = m'

theorem DescriptiveComplexity.Decider.Decides.congr {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] {v : β → A} {P Q : Prop} (h : D.Decides v P) (hPQ : P ↔ Q) : D.Decides v Q

theorem DescriptiveComplexity.Decider.Decides.congr_val {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] {v w : β → A} {P : Prop} (h : D.Decides v P) (hvw : v = w) : D.Decides w P

theorem DescriptiveComplexity.Decider.Functional.step_unique {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) {v : β → A} {a b c : D.Node A} (hb : D.StepAt v a b) (hc : D.StepAt v a c) : b = c

theorem DescriptiveComplexity.Decider.Functional.not_exit_of_step {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) {v : β → A} {a b : D.Node A} (hb : D.StepAt v a b) {o : Bool} (ho : D.ExitAt v a o) : False

theorem DescriptiveComplexity.Decider.Functional.exit_unique {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) {v : β → A} {a : D.Node A} {o o' : Bool} (ho : D.ExitAt v a o) (ho' : D.ExitAt v a o') : o = o'

theorem DescriptiveComplexity.Decider.functional_of {L : FirstOrder.Language} {β : Type} {D : Decider L β} {A : Type} [L.Structure A] [LinearOrder A] (hstep : ∀ (v : β → A) (a b c : D.Node A), D.StepAt v a b → D.StepAt v a c → b = c) (hexit : ∀ (v : β → A) (a b : D.Node A) (o : Bool), D.StepAt v a b → ¬D.ExitAt v a o) (hboth : ∀ (v : β → A) (a : D.Node A), D.ExitAt v a true → ¬D.ExitAt v a false) : D.Functional A

Functionality, from its three components.

Renaming the parameters

@[reducible]

noncomputable def DescriptiveComplexity.Decider.relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) : Decider L γ

The decider with its parameters renamed along f: a parameter of the new decider is read where f sends it.

Equations

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

theorem DescriptiveComplexity.Decider.stepAt_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (v : γ → A) (a b : D.Node A) : (D.relabelPar f).StepAt v a b ↔ D.StepAt (v ∘ f) a b

theorem DescriptiveComplexity.Decider.exitAt_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (v : γ → A) (a : D.Node A) (o : Bool) : (D.relabelPar f).ExitAt v a o ↔ D.ExitAt (v ∘ f) a o

theorem DescriptiveComplexity.Decider.reachAt_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (v : γ → A) (a b : D.Node A) : (D.relabelPar f).ReachAt v a b ↔ D.ReachAt (v ∘ f) a b

theorem DescriptiveComplexity.Decider.out_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (v : γ → A) (t : D.Coord → A) (o : Bool) : (D.relabelPar f).Out v t o ↔ D.Out (v ∘ f) t o

theorem DescriptiveComplexity.Decider.decides_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (v : γ → A) {P : Prop} (h : D.Decides (v ∘ f) P) : (D.relabelPar f).Decides v P

theorem DescriptiveComplexity.Decider.functional_relabelPar {L : FirstOrder.Language} {β γ : Type} (D : Decider L β) (f : β → γ) {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) : (D.relabelPar f).Functional A

Atoms

@[reducible]

noncomputable def DescriptiveComplexity.Decider.atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) : Decider L β

The decider of a first-order formula over the base: no step, and it exits at once with the truth value of the formula.

Equations

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

theorem DescriptiveComplexity.Decider.exitAt_atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a : (atom ψ).Node A) (o : Bool) : (atom ψ).ExitAt v a o ↔ if o = true then ψ.Realize v else ¬ψ.Realize v

theorem DescriptiveComplexity.Decider.not_stepAt_atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a b : (atom ψ).Node A) : ¬(atom ψ).StepAt v a b

theorem DescriptiveComplexity.Decider.reachAt_atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {a b : (atom ψ).Node A} (h : (atom ψ).ReachAt v a b) : b = a

theorem DescriptiveComplexity.Decider.decides_atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) : (atom ψ).Decides v (ψ.Realize v)

theorem DescriptiveComplexity.Decider.functional_atom {L : FirstOrder.Language} {β : Type} (ψ : (L.sum FirstOrder.Language.order).Formula β) {A : Type} [L.Structure A] [LinearOrder A] : (atom ψ).Functional A

Negation

@[reducible]

noncomputable def DescriptiveComplexity.Decider.neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) : Decider L β

The decider with its two exits swapped.

Equations

• D.neg = { Mode := D.Mode, modeFinite := ⋯, Coord := D.Coord, coordFinite := ⋯, start := D.start, step := D.step, exit := fun (m : D.Mode) (o : Bool) => D.exit m !o }

theorem DescriptiveComplexity.Decider.stepAt_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a b : D.Node A) : D.neg.StepAt v a b ↔ D.StepAt v a b

theorem DescriptiveComplexity.Decider.exitAt_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a : D.Node A) (o : Bool) : D.neg.ExitAt v a o ↔ D.ExitAt v a !o

theorem DescriptiveComplexity.Decider.reachAt_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (a b : D.Node A) : D.neg.ReachAt v a b ↔ D.ReachAt v a b

theorem DescriptiveComplexity.Decider.out_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D.Coord → A) (o : Bool) : D.neg.Out v t o ↔ D.Out v t !o

theorem DescriptiveComplexity.Decider.decides_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {P : Prop} (h : D.Decides v P) : D.neg.Decides v ¬P

theorem DescriptiveComplexity.Decider.functional_neg {L : FirstOrder.Language} {β : Type} (D : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) : D.neg.Functional A

Sequential composition

def DescriptiveComplexity.Decider.seqVarL {β C₁ C₂ : Type} : (C₁ ⊕ C₁) ⊕ β → ((C₁ ⊕ C₂) ⊕ C₁ ⊕ C₂) ⊕ β

The variables of the first component's step, in the composite's.

Equations

• DescriptiveComplexity.Decider.seqVarL = Sum.map (Sum.map Sum.inl Sum.inl) id

def DescriptiveComplexity.Decider.seqVarR {β C₁ C₂ : Type} : (C₂ ⊕ C₂) ⊕ β → ((C₁ ⊕ C₂) ⊕ C₁ ⊕ C₂) ⊕ β

The variables of the second component's step, in the composite's.

Equations

• DescriptiveComplexity.Decider.seqVarR = Sum.map (Sum.map Sum.inr Sum.inr) id

def DescriptiveComplexity.Decider.seqExitL {β C₁ C₂ : Type} : C₁ ⊕ β → (C₁ ⊕ C₂) ⊕ β

The variables of the first component's exit, in the composite's exit.

Equations

• DescriptiveComplexity.Decider.seqExitL = Sum.map Sum.inl id

def DescriptiveComplexity.Decider.seqExitR {β C₁ C₂ : Type} : C₂ ⊕ β → (C₁ ⊕ C₂) ⊕ β

The variables of the second component's exit, in the composite's exit.

Equations

• DescriptiveComplexity.Decider.seqExitR = Sum.map Sum.inr id

def DescriptiveComplexity.Decider.seqExitStep {β C₁ C₂ : Type} : C₁ ⊕ β → ((C₁ ⊕ C₂) ⊕ C₁ ⊕ C₂) ⊕ β

The variables of the first component's exit, in the composite's step (read on the current tuple).

Equations

• DescriptiveComplexity.Decider.seqExitStep = Sum.map (fun (c : C₁) => Sum.inl (Sum.inl c)) id

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.curVar {β C : Type} (c : C) : (C ⊕ C) ⊕ β

The current tuple's coordinate c, as a step variable.

Equations

• DescriptiveComplexity.Decider.curVar c = Sum.inl (Sum.inl c)

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.nextVar {β C : Type} (c : C) : (C ⊕ C) ⊕ β

The next tuple's coordinate c, as a step variable.

Equations

• DescriptiveComplexity.Decider.nextVar c = Sum.inl (Sum.inr c)

@[reducible]

noncomputable def DescriptiveComplexity.Decider.seq {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) : Decider L β

Sequential composition: the first decider runs, and where it exits yes the second one starts, from the tuple it left; the answer is the second's. The coordinates of the idle component are copied along.

Equations

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

theorem DescriptiveComplexity.Decider.stepAt_seq_inl_inl {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m m' : D₁.Mode) (t t' : D₁.Coord ⊕ D₂.Coord → A) : (D₁.seq D₂).StepAt v (Sum.inl m, t) (Sum.inl m', t') ↔ D₁.StepAt v (m, t ∘ Sum.inl) (m', t' ∘ Sum.inl) ∧ t' ∘ Sum.inr = t ∘ Sum.inr

theorem DescriptiveComplexity.Decider.stepAt_seq_inl_inr {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D₁.Mode) (m' : D₂.Mode) (t t' : D₁.Coord ⊕ D₂.Coord → A) : (D₁.seq D₂).StepAt v (Sum.inl m, t) (Sum.inr m', t') ↔ m' = D₂.start ∧ D₁.ExitAt v (m, t ∘ Sum.inl) true ∧ t' = t

theorem DescriptiveComplexity.Decider.not_stepAt_seq_inr_inl {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D₂.Mode) (m' : D₁.Mode) (t t' : D₁.Coord ⊕ D₂.Coord → A) : ¬(D₁.seq D₂).StepAt v (Sum.inr m, t) (Sum.inl m', t')

theorem DescriptiveComplexity.Decider.stepAt_seq_inr_inr {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m m' : D₂.Mode) (t t' : D₁.Coord ⊕ D₂.Coord → A) : (D₁.seq D₂).StepAt v (Sum.inr m, t) (Sum.inr m', t') ↔ D₂.StepAt v (m, t ∘ Sum.inr) (m', t' ∘ Sum.inr) ∧ t' ∘ Sum.inl = t ∘ Sum.inl

theorem DescriptiveComplexity.Decider.exitAt_seq_inl {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D₁.Mode) (t : D₁.Coord ⊕ D₂.Coord → A) (o : Bool) : (D₁.seq D₂).ExitAt v (Sum.inl m, t) o ↔ o = false ∧ D₁.ExitAt v (m, t ∘ Sum.inl) false

theorem DescriptiveComplexity.Decider.exitAt_seq_inr {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D₂.Mode) (t : D₁.Coord ⊕ D₂.Coord → A) (o : Bool) : (D₁.seq D₂).ExitAt v (Sum.inr m, t) o ↔ D₂.ExitAt v (m, t ∘ Sum.inr) o

theorem DescriptiveComplexity.Decider.reachAt_seq_of_reachAt₁ {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {a b : D₁.Node A} (h : D₁.ReachAt v a b) (y : D₂.Coord → A) : (D₁.seq D₂).ReachAt v (Sum.inl a.1, Sum.elim a.2 y) (Sum.inl b.1, Sum.elim b.2 y)

A path of the first component lifts to the composite, the second component's coordinates fixed.

theorem DescriptiveComplexity.Decider.reachAt_seq_of_reachAt₂ {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {a b : D₂.Node A} (h : D₂.ReachAt v a b) (x : D₁.Coord → A) : (D₁.seq D₂).ReachAt v (Sum.inr a.1, Sum.elim x a.2) (Sum.inr b.1, Sum.elim x b.2)

A path of the second component lifts to the composite, the first component's coordinates fixed.

def DescriptiveComplexity.Decider.SeqInv {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D₁.Coord ⊕ D₂.Coord → A) (c : (D₁.seq D₂).Node A) : Prop

What the composite may have reached from its start at t: a node of the first component reached by it, the second's coordinates untouched, or a node of the second component reached after the first exited yes.

Equations

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

theorem DescriptiveComplexity.Decider.seqInv_of_reachAt {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D₁.Coord ⊕ D₂.Coord → A) {c : (D₁.seq D₂).Node A} (h : (D₁.seq D₂).ReachAt v (Sum.inl D₁.start, t) c) : D₁.SeqInv D₂ v t c

theorem DescriptiveComplexity.Decider.out_seq {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D₁.Coord ⊕ D₂.Coord → A) (o : Bool) : (D₁.seq D₂).Out v t o ↔ o = false ∧ D₁.Out v (t ∘ Sum.inl) false ∨ D₁.Out v (t ∘ Sum.inl) true ∧ D₂.Out v (t ∘ Sum.inr) o

theorem DescriptiveComplexity.Decider.decides_seq {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {P Q : Prop} (h₁ : D₁.Decides v P) (h₂ : D₂.Decides v Q) : (D₁.seq D₂).Decides v (P ∧ Q)

theorem DescriptiveComplexity.Decider.functional_seq {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) {A : Type} [L.Structure A] [LinearOrder A] (h₁ : D₁.Functional A) (h₂ : D₂.Functional A) : (D₁.seq D₂).Functional A

Universal quantification: an iteration along the order

def DescriptiveComplexity.Decider.allVar {β C : Type} : (C ⊕ C) ⊕ β ⊕ Unit → ((C ⊕ Unit) ⊕ C ⊕ Unit) ⊕ β

The variables of the component's step in the iteration's: the quantified parameter is read off the current tuple's extra coordinate.

Equations

• DescriptiveComplexity.Decider.allVar (Sum.inl (Sum.inl c)) = Sum.inl (Sum.inl (Sum.inl c))
• DescriptiveComplexity.Decider.allVar (Sum.inl (Sum.inr c)) = Sum.inl (Sum.inr (Sum.inl c))
• DescriptiveComplexity.Decider.allVar (Sum.inr (Sum.inl b)) = Sum.inr b
• DescriptiveComplexity.Decider.allVar (Sum.inr (Sum.inr PUnit.unit)) = Sum.inl (Sum.inl (Sum.inr ()))

def DescriptiveComplexity.Decider.allExitStep {β C : Type} : C ⊕ β ⊕ Unit → ((C ⊕ Unit) ⊕ C ⊕ Unit) ⊕ β

The variables of the component's exit in the iteration's step (read on the current tuple).

Equations

• DescriptiveComplexity.Decider.allExitStep (Sum.inl c) = Sum.inl (Sum.inl (Sum.inl c))
• DescriptiveComplexity.Decider.allExitStep (Sum.inr (Sum.inl b)) = Sum.inr b
• DescriptiveComplexity.Decider.allExitStep (Sum.inr (Sum.inr PUnit.unit)) = Sum.inl (Sum.inl (Sum.inr ()))

def DescriptiveComplexity.Decider.allExit {β C : Type} : C ⊕ β ⊕ Unit → (C ⊕ Unit) ⊕ β

The variables of the component's exit in the iteration's exit.

Equations

• DescriptiveComplexity.Decider.allExit (Sum.inl c) = Sum.inl (Sum.inl c)
• DescriptiveComplexity.Decider.allExit (Sum.inr (Sum.inl b)) = Sum.inr b
• DescriptiveComplexity.Decider.allExit (Sum.inr (Sum.inr PUnit.unit)) = Sum.inl (Sum.inr ())

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.yCur {β C : Type} : ((C ⊕ Unit) ⊕ C ⊕ Unit) ⊕ β

The extra coordinate holding the quantified element, in a step.

Equations

• DescriptiveComplexity.Decider.yCur = Sum.inl (Sum.inl (Sum.inr ()))

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.yNext {β C : Type} : ((C ⊕ Unit) ⊕ C ⊕ Unit) ⊕ β

The extra coordinate holding the quantified element, in a step.

Equations

• DescriptiveComplexity.Decider.yNext = Sum.inl (Sum.inr (Sum.inr ()))

@[reducible]

noncomputable def DescriptiveComplexity.Decider.all {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) : Decider L β

Universal quantification: the component is run once per element of the universe, in the order of the structure, the element being held in one extra coordinate. The first step sets it to the minimum; where the component exits yes below the maximum, it is restarted at the successor; a yes at the maximum, or a no anywhere, is the answer.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.vy {β A : Type} (v : β → A) (y : A) : β ⊕ Unit → A

The valuation of the component's parameters: the iteration's, and the current element.

Equations

• DescriptiveComplexity.Decider.vy v y = Sum.elim v fun (x : Unit) => y

theorem DescriptiveComplexity.Decider.stepAt_all_none_some {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (n : D.Mode) (t t' : D.Coord ⊕ Unit → A) : D.all.StepAt v (none, t) (some n, t') ↔ n = D.start ∧ t' ∘ Sum.inl = t ∘ Sum.inl ∧ ∀ (a : A), t' (Sum.inr ()) ≤ a

theorem DescriptiveComplexity.Decider.not_stepAt_all_none_none {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t t' : D.Coord ⊕ Unit → A) : ¬D.all.StepAt v (none, t) (none, t')

theorem DescriptiveComplexity.Decider.not_stepAt_all_some_none {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D.Mode) (t t' : D.Coord ⊕ Unit → A) : ¬D.all.StepAt v (some m, t) (none, t')

theorem DescriptiveComplexity.Decider.stepAt_all_some_some {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m n : D.Mode) (t t' : D.Coord ⊕ Unit → A) : D.all.StepAt v (some m, t) (some n, t') ↔ D.StepAt (vy v (t (Sum.inr ()))) (m, t ∘ Sum.inl) (n, t' ∘ Sum.inl) ∧ t' (Sum.inr ()) = t (Sum.inr ()) ∨ n = D.start ∧ D.ExitAt (vy v (t (Sum.inr ()))) (m, t ∘ Sum.inl) true ∧ (t (Sum.inr ()) < t' (Sum.inr ()) ∧ ∀ (a : A), ¬(t (Sum.inr ()) < a ∧ a < t' (Sum.inr ()))) ∧ t' ∘ Sum.inl = t ∘ Sum.inl

theorem DescriptiveComplexity.Decider.not_exitAt_all_none {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (t : D.Coord ⊕ Unit → A) (o : Bool) : ¬D.all.ExitAt v (none, t) o

theorem DescriptiveComplexity.Decider.exitAt_all_some {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (m : D.Mode) (t : D.Coord ⊕ Unit → A) (o : Bool) : D.all.ExitAt v (some m, t) o ↔ D.ExitAt (vy v (t (Sum.inr ()))) (m, t ∘ Sum.inl) o ∧ (o = true → ∀ (a : A), a ≤ t (Sum.inr ()))

theorem DescriptiveComplexity.Decider.reachAt_all_of_reachAt {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {y : A} {a b : D.Node A} (h : D.ReachAt (vy v y) a b) : D.all.ReachAt v (some a.1, Sum.elim a.2 fun (x : Unit) => y) (some b.1, Sum.elim b.2 fun (x : Unit) => y)

A path of the component lifts to the iteration, the element fixed.

theorem DescriptiveComplexity.Decider.all_reach_yes {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) [Finite A] {P : A → Prop} (h : ∀ (y : A), D.Decides (vy v y) (P y)) (y : A) (hy : ∀ (y' : A), y ≤ y' → P y') (u : D.Coord → A) : ∃ (c : D.all.Node A), D.all.ReachAt v (some D.start, Sum.elim u fun (x : Unit) => y) c ∧ D.all.ExitAt v c true

Upwards from any element: if the component says yes at every element from y on, the iteration exits yes from the component's start at y.

theorem DescriptiveComplexity.Decider.all_reach_no {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) [Finite A] {P : A → Prop} (h : ∀ (y : A), D.Decides (vy v y) (P y)) (hnot : ¬∀ (y : A), P y) (y : A) (hy : ∀ y' < y, P y') (u : D.Coord → A) : ∃ (c : D.all.Node A), D.all.ReachAt v (some D.start, Sum.elim u fun (x : Unit) => y) c ∧ D.all.ExitAt v c false

Upwards to a failure: if the component says yes below y but not everywhere, the iteration exits no from the component's start at y.

def DescriptiveComplexity.Decider.AllInv {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) (P : A → Prop) (t : D.Coord ⊕ Unit → A) (c : D.all.Node A) : Prop

What the iteration may have reached: its start, or a node of the component at some element, every smaller element having been answered yes.

Equations

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

theorem DescriptiveComplexity.Decider.allInv_of_reachAt {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) {P : A → Prop} (h : ∀ (y : A), D.Decides (vy v y) (P y)) (t : D.Coord ⊕ Unit → A) {c : D.all.Node A} (hc : D.all.ReachAt v (none, t) c) : D.AllInv v P t c

theorem DescriptiveComplexity.Decider.out_all {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) [Finite A] [Nonempty A] {P : A → Prop} (h : ∀ (y : A), D.Decides (vy v y) (P y)) (t : D.Coord ⊕ Unit → A) : (D.all.Out v t true ↔ ∀ (y : A), P y) ∧ (D.all.Out v t false ↔ ¬∀ (y : A), P y)

theorem DescriptiveComplexity.Decider.decides_all {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (v : β → A) [Finite A] [Nonempty A] {P : A → Prop} (h : ∀ (y : A), D.Decides (vy v y) (P y)) : D.all.Decides v (∀ (y : A), P y)

The iteration decides the universal quantification.

theorem DescriptiveComplexity.Decider.functional_all {L : FirstOrder.Language} {β : Type} (D : Decider L (β ⊕ Unit)) {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) : D.all.Functional A

Quantifying over a tuple, and the derived connectives

def DescriptiveComplexity.Decider.snocVar (β : Type) (K : ℕ) : β ⊕ Fin (K + 1) → (β ⊕ Fin K) ⊕ Unit

The parameters of a decider over a tuple of K + 1 variables, read as the parameters over K variables together with one more.

Equations

• DescriptiveComplexity.Decider.snocVar β K = Sum.elim (fun (b : β) => Sum.inl (Sum.inl b)) fun (i : Fin (K + 1)) => Fin.lastCases (Sum.inr ()) (fun (i : Fin K) => Sum.inl (Sum.inr i)) i

@[reducible]

noncomputable def DescriptiveComplexity.Decider.allTup {L : FirstOrder.Language} {β : Type} (K : ℕ) : Decider L (β ⊕ Fin K) → Decider L β

Universal quantification over a tuple: one iteration per coordinate.

Equations

• DescriptiveComplexity.Decider.allTup 0 D = D.relabelPar (Sum.elim id Fin.elim0)
• DescriptiveComplexity.Decider.allTup K.succ D = DescriptiveComplexity.Decider.allTup K (D.relabelPar (DescriptiveComplexity.Decider.snocVar x✝ K)).all

@[reducible]

noncomputable def DescriptiveComplexity.Decider.exTup {L : FirstOrder.Language} {β : Type} (K : ℕ) (D : Decider L (β ⊕ Fin K)) : Decider L β

Existential quantification over a tuple, by De Morgan.

Equations

• DescriptiveComplexity.Decider.exTup K D = (DescriptiveComplexity.Decider.allTup K D.neg).neg

@[reducible]

noncomputable def DescriptiveComplexity.Decider.imp {L : FirstOrder.Language} {β : Type} (D₁ D₂ : Decider L β) : Decider L β

Implication, by De Morgan: not (the first and not the second).

Equations

• D₁.imp D₂ = (D₁.seq D₂.neg).neg

theorem DescriptiveComplexity.Decider.decides_allTup {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} (K : ℕ) (D : Decider L (β ⊕ Fin K)) (v : β → A) {P : (Fin K → A) → Prop} (h : ∀ (xs : Fin K → A), D.Decides (Sum.elim v xs) (P xs)) : (allTup K D).Decides v (∀ (xs : Fin K → A), P xs)

theorem DescriptiveComplexity.Decider.functional_allTup {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {β : Type} (K : ℕ) (D : Decider L (β ⊕ Fin K)) (h : D.Functional A) : (allTup K D).Functional A

theorem DescriptiveComplexity.Decider.decides_exTup {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} (K : ℕ) (D : Decider L (β ⊕ Fin K)) (v : β → A) {P : (Fin K → A) → Prop} (h : ∀ (xs : Fin K → A), D.Decides (Sum.elim v xs) (P xs)) : (exTup K D).Decides v (∃ (xs : Fin K → A), P xs)

theorem DescriptiveComplexity.Decider.functional_exTup {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {β : Type} (K : ℕ) (D : Decider L (β ⊕ Fin K)) (h : D.Functional A) : (exTup K D).Functional A

theorem DescriptiveComplexity.Decider.decides_imp {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {β : Type} (D₁ D₂ : Decider L β) (v : β → A) {P Q : Prop} (h₁ : D₁.Decides v P) (h₂ : D₂.Decides v Q) : (D₁.imp D₂).Decides v (P → Q)

theorem DescriptiveComplexity.Decider.functional_imp {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {β : Type} (D₁ D₂ : Decider L β) (h₁ : D₁.Functional A) (h₂ : D₂.Functional A) : (D₁.imp D₂).Functional A

A decider with no parameters is a specification

noncomputable def DescriptiveComplexity.Decider.coordEquiv {L : FirstOrder.Language} (D : Decider L Empty) : D.Coord ≃ Fin (Nat.card D.Coord)

The coordinates of a decider, enumerated.

Equations

• D.coordEquiv = (Fintype.equivFin D.Coord).trans (finCongr ⋯)

noncomputable def DescriptiveComplexity.Decider.specVar {L : FirstOrder.Language} (D : Decider L Empty) : (D.Coord ⊕ D.Coord) ⊕ Empty → Fin (Nat.card D.Coord) ⊕ Fin (Nat.card D.Coord)

The variables of the decider's step, as the specification's.

Equations

• D.specVar = Sum.elim (Sum.map ⇑D.coordEquiv ⇑D.coordEquiv) Empty.elim

noncomputable def DescriptiveComplexity.Decider.specExitVar {L : FirstOrder.Language} (D : Decider L Empty) : D.Coord ⊕ Empty → Fin (Nat.card D.Coord) ⊕ Fin (Nat.card D.Coord)

The variables of the decider's exit, as the specification's step.

Equations

• D.specExitVar = Sum.elim (fun (c : D.Coord) => Sum.inl (D.coordEquiv c)) Empty.elim

@[reducible]

noncomputable def DescriptiveComplexity.Decider.toSpec {L : FirstOrder.Language} (D : Decider L Empty) : TCSpec L

A decider as a specification: the two exits become two terminal modes, the yes one accepting; the start mode is the source, at any tuple.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.noPar (A : Type) : Empty → A

The valuation of the (absent) parameters.

Equations

• DescriptiveComplexity.Decider.noPar A z = z.elim

theorem DescriptiveComplexity.Decider.step_toSpec_inl_inl {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (m n : D.Mode) (x x' : Fin (Nat.card D.Coord) → A) : D.toSpec.Step (Sum.inl m, x) (Sum.inl n, x') ↔ D.StepAt (noPar A) (m, x ∘ ⇑D.coordEquiv) (n, x' ∘ ⇑D.coordEquiv)

theorem DescriptiveComplexity.Decider.step_toSpec_inl_inr {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (m : D.Mode) (o : Bool) (x x' : Fin (Nat.card D.Coord) → A) : D.toSpec.Step (Sum.inl m, x) (Sum.inr o, x') ↔ D.ExitAt (noPar A) (m, x ∘ ⇑D.coordEquiv) o ∧ x' = x

theorem DescriptiveComplexity.Decider.not_step_toSpec_inr {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (o : Bool) (n : D.Mode ⊕ Bool) (x x' : Fin (Nat.card D.Coord) → A) : ¬D.toSpec.Step (Sum.inr o, x) (n, x')

theorem DescriptiveComplexity.Decider.isSrc_toSpec_inl {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (m : D.Mode) (x : Fin (Nat.card D.Coord) → A) : D.toSpec.IsSrc (Sum.inl m, x) ↔ m = D.start

theorem DescriptiveComplexity.Decider.not_isSrc_toSpec_inr {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (o : Bool) (x : Fin (Nat.card D.Coord) → A) : ¬D.toSpec.IsSrc (Sum.inr o, x)

theorem DescriptiveComplexity.Decider.isTgt_toSpec {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (m : D.Mode ⊕ Bool) (x : Fin (Nat.card D.Coord) → A) : D.toSpec.IsTgt (m, x) ↔ m = Sum.inr true

theorem DescriptiveComplexity.Decider.toSpec_invariant {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (x : Fin (Nat.card D.Coord) → A) {c : D.toSpec.Node A} (h : D.toSpec.Reach (Sum.inl D.start, x) c) : (∃ (m : D.Mode) (x' : Fin (Nat.card D.Coord) → A), c = (Sum.inl m, x') ∧ D.ReachAt (noPar A) (D.start, x ∘ ⇑D.coordEquiv) (m, x' ∘ ⇑D.coordEquiv)) ∨ ∃ (o : Bool) (x' : Fin (Nat.card D.Coord) → A), c = (Sum.inr o, x') ∧ D.Out (noPar A) (x ∘ ⇑D.coordEquiv) o

What the specification reaches from its source: a node of the decider it reaches, or an exit it reaches.

theorem DescriptiveComplexity.Decider.reach_toSpec_of_reachAt {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] {a b : D.Node A} (h : D.ReachAt (noPar A) a b) : D.toSpec.Reach (Sum.inl a.1, a.2 ∘ ⇑D.coordEquiv.symm) (Sum.inl b.1, b.2 ∘ ⇑D.coordEquiv.symm)

A path of the decider is a path of the specification.

theorem DescriptiveComplexity.Decider.accepts_toSpec {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {P : Prop} (h : D.Decides (noPar A) P) : D.toSpec.Accepts A ↔ P

The specification accepts exactly when the decider says yes from some tuple.

theorem DescriptiveComplexity.Decider.functional_toSpec {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] (h : D.Functional A) : D.toSpec.Functional A

A functional decider gives a functional specification.

theorem DescriptiveComplexity.Decider.det_accepts_toSpec {L : FirstOrder.Language} (D : Decider L Empty) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {P : Prop} (h : D.Decides (noPar A) P) (hf : D.Functional A) : D.toSpec.det.Accepts A ↔ P

A functional decider's specification is unchanged by determinization: its deterministic reading accepts exactly when the decider says yes.