Runs of a deterministic machine, unbounded in time

The tool that makes the converse half of a space-bounded hardness proof free.

A reduction into DescriptiveComplexity.DTMAcceptSpace has to show both that a yes-instance is accepted and that a no-instance is not. The second half is usually a second induction – an invariant strong enough to rule out every run. For a deterministic machine it is not needed: the configurations reachable from one starting point are linearly ordered by reachability (DescriptiveComplexity.TMData.reach_total, from Mathlib's Relation.ReflTransGen.total_of_right_unique and DescriptiveComplexity.TMData.step_functional), so it is enough to exhibit one run, of the machine's own choosing, that ends badly.

Concretely, DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead says: if the initial configuration reaches a configuration that is stuck and not accepting, and if accepting configurations are themselves stuck, then the machine does not accept. Both side conditions are properties of the transition table, so a reduction discharges them by inspection of its own program.

Nothing here is about space: the statements hold for any TMData whose runs are read with Relation.ReflTransGen.

theorem DescriptiveComplexity.TMData.reflTransGen_of_stepsIn {A : Type} {M : TMData A} {n : ℕ} {c d : Config A} : M.StepsIn n c d → Relation.ReflTransGen M.Step c d

A budgeted run is a run: the space-bounded reading of acceptance forgets the step count, so every lemma stated with DescriptiveComplexity.TMData.StepsIn – the sweep primitives of DescriptiveComplexity.Problems.Machine.Program, in particular – feeds straight into it.

theorem DescriptiveComplexity.TMData.reach_total {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) (hdet : M.Deterministic) {c x y : Config A} (hx : Relation.ReflTransGen M.Step c x) (hy : Relation.ReflTransGen M.Step c y) : Relation.ReflTransGen M.Step x y ∨ Relation.ReflTransGen M.Step y x

A deterministic machine has one run: two configurations reachable from the same starting point are reachable from one another.

theorem DescriptiveComplexity.TMData.eq_of_reach_stuck {A : Type} {M : TMData A} {c d : Config A} (hstuck : ∀ (e : Config A), ¬M.Step c e) (h : Relation.ReflTransGen M.Step c d) : c = d

Nothing is reachable from a stuck configuration but itself.

theorem DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead {A : Type} {M : TMData A} (hwf : M.WellFormed) (hdet : M.Deterministic) {c₀ d : Config A} (hinit : M.IsInit c₀) (hreach : Relation.ReflTransGen M.Step c₀ d) (hdead : ∀ (e : Config A), ¬M.Step d e) (hnacc : ¬M.Acc d.state) (hsink : ∀ (e : Config A), M.Acc e.state → ∀ (e' : Config A), ¬M.Step e e') : ¬M.AcceptsSpace

A deterministic machine that runs into a dead end does not accept.

The run exhibited by hreach is the run, so an accepting configuration would have to lie on it – before the dead end, and then it would have to be the dead end itself since an accepting configuration is stuck, or after it, and then it would be the dead end because nothing follows a dead end. Either way the dead end is accepting, which it is not.

theorem DescriptiveComplexity.TMData.acceptsSpace_of_reaches_acc {A : Type} {M : TMData A} {c₀ d : Config A} (hinit : M.IsInit c₀) (hreach : Relation.ReflTransGen M.Step c₀ d) (hacc : M.Acc d.state) : M.AcceptsSpace

The positive half, for symmetry: a run from the initial configuration to an accepting one is exactly what acceptance in bounded space asks for.