Transitive closure logic and NL

AbbreviationOrdered graphs for first-order logic with transitive closure#✓fully proved

An ordered graph is encoded as a pair \((n, e)\) of a natural number \(n\), the domain size, and a finite list \(e\) of booleans of arbitrary length, the edge table in row-major order. It is read as the graph on \(\{0, \dots, n - 1\}\), ordered numerically, with an edge from \(a\) to \(b\) when the entry of \(e\) at position \(an + b\) is true; a missing entry counts as false.

abbrev TCOrderedGraph := ℕ × List Bool

Used by 7

Used byImmerman: FO + transitive closure is NL on ordered structures · Order and edge relations as FO + TC relation symbols · Definability in FO + TC · Edge relation of an ordered graph for FO + TC · Encodings of a class of ordered graphs · Evaluation of FO + TC formulas · Satisfaction of an FO + TC formula in an ordered graph

DefinitionEdge relation of an ordered graph for FO + TC#✓fully proved

For an ordered graph \((n, T)\) with edge table \(T\) and elements \(a, b < n\), there is an edge from \(a\) to \(b\) when the entry of \(T\) at position \(a n + b\) is true; positions beyond the end of \(T\) count as false.

def tcEdge (G : TCOrderedGraph) (a b : Fin G.1) : Prop :=
  G.2.getD (a.val * G.1 + b.val) false = true

Uses 1 · Used by 1

Statement usesOrdered graphs for first-order logic with transitive closure

Used byOrder and edge relations as FO + TC relation symbols

InductiveFormulas of first-order logic with transitive closure#✓fully proved

FO + TC formulas, with variables and relation symbols indexed by natural numbers, are built from equations between two variables and relation symbols applied to lists of variables by negation, conjunction, disjunction, existential quantification (which binds variable \(0\), de Bruijn style) and transitive closure \(\mathrm{TC}(\varphi; \bar u, \bar v)\) of a formula \(\varphi\) applied to two lists \(\bar u\), \(\bar v\) of variables. With \(a = |\bar u| = |\bar v|\), the body \(\varphi\) defines a step relation on \(a\)-tuples: its variables \(0, \dots, a - 1\) are the source tuple, \(a, \dots, 2a - 1\) the target tuple, and each variable \(j \ge 2a\) is outer variable \(j - 2a\).

inductive TCFO where
  | eq : ℕ → ℕ → TCFO
  | rel : ℕ → List ℕ → TCFO
  | not : TCFO → TCFO
  | and : TCFO → TCFO → TCFO
  | or : TCFO → TCFO → TCFO
  | exists : TCFO → TCFO
  | tc : TCFO → List ℕ → List ℕ → TCFO

Used by 5

Used byDefinability in FO + TC · Evaluation of FO + TC formulas · Example: simultaneous reachability of pairs in FO + TC · Example: parameterized transitive closure in FO + TC · Satisfaction of an FO + TC formula in an ordered graph

DefinitionOrder and edge relations as FO + TC relation symbols#✓fully proved

In an ordered graph with domain \(\{0, \dots, n - 1\}\), relation symbol \(0\) holds of a list of elements exactly when the list is \([a, b]\) with \(a < b\), relation symbol \(1\) holds exactly when the list is \([a, b]\) and there is an edge from \(a\) to \(b\), and every other relation symbol holds of no list.

def tcBase (G : TCOrderedGraph) (i : ℕ) : List (Fin G.1) → Prop :=
  match i with
  | 0 => fun args => match args with
    | [a, b] => a.val < b.val
    | _ => False
  | 1 => fun args => match args with
    | [a, b] => tcEdge G a b
    | _ => False
  | _ => fun _ => False

Uses 2 · Used by 1

Statement usesOrdered graphs for first-order logic with transitive closure · Edge relation of an ordered graph for FO + TC

Used bySatisfaction of an FO + TC formula in an ordered graph

DefinitionEvaluation of FO + TC formulas#✓fully proved

Fix an ordered graph with domain \(D = \{0, \dots, n - 1\}\), an assignment \(\rho\) of an element of \(D\) to each variable index and an assignment \(S\) of a relation on lists of elements of \(D\) to each relation symbol. The truth value of a formula is defined by recursion. The equation between variables \(i\) and \(j\) holds when \(\rho(i) = \rho(j)\). Relation symbol \(i\) applied to variables \(j_1, \dots, j_k\) holds when \(S_i\) holds of the list \([\rho(j_1), \dots, \rho(j_k)]\). Negation, conjunction and disjunction are interpreted as usual. An existential formula \(\exists \varphi\) holds when \(\varphi\) holds under the assignment sending \(0\) to some \(d \in D\) and \(j + 1\) to \(\rho(j)\). A transitive closure \(\mathrm{TC}(\varphi; \bar u, \bar v)\) is false when the index lists \(\bar u\) and \(\bar v\) have different lengths. Otherwise, with \(a\) their common length, it holds when the tuple \((\rho(v_0), \dots, \rho(v_{a-1}))\) is reachable from \((\rho(u_0), \dots, \rho(u_{a-1}))\) in zero or more steps, where a step from \(s \in D^a\) to \(t \in D^a\) means that \(\varphi\) holds under the assignment sending \(j < a\) to \(s_j\), \(a \le j < 2a\) to \(t_{j - a}\), and \(j \ge 2a\) to \(\rho(j - 2a)\).

MetaMathlibExt.Complexity.KeyTheorems.FOTC.tcEval · 18 lines

def tcEval (G : TCOrderedGraph) (ρ : ℕ → Fin G.1)
    (S : ℕ → List (Fin G.1) → Prop) : TCFO → Prop
  | .eq a b => ρ a = ρ b
  | .rel i args => S i (args.map ρ)
  | .not φ => ¬ tcEval G ρ S φ
  | .and φ ψ => tcEval G ρ S φ ∧ tcEval G ρ S ψ
  | .or φ ψ => tcEval G ρ S φ ∨ tcEval G ρ S ψ
  | .exists φ => ∃ a : Fin G.1,
      tcEval G (fun j => match j with | 0 => a | j + 1 => ρ j) S φ
  | .tc φ xs ys =>
      if h : xs.length = ys.length then
        Relation.ReflTransGen (fun s t : Fin xs.length → Fin G.1 =>
          tcEval G (fun j =>
            if hj : j < xs.length then s ⟨j, hj⟩
            else if hj2 : j < 2 * xs.length then t ⟨j - xs.length, by omega⟩
            else ρ (j - 2 * xs.length)) S φ)
          (fun i => ρ (xs.getD i.val 0)) (fun i => ρ (ys.getD i.val 0))
      else False

Uses 2 · Used by 1

Statement usesFormulas of first-order logic with transitive closure · Ordered graphs for first-order logic with transitive closure

Used bySatisfaction of an FO + TC formula in an ordered graph

DefinitionExample: parameterized transitive closure in FO + TC#✓fully proved

The FO + TC formula \(\mathrm{TC}(\varphi; (1), (2))\) of arity \(1\) whose body \(\varphi\) is \(E(0, 1) \lor (E(0, 2) \land E(2, 1))\), where \(E\) is relation symbol \(1\) (the edge relation). In the body, variable \(0\) is the source, variable \(1\) the target, and variable \(2\) is outer variable \(0\), shifted by \(2\); the endpoint arguments \(1\) and \(2\) are outer variables, not shifted. So the formula expresses that outer variable \(2\) is reachable from outer variable \(1\) by steps that are either an edge or a path of two edges through outer variable \(0\).

def tcParamExample : TCFO :=
  .tc (.or (.rel 1 [0, 1])
    (.and (.rel 1 [0, 2]) (.rel 1 [2, 1]))) [1] [2]

Uses 1

Statement usesFormulas of first-order logic with transitive closure

DefinitionExample: simultaneous reachability of pairs in FO + TC#✓fully proved

The FO + TC formula \(\mathrm{TC}(\varphi; (0, 1), (2, 3))\) of arity \(2\) whose body \(\varphi\) states that relation symbol \(1\) (the edge relation) holds of variables \(0, 2\) and of variables \(1, 3\). In the body, variables \(0, 1\) are the source pair and \(2, 3\) the target pair, so a step moves both components along an edge at the same time, and the formula expresses that the pair of outer variables \((2, 3)\) is reachable from the pair \((0, 1)\) by such steps.

def tcPairExample : TCFO :=
  .tc (.and (.rel 1 [0, 2]) (.rel 1 [1, 3])) [0, 1] [2, 3]

Uses 1

Statement usesFormulas of first-order logic with transitive closure

DefinitionSatisfaction of an FO + TC formula in an ordered graph#✓fully proved

An ordered graph with nonempty domain \(\{0, \dots, n - 1\}\) satisfies an FO + TC formula \(\varphi\) when \(\varphi\) evaluates to true with every variable assigned the element \(0\), relation symbol \(0\) interpreted as the order \(<\) and relation symbol \(1\) as the edge relation (both only on two-element lists), and every other relation symbol interpreted as the empty relation.

def tcSat (G : TCOrderedGraph) (h : 0 < G.1) (φ : TCFO) : Prop :=
  tcEval G (fun _ => ⟨0, h⟩) (tcBase G) φ

Uses 4 · Used by 1

Statement usesFormulas of first-order logic with transitive closure · Ordered graphs for first-order logic with transitive closure · Order and edge relations as FO + TC relation symbols · Evaluation of FO + TC formulas

Used byDefinability in FO + TC

DefinitionEncodings of a class of ordered graphs#✓fully proved

For a set \(K\) of ordered graphs, this is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of pairs of a natural number and a list of booleans, to some ordered graph \((n, T) \in K\) whose edge table \(T\) has length exactly \(n^2\).

noncomputable def tcEncodings (K : Set TCOrderedGraph) :
    MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x => decide (∃ G ∈ K,
    MetaMathlibExt.BitstringEncoding.bitDecode x = some G ∧ G.2.length = G.1 * G.1)

Uses 10 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Ordered graphs for first-order logic with transitive closure · Decision problems

Used byImmerman: FO + transitive closure is NL on ordered structures

DefinitionDefinability in FO + TC#✓fully proved

A set \(K\) of ordered graphs is FO + TC-definable when there are an FO + TC formula \(\varphi\) and a boolean \(b\) such that for every ordered graph \((n, T)\) whose edge table \(T\) has length exactly \(n^2\): if \(n > 0\), then \((n, T) \in K\) exactly when \((n, T)\) satisfies \(\varphi\), and if \(n = 0\), then \((n, T) \in K\) exactly when \(b\) is true.

def tcDefinable (K : Set TCOrderedGraph) : Prop :=
  ∃ φ, ∃ emptyIn : Bool, ∀ G : TCOrderedGraph, G.2.length = G.1 * G.1 →
    (G ∈ K ↔ (if h : 0 < G.1 then tcSat G h φ else emptyIn = true))

Uses 3 · Used by 1

Statement usesFormulas of first-order logic with transitive closure · Ordered graphs for first-order logic with transitive closure · Satisfaction of an FO + TC formula in an ordered graph

Used byImmerman: FO + transitive closure is NL on ordered structures

TheoremImmerman: FO + transitive closure is NL on ordered structures#●ready to prove

For every set \(K\) of finite ordered graphs, the decision problem of the encodings of \(K\) (the bitstrings that decode to a member \((n, T)\) of \(K\) whose edge table \(T\) has length exactly \(n^2\)) belongs to \(\mathrm{NL}\) if and only if \(K\) is definable in first-order logic with transitive closure.

public theorem_wanted fo_tc_eq_nl :
    ∀ K : Set TCOrderedGraph,
      (tcEncodings K ∈ NL ↔ tcDefinable K)

Sources

• N. Immerman, "Languages that capture complexity classes", SIAM Journal on Computing 16 (1987), 760-778 (STOC 1983).

Uses 6

Statement usesThe complexity class NL · Ordered graphs for first-order logic with transitive closure · Definability in FO + TC · Encodings of a class of ordered graphs · Complexity classes · Decision problems

10 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.