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 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), which 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} [L.IsRelational] (P : DecisionProblem L) : LOGSPACE.Mem P ↔ DTCDefinable P

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

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). Registered in the Lax archive as Lax485149.LSubsetNL.LOGSPACE_subset_NL.