Documentation

Complexity.Computability.Machines.Turing.MultiTape.Machine.Halting

Halting bounds for effectful machines #

A halting bound concerns the control state of every supported run, rather than merely its externally stopped output. Once the machine has halted, extra fuel preserves the whole joint distribution of machine configuration and interpreter state.

The choice and query programs are explicit parameters, as in runConfigFrom. HaltsWithin quantifies over every stateful interpretation of those programs; it does not assert efficiency of either handler.

Main definitions #

Main results #

References #

Adapted from MultiTape/Oracle/Halting.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common machine and typed program interface.

source
def Turing.MultiTapeMachine.HaltsWithin {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (input : List Symbol) :
Prop

Every supported execution halts within fuel, against every stateful interpreter.

Instances For
    source
    theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_add_of_halted {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {OracleState : Type} {input : List Symbol} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (cfg : Config k Symbol State Oracle input) (fuel padding : ℕ) (s : OracleState) (hhalt : ∀ result ∈ ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg)).run s).support, result.1.tapes.state = none) :
    (Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query (fuel + padding) cfg)).run s = (Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg)).run s

    Once every supported execution has halted, extra time preserves the complete distribution.

    source
    theorem Turing.MultiTapeMachine.interpret_runConfigFrom_add_of_halted_list {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {input : List Symbol} (oracle : (q : Query) → List (spec q)) (cfg : Config k Symbol State Oracle input) (fuel padding : ℕ) (hhalt : ∀ final ∈ Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg), final.tapes.state = none) :
    Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query (fuel + padding) cfg) = Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg)

    Enumerating finite responses preserves every endpoint occurrence after halting. Unlike a probability interpretation, a List interpreter may have no outcomes; this equality does not itself assert that the machine cannot get stuck.

    source
    theorem Turing.MultiTapeMachine.HaltsWithin.run_interpret_runConfigFrom_eq {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] {machine : MultiTapeMachine k Symbol State Oracle Choose} {choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)} {query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)} {fuel : ℕ} {input : List Symbol} (h : machine.HaltsWithin choose query fuel input) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (larger : ℕ) (s : OracleState) (hle : fuel ≤ larger) :
    (Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query larger (machine.initialConfig input))).run s = (Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel (machine.initialConfig input))).run s

    Any larger clock gives the same joint distribution once a halting bound is known.

    source
    theorem Turing.MultiTapeMachine.HaltsWithin.mono {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] {machine : MultiTapeMachine k Symbol State Oracle Choose} {choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)} {query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)} {fuel larger : ℕ} {input : List Symbol} (h : machine.HaltsWithin choose query fuel input) (hle : fuel ≤ larger) :
    machine.HaltsWithin choose query larger input

    A halting bound remains valid when increased.

    source
    theorem Turing.MultiTapeMachine.HaltsWithin.run_interpret_run_eq {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] {machine : MultiTapeMachine k Symbol State Oracle Choose} {choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)} {query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)} {fuel : ℕ} {input : List Symbol} (h : machine.HaltsWithin choose query fuel input) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (larger : ℕ) (s : OracleState) (hle : fuel ≤ larger) :
    (Cslib.OracleComp.interpret oracle (machine.run choose query larger input)).run s = (Cslib.OracleComp.interpret oracle (machine.run choose query fuel input)).run s

    Padding a halting run also preserves its output and the final private state.