From FO(TC) to the Krom fragment, through the complement

The complement of an FO(TC) definable problem is SO-Krom definable (DescriptiveComplexity.SigmaSOKromDefinable.compl_of_tcDefinable), hence in DescriptiveComplexity.NL.

The program is the general form of the one that defines UNREACH in DescriptiveComplexity.Problems.Reachability. Guess the set U of nodes from which an accepting node is reachable; a node being a mode together with a k-tuple, that set is one k-ary relation variable per mode – the block's index type is the specification's mode type. The clauses run over 2k universally quantified first-order variables, the first k holding the tuple x̄ of the current node and the last k the tuple ȳ of the next one:

                   tgt_p(x̄) → U_p(x̄)              (one clause per mode `p`)
  step_{p,q}(x̄, ȳ)          → ¬U_q(ȳ) ∨ U_p(x̄)   (one per pair of modes)
                   src_p(x̄) → ¬U_p(x̄)             (one clause per mode `p`)

All guards are the specification's own first-order formulas, relabelled along the two halves of Fin (k + k); the middle family is the only one with two literals, and it is what makes the program Krom rather than Horn.

Correctness is the argument the concrete case already used, with nodes in place of vertices: the witness is U = {a | some accepting node is reachable from a}, and conversely a set containing the accepting nodes and closed under predecessors contains every node from which one is reachable, so a starting node could not be excluded if the structure were accepted.

This is the direction that is free. The converse – expressing reachability itself in the Krom fragment – is Immerman–Szelepcsényi, proved through FO(TC) in DescriptiveComplexity.ImmermanSzelepcsenyi; see also the discussion in DescriptiveComplexity.LogSpace.

The block, the halves, and the modes

@[reducible, inline]

abbrev DescriptiveComplexity.TCKrom.uBlock {L : FirstOrder.Language} (spec : TCSpec L) : SOBlock

The block of the Krom program: one k-ary relation variable per mode, together holding the set of nodes from which an accepting node is reachable. An abbrev, so that the arity reduces where tuples are applied.

Equations

• DescriptiveComplexity.TCKrom.uBlock spec = { ι := spec.Mode, ιFinite := ⋯, arity := fun (x : spec.Mode) => spec.k }

@[reducible, inline]

abbrev DescriptiveComplexity.TCKrom.fst (k : ℕ) : Fin k → Fin (k + k)

The first half of the 2k universally quantified variables: the tuple x̄ of the current node.

Equations

• DescriptiveComplexity.TCKrom.fst k = Fin.castAdd k

@[reducible, inline]

abbrev DescriptiveComplexity.TCKrom.snd (k : ℕ) : Fin k → Fin (k + k)

The second half of the 2k universally quantified variables: the tuple ȳ of the next node.

Equations

• DescriptiveComplexity.TCKrom.snd k = Fin.natAdd k

def DescriptiveComplexity.TCKrom.uAtom {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) (half : Fin spec.k → Fin (spec.k + spec.k)) : SOAtom (uBlock spec) (spec.k + spec.k)

The atom U_m at one of the two halves.

Equations

• DescriptiveComplexity.TCKrom.uAtom spec m half = { idx := m, args := half }

def DescriptiveComplexity.TCKrom.uLit {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) (half : Fin spec.k → Fin (spec.k + spec.k)) (pos : Bool) : KromLit (uBlock spec) (spec.k + spec.k)

The literal U_m at one of the two halves, positive or negated.

Equations

• DescriptiveComplexity.TCKrom.uLit spec m half pos = { atom := DescriptiveComplexity.TCKrom.uAtom spec m half, positive := pos }

noncomputable def DescriptiveComplexity.TCKrom.allModes {L : FirstOrder.Language} (spec : TCSpec L) : List spec.Mode

The modes, as a list: the clause families are instantiated at each of them.

Equations

• DescriptiveComplexity.TCKrom.allModes spec = Finset.univ.toList

theorem DescriptiveComplexity.TCKrom.mem_allModes {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : m ∈ allModes spec

The clauses

noncomputable def DescriptiveComplexity.TCKrom.tgtClause {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : KromClause (L.sum FirstOrder.Language.order) (uBlock spec) (spec.k + spec.k)

An accepting node belongs to U.

Equations

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

noncomputable def DescriptiveComplexity.TCKrom.stepClause {L : FirstOrder.Language} (spec : TCSpec L) (p q : spec.Mode) : KromClause (L.sum FirstOrder.Language.order) (uBlock spec) (spec.k + spec.k)

U is closed under predecessors: a step into U starts in U.

Equations

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

noncomputable def DescriptiveComplexity.TCKrom.srcClause {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : KromClause (L.sum FirstOrder.Language.order) (uBlock spec) (spec.k + spec.k)

No starting node belongs to U.

Equations

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

noncomputable def DescriptiveComplexity.TCKrom.program {L : FirstOrder.Language} (spec : TCSpec L) : KromProgram (L.sum FirstOrder.Language.order) (uBlock spec) (spec.k + spec.k)

The Krom program defining the complement of an FO(TC) definable problem.

Equations

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

theorem DescriptiveComplexity.TCKrom.tgtClause_mem {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : tgtClause spec m ∈ program spec

theorem DescriptiveComplexity.TCKrom.stepClause_mem {L : FirstOrder.Language} (spec : TCSpec L) (p q : spec.Mode) : stepClause spec p q ∈ program spec

theorem DescriptiveComplexity.TCKrom.srcClause_mem {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : srcClause spec m ∈ program spec

theorem DescriptiveComplexity.TCKrom.mem_program_iff {L : FirstOrder.Language} (spec : TCSpec L) {c : KromClause (L.sum FirstOrder.Language.order) (uBlock spec) (spec.k + spec.k)} : c ∈ program spec ↔ (∃ (m : spec.Mode), c = tgtClause spec m) ∨ (∃ (p : spec.Mode) (q : spec.Mode), c = stepClause spec p q) ∨ ∃ (m : spec.Mode), c = srcClause spec m

The clauses of the program are exactly the three families.

Semantics

def DescriptiveComplexity.TCKrom.URel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (ρ : (uBlock spec).Assignment A) (a : spec.Node A) : Prop

The set of nodes guessed by an assignment of the block.

Equations

• DescriptiveComplexity.TCKrom.URel spec ρ a = ρ a.1 a.2

def DescriptiveComplexity.TCKrom.pairVal {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x y : Fin spec.k → A) : Fin (spec.k + spec.k) → A

The valuation of the 2k variables holding the tuples of two nodes.

Equations

• DescriptiveComplexity.TCKrom.pairVal spec x y i = Fin.addCases x y i

@[simp]

theorem DescriptiveComplexity.TCKrom.pairVal_fst {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x y : Fin spec.k → A) (j : Fin spec.k) : pairVal spec x y (fst spec.k j) = x j

@[simp]

theorem DescriptiveComplexity.TCKrom.pairVal_snd {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x y : Fin spec.k → A) (j : Fin spec.k) : pairVal spec x y (snd spec.k j) = y j

theorem DescriptiveComplexity.TCKrom.uLit_holds_true {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (ρ : (uBlock spec).Assignment A) (m : spec.Mode) (half : Fin spec.k → Fin (spec.k + spec.k)) (v : Fin (spec.k + spec.k) → A) : (uLit spec m half true).Holds ρ v ↔ URel spec ρ (m, fun (j : Fin spec.k) => v (half j))

theorem DescriptiveComplexity.TCKrom.uLit_holds_false {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (ρ : (uBlock spec).Assignment A) (m : spec.Mode) (half : Fin spec.k → Fin (spec.k + spec.k)) (v : Fin (spec.k + spec.k) → A) : (uLit spec m half false).Holds ρ v ↔ ¬URel spec ρ (m, fun (j : Fin spec.k) => v (half j))

theorem DescriptiveComplexity.TCKrom.realize_tgt_relabel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) (v : Fin (spec.k + spec.k) → A) : (FirstOrder.Language.Formula.relabel (fst spec.k) (spec.tgt m)).Realize v ↔ spec.IsTgt (m, fun (j : Fin spec.k) => v (fst spec.k j))

theorem DescriptiveComplexity.TCKrom.realize_src_relabel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) (v : Fin (spec.k + spec.k) → A) : (FirstOrder.Language.Formula.relabel (fst spec.k) (spec.src m)).Realize v ↔ spec.IsSrc (m, fun (j : Fin spec.k) => v (fst spec.k j))

theorem DescriptiveComplexity.TCKrom.realize_step_relabel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (p q : spec.Mode) (v : Fin (spec.k + spec.k) → A) : (FirstOrder.Language.Formula.relabel (Sum.elim (fst spec.k) (snd spec.k)) (spec.step p q)).Realize v ↔ spec.Step (p, fun (j : Fin spec.k) => v (fst spec.k j)) (q, fun (j : Fin spec.k) => v (snd spec.k j))

theorem DescriptiveComplexity.TCKrom.program_holds_iff {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ : (uBlock spec).Assignment A) : (program spec).Holds ρ ↔ (∀ (a : spec.Node A), spec.IsTgt a → URel spec ρ a) ∧ (∀ (a b : spec.Node A), spec.Step a b → URel spec ρ b → URel spec ρ a) ∧ ∀ (a : spec.Node A), spec.IsSrc a → ¬URel spec ρ a

What it means for an assignment to satisfy the program: the guessed set contains the accepting nodes, is closed under predecessors, and avoids the starting nodes.

def DescriptiveComplexity.TCKrom.coReachAssign {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : (uBlock spec).Assignment A

The set of nodes from which an accepting node is reachable: the witness of the nontrivial direction.

Equations

• DescriptiveComplexity.TCKrom.coReachAssign spec m x = ∃ (w : spec.Node A), spec.IsTgt w ∧ spec.Reach (m, x) w

@[simp]

theorem DescriptiveComplexity.TCKrom.uRel_coReachAssign {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a : spec.Node A) : URel spec (coReachAssign spec) a ↔ ∃ (w : spec.Node A), spec.IsTgt w ∧ spec.Reach a w

theorem DescriptiveComplexity.TCKrom.uRel_of_reach {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] {ρ : (uBlock spec).Assignment A} (h2 : ∀ (a b : spec.Node A), spec.Step a b → URel spec ρ b → URel spec ρ a) {a b : spec.Node A} (h : spec.Reach a b) : URel spec ρ b → URel spec ρ a

A set containing the accepting nodes and closed under predecessors contains every node from which an accepting node is reachable.

theorem DescriptiveComplexity.TCKrom.exists_holds_iff_not_accepts {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : (∃ (ρ : (uBlock spec).Assignment A), (program spec).Holds ρ) ↔ ¬spec.Accepts A

Correctness: the program is satisfiable exactly when the structure is not accepted.

theorem DescriptiveComplexity.SigmaSOKromDefinable.compl_of_tcDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : TCDefinable P) : SigmaSOKromDefinable Pᶜ

The complement of an FO(TC) definable problem is SO-Krom definable: guess the set of nodes from which an accepting node is reachable – one k-ary relation variable per mode – close it under predecessors with the 2-clause ¬U_q(ȳ) ∨ U_p(x̄), and forbid the starting nodes. This is the direction a clausal fragment gives for free; the converse is Immerman–Szelepcsényi.

theorem DescriptiveComplexity.mem_NL_compl_of_tcDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : TCDefinable P) : NL.Mem Pᶜ

The complement of an FO(TC) definable problem is in NL.