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.decides_listOr_map {L : FirstOrder.Language} {β A : Type} [L.Structure A] [LinearOrder A] {ι : Type} (l : List ι) (f : ι → Decider L β) (v : β → A) {P : ι → Prop} (h : ∀ i ∈ l, (f i).Decides v (P i)) : (listOr (List.map f l)).Decides v (∃ i ∈ l, P i)

The disjunction of a family of deciders indexed by a list.

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

theorem DescriptiveComplexity.Decider.exists_of_formula₀ {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} (ρ : (A : Type) → [L.Structure A] → [LinearOrder A] → B.Assignment A) (Dq : (q : B.ι) → Decider L (Fin (B.arity q))) (hD : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : B.ι) (w : Fin (B.arity q) → A), (Dq q).Decides w (ρ A q w)) {α : Type} (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Formula α) : ∃ (D : Decider L α), (∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (v : α → A), D.Decides v (φ.Realize v)) ∧ ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A], (∀ (q : B.ι), (Dq q).Functional A) → D.Functional A

A formula with free variables, decided; the sentence-level instance of DescriptiveComplexity.Decider.exists_of_formula.

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₂

def DescriptiveComplexity.ParamTCSpec.DecidesReach {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) (Dr : S.Mode → S.Mode → Decider L (Fin (Nat.card (S.flat D det).Coord + Nat.card (S.flat D det).Coord + S.par))) (A : Type) [L.Structure A] [LinearOrder A] : Prop

What the reachability deciders of the flat walk decide, in the two readings.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.decides_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) (Ssrc Stgt : S.Mode → ((L.sum FirstOrder.Language.order).sum B.lang).Formula (Fin S.k)) (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))) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (z : Fin S.par → A) (p : S.Mode × S.Mode) (hsrc : ∀ (m : S.Mode) (x : Fin S.k → A), (Dsrc m).Decides x ((Ssrc m).Realize x)) (htgt : ∀ (m : S.Mode) (x : Fin S.k → A), (Dtgt m).Decides x ((Stgt m).Realize x)) (hr : S.DecidesReach D det Dr A) (hsim : ∀ (a b : S.Node A), (S.flat D det).ReachAt z (S.flatEnc D det a₀ a) (S.flatEnc D det a₀ b) ↔ S.ReachAt z a b) : (S.pairDecider D det Dsrc Dtgt Dr p).Decides z (∃ (x : Fin S.k → A) (y : Fin S.k → A), (Ssrc p.1).Realize x ∧ (Stgt p.2).Realize y ∧ S.ReachAt z (p.1, x) (p.2, y))

The pair decider decides: some source tuple and some target tuple, the outer walk reaching the target from the source – given that the flat walk simulates the outer one at the encodings.

theorem DescriptiveComplexity.ParamTCSpec.decides_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) (Ssrc Stgt : S.Mode → ((L.sum FirstOrder.Language.order).sum B.lang).Formula (Fin S.k)) (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))) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (z : Fin S.par → A) (hsrc : ∀ (m : S.Mode) (x : Fin S.k → A), (Dsrc m).Decides x ((Ssrc m).Realize x)) (htgt : ∀ (m : S.Mode) (x : Fin S.k → A), (Dtgt m).Decides x ((Stgt m).Realize x)) (hr : S.DecidesReach D det Dr A) (hsim : ∀ (a b : S.Node A), (S.flat D det).ReachAt z (S.flatEnc D det a₀ a) (S.flatEnc D det a₀ b) ↔ S.ReachAt z a b) : (S.sentenceDecider D det Dsrc Dtgt Dr).Decides z (∃ (a : S.Node A) (b : S.Node A), (Ssrc a.1).Realize a.2 ∧ (Stgt b.1).Realize b.2 ∧ S.ReachAt z a b)

The sentence decider decides the sentence: some source node reaches some target node in the outer walk.

theorem DescriptiveComplexity.ParamTCSpec.functional_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))) {A : Type} [L.Structure A] [LinearOrder A] (hsrc : ∀ (m : S.Mode), (Dsrc m).Functional A) (htgt : ∀ (m : S.Mode), (Dtgt m).Functional A) (hr : ∀ (m n : S.Mode), (Dr m n).Functional A) : (S.sentenceDecider D det Dsrc Dtgt Dr).Functional A

The sentence decider is functional when its components are.