A walk over an expansion, with endpoints, as one decider

The last assembly step of the normal form: an FO(TC) sentence over an expansion – a walk whose step, source and target formulas read the relations of a block that has deciders – is decided by one DescriptiveComplexity.Decider over the base vocabulary (DescriptiveComplexity.ParamTCSpec.sentenceDecider), hence is one DescriptiveComplexity.TCSpec (DescriptiveComplexity.Decider.toSpec).

The sentence says “some source node reaches some target node”. Its modes are finite, so it is a finite disjunction over the pairs of modes (DescriptiveComplexity.Decider.listOr); at a pair, the two tuples are existentially quantified (DescriptiveComplexity.Decider.exTup), the source and target formulas are decided by DescriptiveComplexity.Decider.exists_of_formula, and reachability is that of the flat walk (DescriptiveComplexity.ParamTCSpec.flat) between the encodings of the two nodes, decided by DescriptiveComplexity.ParamTCSpec.reachDecider – or, deterministically, by DescriptiveComplexity.ParamTCSpec.detReachDecider on the searching flat walk, which is functional. The encodings are two more quantified tuples, pinned by a formula (DescriptiveComplexity.ParamTCSpec.encF).

Finite disjunctions of deciders

@[reducible]

noncomputable def DescriptiveComplexity.Decider.listOr {L : FirstOrder.Language} {β : Type} : List (Decider L β) → Decider L β

The disjunction of a list of deciders, by De Morgan.

Equations

• DescriptiveComplexity.Decider.listOr [] = DescriptiveComplexity.Decider.atom ⊥
• DescriptiveComplexity.Decider.listOr (D :: l) = (D.neg.seq (DescriptiveComplexity.Decider.listOr l).neg).neg

theorem DescriptiveComplexity.Decider.decides_listOr {L : FirstOrder.Language} {β A : Type} [L.Structure A] [LinearOrder A] (l : List (Decider L β)) (v : β → A) {P : Decider L β → Prop} (h : ∀ D ∈ l, D.Decides v (P D)) : (listOr l).Decides v (∃ D ∈ l, P D)

theorem DescriptiveComplexity.Decider.functional_listOr {L : FirstOrder.Language} {β A : Type} [L.Structure A] [LinearOrder A] (l : List (Decider L β)) (h : ∀ D ∈ l, D.Functional A) : (listOr l).Functional A

The sentence decider

noncomputable def DescriptiveComplexity.ParamTCSpec.allPairs {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) : List (S.Mode × S.Mode)

The pairs of modes, listed.

Equations

• S.allPairs = Finset.univ.toList

theorem DescriptiveComplexity.ParamTCSpec.mem_allPairs {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (p : S.Mode × S.Mode) : p ∈ S.allPairs

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.Par4 {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) : Type

The parameters of the innermost decider: the outer parameters, the source tuple, the target tuple, and the two encodings.

Equations

• S.Par4 D det = ((((Fin S.par ⊕ Fin S.k) ⊕ Fin S.k) ⊕ Fin (Nat.card (S.flat D det).Coord)) ⊕ Fin (Nat.card (S.flat D det).Coord))

noncomputable def DescriptiveComplexity.ParamTCSpec.encF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {γ : Type} (x : Fin S.k → γ) (w : Fin (Nat.card (S.flat D det).Coord) → γ) : (L.sum FirstOrder.Language.order).Formula γ

“The tuple w encodes the node with tuple x”: on the current coordinates it is x, everywhere else the minimum.

Equations

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

def DescriptiveComplexity.ParamTCSpec.srcVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin S.k → S.Par4 D det

The variables of the source formula's decider.

Equations

• S.srcVar D i = Sum.inl (Sum.inl (Sum.inl (Sum.inr i)))

def DescriptiveComplexity.ParamTCSpec.tgtVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin S.k → S.Par4 D det

The variables of the target formula's decider.

Equations

• S.tgtVar D i = Sum.inl (Sum.inl (Sum.inr i))

def DescriptiveComplexity.ParamTCSpec.enc₁Var {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin (Nat.card (S.flat D det).Coord) → S.Par4 D det

The variables of the first encoding.

Equations

• S.enc₁Var D j = Sum.inl (Sum.inr j)

def DescriptiveComplexity.ParamTCSpec.enc₂Var {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin (Nat.card (S.flat D det).Coord) → S.Par4 D det

The variables of the second encoding.

Equations

• S.enc₂Var D j = Sum.inr j

def DescriptiveComplexity.ParamTCSpec.parVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin S.par → S.Par4 D det

The variables of the outer parameters.

Equations

• S.parVar D i = Sum.inl (Sum.inl (Sum.inl (Sum.inl i)))

noncomputable def DescriptiveComplexity.ParamTCSpec.reachVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} : Fin (Nat.card (S.flat D det).Coord + Nat.card (S.flat D det).Coord + S.par) → S.Par4 D det

The variables of the reachability decider of the flat walk.

Equations

• S.reachVar D = DescriptiveComplexity.ParamTCSpec.pack (S.enc₁Var D) (S.enc₂Var D) (S.parVar D)

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.pairDecider {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) (Dsrc Dtgt : S.Mode → Decider L (Fin S.k)) (Dr : S.Mode → S.Mode → Decider L (Fin (Nat.card (S.flat D det).Coord + Nat.card (S.flat D det).Coord + S.par))) (p : S.Mode × S.Mode) : Decider L (Fin S.par)

The decider of one pair of modes: some source tuple, some target tuple, their two encodings, and reachability between the encodings.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.sentenceDecider {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) (Dsrc Dtgt : S.Mode → Decider L (Fin S.k)) (Dr : S.Mode → S.Mode → Decider L (Fin (Nat.card (S.flat D det).Coord + Nat.card (S.flat D det).Coord + S.par))) : Decider L (Fin S.par)

The sentence decider: the disjunction over the pairs of modes.

Equations

• S.sentenceDecider D det Dsrc Dtgt Dr = DescriptiveComplexity.Decider.listOr (List.map (S.pairDecider D det Dsrc Dtgt Dr) S.allPairs)

Semantics

theorem DescriptiveComplexity.ParamTCSpec.realize_encF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) {γ : Type} (x : Fin S.k → γ) (w : Fin (Nat.card (S.flat D det).Coord) → γ) (v : γ → A) : (S.encF D x w).Realize v ↔ (v ∘ w) ∘ ⇑(S.flat D det).coordEquiv = Sum.elim (Sum.elim (v ∘ x) fun (x : Fin S.k) => a₀) fun (x : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) => a₀

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.val4 {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) {A : Type} (z : Fin S.par → A) (x y : Fin S.k → A) (w₁ w₂ : Fin (Nat.card (S.flat D det).Coord) → A) : S.Par4 D det → A

The valuation of the innermost parameters.

Equations

• S.val4 D det z x y w₁ w₂ = Sum.elim (Sum.elim (Sum.elim (Sum.elim z x) y) w₁) w₂