LOGSPACE, by deterministic transitive closure

The class LOGSPACE: the problems definable in FO(DTC) (DescriptiveComplexity.DTCDefinable), first-order logic with a deterministic transitive-closure operator, which captures deterministic logarithmic space on ordered structures (Immerman 1987). As everywhere in this library the capture theorem is the definition: the class is what the logic defines, no machine model is involved, and no axiom is added.

It is called LOGSPACE rather than L because L is the name this development gives to a first-order vocabulary in almost every file.

Why an operator, and not a fragment of ∃SO

DescriptiveComplexity.PTIME is defined by the Horn fragment and DescriptiveComplexity.NL by the Krom fragment of existential second-order logic (Grädel 1992). There is no comparable syntactic fragment known for deterministic logarithmic space, so this class breaks the pattern: it is the first one here defined by an operator-as-data logic (DescriptiveComplexity.TCSpec read through DescriptiveComplexity.TCSpec.det) rather than by the shape of a kernel. That it is nonetheless a bona fide DescriptiveComplexity.ComplexityClass is the content of DescriptiveComplexity.TransitiveClosurePull: FO(DTC) definability is closed under (ordered) first-order reductions, the walk on the interpreted structure being a walk on the base structure with the tags carried in the mode.

Where it sits

L ⊆ NL (DescriptiveComplexity.LOGSPACE_subset_NL) is immediate at the level of definability – a determinized specification is a specification – followed by the FO(TC)/SO-Krom translation of DescriptiveComplexity.ImmermanSzelepcsenyi. DescriptiveComplexity.LOGSPACE_subset_PTIME and DescriptiveComplexity.LOGSPACE_subset_NP compose that with the inclusions of NL (proved downstream, with 2SAT).

The canonical complete problem is REACHd, deterministic reachability, in DescriptiveComplexity.Problems.ReachabilityDet; its complement UNREACHd is complete too, and with it the class is closed under complement (DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE, in DescriptiveComplexity.Problems.ReachabilityDet.Complement) – with no analogue of Immerman–Szelepcsényi needed, a deterministic walk being witnessed not to arrive by a step budget.

What is not claimed, here as for the other classes: nothing relates this class to a machine model. L ≠ NL and L = NL are both consistent with everything proved here, and the containment FO(DTC) ⊆ L on the machine side – the half of Immerman's theorem this definition replaces – is not formalized.

noncomputable def DescriptiveComplexity.LOGSPACE : ComplexityClass

The class LOGSPACE: the problems definable in FO(DTC), first-order logic with a deterministic transitive closure, which captures deterministic logarithmic space on ordered structures (Immerman 1987).

Hardness is stated cofinally, exactly as for the other classes of this library (DescriptiveComplexity.CofinalHard); over a relational vocabulary it is the usual notion, DescriptiveComplexity.hard_LOGSPACE_iff.

Equations

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

theorem DescriptiveComplexity.mem_LOGSPACE_iff {L : FirstOrder.Language} (P : DecisionProblem L) : LOGSPACE.Mem P ↔ DTCDefinable P

Membership in LOGSPACE is exactly FO(DTC) definability, by definition.

theorem DescriptiveComplexity.hard_LOGSPACE_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : LOGSPACE.Hard P ↔ ∀ {L'' : FirstOrder.Language} (Q : DecisionProblem L''), DTCDefinable Q → Nonempty (RelOrderedFOReduction Q P)

Over a relational vocabulary, LOGSPACE-hardness is the usual notion: every FO(DTC) definable problem reduces to P.

theorem DescriptiveComplexity.LOGSPACE_subset_NL : LOGSPACE ⊆ NL

L ⊆ NL: a deterministic walk is a walk, and FO(TC) definability is membership in NL (DescriptiveComplexity.tcDefinable_iff_mem_NL, the two translations through the Krom fragment).