Documentation

DescriptiveComplexity.TransitiveClosureFO

First-order logic sits inside FO(TC), and inside FO(DTC) #

The trivial half of FO ⊆ FO(TC), needed to state the strict inclusion that DescriptiveComplexity.Problems.Even proves: a sentence is the walk that takes no step at all – arity 0, one mode, no transition, the sentence as the condition on starting nodes and nothing to check at the end. Reachability is then reflexivity, and acceptance is the sentence.

The same walk is deterministic, and for the cheapest of reasons: a walk with no step has no step with a competitor either, so nothing in the argument reads the transition formula and the proof of DescriptiveComplexity.accepts_det_sentenceSpec_iff is the proof of DescriptiveComplexity.accepts_sentenceSpec_iff again. That gives FO(≤) ⊆ FO(DTC) (DescriptiveComplexity.FODefinable.dtcDefinable), hence FO(≤) ⊆ L through DescriptiveComplexity.mem_LOGSPACE_iff – the end of the chain FO(≤) ⊊ AC⁰ ⊆ L ⊆ NL that would otherwise be left implicit, since the strict half of it (DescriptiveComplexity.exists_ac0Definable_not_foDefinable) says nothing about where FO(≤) itself sits.

The converse fails, unconditionally: EVEN is a walk and is not a sentence (DescriptiveComplexity.exists_tcDefinable_not_foDefinable).

source
noncomputable def DescriptiveComplexity.sentenceSpec {L : FirstOrder.Language} (φ : (L.sum FirstOrder.Language.order).Sentence) :
TCSpec L

The walk that takes no step: the sentence decides the starting node, and the node it starts at is already accepting.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.isSrc_sentenceSpec_iff {L : FirstOrder.Language} (φ : (L.sum FirstOrder.Language.order).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (u : (sentenceSpec φ).Node A) :
    (sentenceSpec φ).IsSrc u ↔ A ⊨ φ

    A node of the walk is a starting node exactly when the sentence holds: the tuple is empty, so there is nothing for the relabeling to carry.

    Dependency graph
    source
    theorem DescriptiveComplexity.accepts_sentenceSpec_iff {L : FirstOrder.Language} (φ : (L.sum FirstOrder.Language.order).Sentence) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty A] :
    (sentenceSpec φ).Accepts A ↔ A ⊨ φ
    Dependency graph
    source
    theorem DescriptiveComplexity.accepts_det_sentenceSpec_iff {L : FirstOrder.Language} (φ : (L.sum FirstOrder.Language.order).Sentence) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty A] :
    (sentenceSpec φ).det.Accepts A ↔ A ⊨ φ

    The deterministic reading of the same walk accepts on the same instances. The proof does not mention the transition formula at all – neither direction takes a step – which is precisely why determinization costs nothing here.

    Dependency graph
    source
    theorem DescriptiveComplexity.FODefinable.tcDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : FODefinable P) :
    TCDefinable P

    A first-order definable problem is FO(TC) definable: the walk that takes no step.

    Dependency graph
    source
    theorem DescriptiveComplexity.FODefinable.dtcDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : FODefinable P) :
    DTCDefinable P

    A first-order definable problem is FO(DTC) definable, hence in DescriptiveComplexity.LOGSPACE by DescriptiveComplexity.mem_LOGSPACE_iff: the walk that takes no step is deterministic for want of any step to compete.

    Dependency graph