How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Nondeterministic acceptance time and exact clocks
Definition
For a fixed finitely branching nondeterministic multitape machine , let be the minimum length of an accepting branch, or if there is none. The minimum of a nonempty set of natural lengths exists by searching lengths in increasing order. This extends the existential acceptance convention in Accepting computations of a nondeterministic machine to the finite-valued multitape transition map in The classes DTIME, NTIME, DSPACE, and NSPACE. Nonaccepting branches may diverge. For a finite integer , acceptance within means . For , put . The acceptance-time class for consists of languages with on their accepted inputs, uniformly in the input and with fixed machine-dependent constants.
This differs at the machine level from the maximum-branch convention in Worst-case time and space complexity of a machine. The library class NTIME uses all-branch halting as in The classes DTIME, NTIME, DSPACE, and NSPACE. Big-O and little-o have the zero-safe and finite-exception meanings in Uniform asymptotic time space comparison.
An exact clock for here is a deterministic fixed multitape machine that halts after exactly transitions on every binary input of length . Its initial state is nonhalting, so . We do not require monotonicity. The exact-clock clause of Machine time and space constructibility motivates the terminology but its separate nondecreasing guard is not imported into this local definition; a unary-only clock can be run after copying a binary input to unary, paying preprocessing time. No equivalence with an output constructor is asserted.
For an acceptor and such a clock, copy the input for to one tape set and simultaneously write one binary per input symbol to the clock's input tape, producing even when has a nonbinary input alphabet. Then perform one simulated transition of each machine per round. Check acceptance at the initial instant and after each N-transition, including the last allowed one; after the clock's th transition reject if no acceptance has occurred. Missing transition options count as rejecting branches. This recognizes exactly : an accepting branch of length at most T survives, and every surviving acceptance came from such a branch. Every branch terminates in real transitions. Temporary stay-put bookkeeping is implementable in the L/R-only model by a two-move excursion right and left, returning to the same cell even at zero, with intermediate states not halting.
To retain a bound rather than just , run C clock copies sequentially while continuing N for one step per simulated clock transition; for a fixed integer C this is still . Resets or prebuilt copies cost the same order. If an acceptor recognizes a language within and , choose C covering the tail bound and the finitely many accepting exceptions (T is positive there). This yields an all-branch machine for the same language in NTIME(T). There is no such conversion asserted for arbitrary unclocked recursive b.
Depends on
Used by
- Shortest acceptance versus clocked all-branch halting Example
- Clocks, cutoffs, and finite unions preserve nondeterministic time bounds Lemma
- Linear acceptance-time simulation on two tapes Lemma
- No recursive bound covers all recursive unary languages Lemma
- Nondeterministic recursive-padding separation Theorem
Dependency tree · two levels
13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Seiferas, Fischer, and Meyer, pp. 147-148 (standard reference, not scraped)