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.
The hypothesis is not determinism but
DescriptiveComplexity.TMData.UniqueFrom: every configuration reachable from a
given one has at most one successor. That is what a program which guesses in
one phase and is deterministic after it has, and it is all the read-off lemmas
need – a reduction into a nondeterministic problem has to read its certificate
off an arbitrary accepting run, and this is what makes that a case analysis on
the guess rather than a second induction. Global determinism is the special case
(DescriptiveComplexity.TMData.uniqueFrom_of_deterministic).
Nothing here is about space: the statements hold for any TMData whose runs
are read with Relation.ReflTransGen.
Determinism where it is used: every configuration reachable from c has
at most one successor.
This is weaker than DescriptiveComplexity.TMData.Deterministic in exactly the
way a guessing program needs. A reduction into a nondeterministic problem has
to read its certificate off an arbitrary accepting run, and the way to survive
that is to guess in one phase and be deterministic everywhere after it: the
machine is then not deterministic at all, but it is unique from the
configuration the guess ends at, and every read-off below asks for no more.
Equations
- M.UniqueFrom c = ∀ (x y z : DescriptiveComplexity.Config A), Relation.ReflTransGen M.Step c x → M.Step x y → M.Step x z → y = z
Instances For
Dependency graph
A deterministic machine is unique from anywhere.
Dependency graph
Uniqueness from an invariant: a property the step relation preserves, and under which the step is functional, makes the machine unique from any configuration having it.
This is how a program that guesses in one phase pays for the rest of its run.
The property is “the phase is one the guess is not reachable from”; the step
preserves it because the program's phases only go forward, and at those phases
its rules separate. Global determinism is the case where the property is
True.
Dependency graph
Uniqueness travels forward along the run.
Dependency graph
A machine unique from c has one run out of c: two configurations
reachable from it are reachable from one another.
Dependency graph
A deterministic machine has one run: two configurations reachable from the same starting point are reachable from one another.
Dependency graph
Nothing is reachable from a stuck configuration but itself.
Dependency graph
A run into a dead end is not an accepting one, at a machine unique from where the run starts. This is the form a guessing program uses: the guess phase is the only nondeterministic one, so what has to be ruled out is an accepting run of the same guess, and that is a statement about one deterministic remainder.
DescriptiveComplexity.TMData.not_acceptsSpace_of_reaches_dead is this with the
uniqueness supplied by global determinism and the initial configuration matched
up.
Dependency graph
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.
Dependency graph
A machine that never halts #
The other way a no-instance is discharged, and the one a machine with no clock
needs: instead of one run that ends badly, an unbounded chain of runs that
never ends. A halted configuration is reached in a fixed number of steps, so a
chain whose n-th link costs at least n of them reaches none.
Reachability is a run of some length.
Dependency graph
A nonempty reachability is a run of positive length.
Dependency graph
A stuck configuration is reached in one number of steps: the shorter run is a prefix of the longer one, and nothing leaves a dead end.
Dependency graph
A deterministic machine whose run passes an unbounded chain does not
accept. Each link of the chain costs at least one step, so the n-th is
reached in at least n; an accepting configuration is stuck, hence reached in
one fixed number of steps, and lies beyond every link. This is what makes a
diverging computation a correct rejection with no clock anywhere.
Dependency graph
The positive half, for symmetry: a run from the initial configuration to an accepting one is exactly what acceptance in bounded space asks for.