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

The formula layer of the converse translation: the implication graph of a Krom program, walked by a DescriptiveComplexity.TCSpec.

DescriptiveComplexity.KromImpl.exists_holds_iff says that a Krom program is satisfiable exactly when no goal clause fires and no literal reaches its own negation and back, and DescriptiveComplexity.TwoCnf.carryReach_iff turns the second condition – a conjunction of two reachabilities – into a single walk of the cycle-witnessing graph, on nodes carrying the start literal, the current one and a flag. This file expresses that walk as first-order data:

• a node's two literals are two modes (a relation variable of the block and a sign, twice) together with two tuples of dimension DescriptiveComplexity.clauseDim, holding the canonically padded arguments of the two atoms – the same encoding the Horn and Krom discharges use;
• the flag is a third component of the mode;
• an edge of the implication graph is DescriptiveComplexity.KromTC.edgeCaseF: for one clause of the program and one choice of which of its literal slots is the source and which the target, the clause's guard holds at some valuation of its k variables, and the two node tuples hold the canonically padded arguments of the two atoms at that valuation. Quantifying the valuation existentially and taking the disjunction over the program gives the transition formula.

The walk starts at a node whose two literals agree and whose flag is down, and accepts when they agree again with the flag up; one extra mode accepts reflexively when a goal clause fires, the empty clause of the 2-CNF. So the specification accepts exactly when the program is unsatisfiable (DescriptiveComplexity.KromTC.accepts_iff_not_exists_holds), which is DescriptiveComplexity.TCDefinable.compl_of_sigmaSOKromDefinable: the complement of an SO-Krom definable problem is FO(TC) definable. With the direction proved in DescriptiveComplexity.TransitiveClosureKrom this is an equivalence, co-NL(Krom) = NL(TC) (DescriptiveComplexity.mem_NL_iff_tcDefinable_compl); what it is not is REACH ∈ NL, which needs the complementation of FO(TC) itself (Immerman–Szelepcsényi).

The two halves of a node's tuple

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.fstHalf (D : ℕ) : Fin D → Fin (D + D)

The first half of a node's tuple: the arguments of the start literal's atom.

Equations

• DescriptiveComplexity.KromTC.fstHalf D = Fin.castAdd D

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.sndHalf (D : ℕ) : Fin D → Fin (D + D)

The second half of a node's tuple: the arguments of the current literal's atom.

Equations

• DescriptiveComplexity.KromTC.sndHalf D = Fin.natAdd D

The edge formula

noncomputable def DescriptiveComplexity.KromTC.edgeCaseF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (c : KromClause (L.sum FirstOrder.Language.order) B k) (a₁ a₂ : SOAtom B k) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

One way for a clause to contribute an edge: its guard holds at some valuation of its k universally quantified variables, the coordinates selected by u hold the canonically padded arguments of the source atom at that valuation, and those selected by w hold the arguments of the target atom.

Equations

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

The literal a node denotes

noncomputable def DescriptiveComplexity.KromTC.litAt {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : TwoCnf.Lit (KromImpl.KromAtom B A)

The literal denoted by a relation variable, a sign and a tuple: the atom holds the first B.arity i coordinates.

Equations

• DescriptiveComplexity.KromTC.litAt i s w = (⟨i, DescriptiveComplexity.pref ⋯ w⟩, s)

@[simp]

theorem DescriptiveComplexity.KromTC.litAt_fst_fst {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : (litAt i s w).1.fst = i

@[simp]

theorem DescriptiveComplexity.KromTC.litAt_snd {B : SOBlock} {k : ℕ} {A : Type} (i : B.ι) (s : Bool) (w : Fin (clauseDim B k) → A) : (litAt i s w).2 = s

The edges a clause contributes

noncomputable def DescriptiveComplexity.KromTC.clauseEdgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (c : KromClause (L.sum FirstOrder.Language.order) B k) (i j : B.ι) (s t : Bool) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

All the ways one clause contributes an edge from the literal (i, s) to the literal (j, t).

Equations

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

The edges of the program

The transition formula proper: the disjunction over the program of the edges each clause contributes. Its realization is a step of the implication graph of DescriptiveComplexity.KromImpl.clauseRel, together with the canonicity of the two node tuples – which the formula forces, each disjunct pinning both tuples to the padded arguments of its atoms.

noncomputable def DescriptiveComplexity.KromTC.edgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (i j : B.ι) (s t : Bool) (u w : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The edge relation of the whole program, from the literal (i, s) to the literal (j, t).

Equations

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

theorem DescriptiveComplexity.KromTC.realize_edgeF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : γ → A} {prog : KromProgram (L.sum FirstOrder.Language.order) B k} {i j : B.ι} {s t : Bool} {u w : Fin (clauseDim B k) → γ} : (edgeF prog i j s t u w).Realize v ↔ (Canon (B.arity i) fun (m : Fin (clauseDim B k)) => v (u m)) ∧ (Canon (B.arity j) fun (m : Fin (clauseDim B k)) => v (w m)) ∧ TwoCnf.Step (KromImpl.clauseRel prog) (litAt i s fun (m : Fin (clauseDim B k)) => v (u m)) (litAt j t fun (m : Fin (clauseDim B k)) => v (w m))

The transition formula is the implication graph: it holds exactly when both node tuples are canonically padded and the literals they denote form an edge.

The specification

The nodes of the walk are the nodes of the cycle-witnessing graph of DescriptiveComplexity.TwoCnf.carryReach_iff: the start literal, the current literal and a flag. The two literals' relation variables and signs, and the flag, are the mode; their arguments are the two halves of the tuple. One extra mode accepts reflexively when a goal clause fires.

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.LitMode (B : SOBlock) : Type

A literal's share of a mode: a relation variable of the block and a sign.

Equations

• DescriptiveComplexity.KromTC.LitMode B = (B.ι × Bool)

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.Mode (B : SOBlock) : Type

The modes of the walk: the two literals' shares and the flag, or the mode that reports a firing goal clause.

Equations

• DescriptiveComplexity.KromTC.Mode B = (DescriptiveComplexity.KromTC.LitMode B × DescriptiveComplexity.KromTC.LitMode B × Bool ⊕ Unit)

noncomputable def DescriptiveComplexity.KromTC.goalF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {γ : Type} : (L.sum FirstOrder.Language.order).Formula γ

Some goal clause of the program fires.

Equations

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

theorem DescriptiveComplexity.KromTC.realize_goalF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {γ A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {v : γ → A} : (goalF prog).Realize v ↔ KromImpl.GoalFires prog A

noncomputable def DescriptiveComplexity.KromTC.srcF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k))

The starting nodes: the current literal is the start, the flag is down, and both halves of the tuple are the same canonical padding – or a firing goal clause, in the reporting mode.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.KromTC.srcF prog (Sum.inr PUnit.unit) = DescriptiveComplexity.KromTC.goalF prog

noncomputable def DescriptiveComplexity.KromTC.tgtF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k))

The accepting nodes: the current literal is the start again, with the flag up – or a firing goal clause.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.KromTC.tgtF prog (Sum.inr PUnit.unit) = DescriptiveComplexity.KromTC.goalF prog

@[reducible, inline]

abbrev DescriptiveComplexity.KromTC.Walk (B : SOBlock) : Type

The payload of a walk mode: the two literals' shares and the flag.

Equations

• DescriptiveComplexity.KromTC.Walk B = (DescriptiveComplexity.KromTC.LitMode B × DescriptiveComplexity.KromTC.LitMode B × Bool)

noncomputable def DescriptiveComplexity.KromTC.stepWalkF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (p q : Walk B) : (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k) ⊕ Fin (clauseDim B k + clauseDim B k))

One step between two walk modes, as a formula on the two nodes' tuples: the start is kept, the current literal moves along an edge of the implication graph, and the flag may go up only on arrival at the negation of the start.

Stated on the payloads rather than on DescriptiveComplexity.KromTC.Mode, so that its realization lemma applies without unfolding a match.

Equations

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

noncomputable def DescriptiveComplexity.KromTC.stepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Mode B → Mode B → (L.sum FirstOrder.Language.order).Formula (Fin (clauseDim B k + clauseDim B k) ⊕ Fin (clauseDim B k + clauseDim B k))

One step: a step between walk modes, and nothing into or out of the mode that reports a firing goal clause.

Equations

• DescriptiveComplexity.KromTC.stepF prog (Sum.inl p) (Sum.inl q) = DescriptiveComplexity.KromTC.stepWalkF prog p q
• DescriptiveComplexity.KromTC.stepF prog x✝¹ x✝ = ⊥

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.KromTC.spec {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : TCSpec L

The specification: the cycle-witnessing walk of the program's implication graph, plus the mode reporting a firing goal clause.

Equations

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

Nodes and carry nodes

noncomputable def DescriptiveComplexity.KromTC.decodeNode {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : TwoCnf.CarryNode (KromImpl.KromAtom B A)

The carry node a walk node denotes.

Equations

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

def DescriptiveComplexity.KromTC.modeOf {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : Walk B

The walk mode of a carry node.

Equations

• DescriptiveComplexity.KromTC.modeOf n = ((n.1.1.fst, n.1.2), (n.2.1.1.fst, n.2.1.2), n.2.2)

noncomputable def DescriptiveComplexity.KromTC.tupleOf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : Fin (clauseDim B k + clauseDim B k) → A

The tuple of a carry node: the two atoms, canonically padded.

Equations

• DescriptiveComplexity.KromTC.tupleOf a₀ n i = Fin.addCases (DescriptiveComplexity.pad a₀ n.1.1.snd) (DescriptiveComplexity.pad a₀ n.2.1.1.snd) i

@[simp]

theorem DescriptiveComplexity.KromTC.tupleOf_fstHalf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) (m : Fin (clauseDim B k)) : tupleOf a₀ n (fstHalf (clauseDim B k) m) = pad a₀ n.1.1.snd m

@[simp]

theorem DescriptiveComplexity.KromTC.tupleOf_sndHalf {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) (m : Fin (clauseDim B k)) : tupleOf a₀ n (sndHalf (clauseDim B k) m) = pad a₀ n.2.1.1.snd m

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_fst {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).1 = (n.1.1.fst, n.1.2)

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_snd_fst {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).2.1 = (n.2.1.1.fst, n.2.1.2)

@[simp]

theorem DescriptiveComplexity.KromTC.modeOf_snd_snd {B : SOBlock} {A : Type} (n : TwoCnf.CarryNode (KromImpl.KromAtom B A)) : (modeOf n).2.2 = n.2.2

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_fst {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).1 = litAt p.1.1 p.1.2 fun (m : Fin (clauseDim B k)) => x (fstHalf (clauseDim B k) m)

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_snd_fst {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).2.1 = litAt p.2.1.1 p.2.1.2 fun (m : Fin (clauseDim B k)) => x (sndHalf (clauseDim B k) m)

@[simp]

theorem DescriptiveComplexity.KromTC.decodeNode_snd_snd {B : SOBlock} {k : ℕ} {A : Type} (p : Walk B) (x : Fin (clauseDim B k + clauseDim B k) → A) : (decodeNode p x).2.2 = p.2.2

theorem DescriptiveComplexity.KromTC.litAt_pad_self {B : SOBlock} {k : ℕ} {A : Type} (a₀ : A) (p : TwoCnf.Lit (KromImpl.KromAtom B A)) : litAt p.1.fst p.2 (pad a₀ p.1.snd) = p

Walks

The endpoints

Correctness

theorem DescriptiveComplexity.KromTC.accepts_iff_not_exists_holds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (spec prog).Accepts A ↔ ¬∃ (ρ : B.Assignment A), prog.Holds ρ

Correctness: the specification accepts exactly when the program is unsatisfiable – either a goal clause fires, in the reporting mode, or some literal of the implication graph reaches its own negation and back, which the cycle-witnessing walk sees as a walk from (p, p, false) to (p, p, true).

theorem DescriptiveComplexity.TCDefinable.compl_of_sigmaSOKromDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SigmaSOKromDefinable P) : TCDefinable Pᶜ

The complement of an SO-Krom definable problem is FO(TC) definable: a Krom program instantiated in a structure is a 2-CNF on the atoms of its block, so it is unsatisfiable exactly when a goal clause fires or some literal reaches its own negation and back, and the second condition is a single walk of the cycle-witnessing graph – whose nodes are a pair of literals and a flag, i.e., a mode and two canonically padded tuples. Together with DescriptiveComplexity.SigmaSOKromDefinable.compl_of_tcDefinable this gives co-NL(Krom) = NL(TC); it is upgraded to NL = coNL by Immerman–Szelepcsényi (DescriptiveComplexity.NL_eq_coNL). Registered in the Lax archive as Lax485149.KromAndTransitiveClosure.tcDefinable_compl_of_sigmaSOKromDefinable.

theorem DescriptiveComplexity.sigmaSOKromDefinable_iff_tcDefinable_compl {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : SigmaSOKromDefinable P ↔ TCDefinable Pᶜ

The two translations compose: a problem is SO-Krom definable exactly when its complement is FO(TC) definable, co-NL(Krom) = NL(TC).

theorem DescriptiveComplexity.mem_NL_iff_tcDefinable_compl {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : NL.Mem P ↔ TCDefinable Pᶜ

NL is the complements of the FO(TC) definable problems. Registered in the Lax archive as Lax485149.NLIsTransitiveClosure.mem_NL_iff_tcDefinable_compl.