Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Callbacks

Native callbacks for the complete counting query machine #

The callbacks receive only the encoded runtime state, current input symbol and choice bit as needed. Their workspace is linear in these short arguments, including on malformed states. The radix is stored in binary, so the graph routines receive it as an argument; the next radix is four times the current one.

Main results #

References #

source
theorem Turing.InductiveCounting.query_inSpace {k : ℕ} :
MultiTapeTM.ComputableInSpace (runtimeQuery k) encRuntime MultiTapeTM.encNat fun (s : Runtime) => (encRuntime s).length

Native linear workspace for the full runtime input-address callback.

source
theorem Turing.InductiveCounting.next_inSpace {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) :
MultiTapeTM.ComputableInSpace (fun (p : Runtime × Option Bool × Bool) => runtimeNext ntm p.1 p.2.1 p.2.2) (MultiTapeTM.encPair encRuntime (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) encRuntime fun (p : Runtime × Option Bool × Bool) => ((MultiTapeTM.encPair encRuntime (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) p).length

Native linear workspace for the full next-state callback on its exact input tuple.

source
theorem Turing.InductiveCounting.halted_inSpace :
MultiTapeTM.ComputableInSpace runtimeHalted encRuntime MultiTapeTM.encBool fun (s : Runtime) => (encRuntime s).length

Native linear workspace for full runtime halt detection.

source
theorem Turing.InductiveCounting.accept_inSpace :
MultiTapeTM.ComputableInSpace runtimeAccept encRuntime MultiTapeTM.encBool fun (s : Runtime) => (encRuntime s).length

Native linear workspace for full runtime acceptance detection.