Documentation

Complexity.Computability.Machines.Turing.MultiTape.Machine.OutputPrefix

Retaining an existing output prefix #

A machine cannot read its output. Prepending a word to that output therefore preserves its entire execution program, including stateful choices and oracle interactions. This is a configuration invariance law; writing the prefix remains separate, charged machine work.

Main definitions #

Main results #

References #

Adapted from Computability/Machines/Turing/MultiTape/Oracle/OutputPrefix.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using upstream's configuration operation and the common one-step program simulation rule.

source
def Turing.MultiTapeMachine.Config.prependOutput {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
Config k Symbol State Oracle input

Change only the unreadable output, retaining all communication channels.

Instances For
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_state {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).tapes.state = cfg.tapes.state
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_inputSymbol {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).tapes.inputSymbol = cfg.tapes.inputSymbol
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_workTapeSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).tapes.workTapeSymbols = cfg.tapes.workTapeSymbols
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_channels {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).channels = cfg.channels
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_answerSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).answerSymbols = cfg.answerSymbols
    source
    @[simp]
    theorem Turing.MultiTapeMachine.Config.prependOutput_output {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    (cfg.prependOutput pre).tapes.output = pre ++ cfg.tapes.output
    source
    theorem Turing.MultiTapeMachine.Config.step_prependOutput {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (pre : List Symbol) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) :
    (cfg.prependOutput pre).step action symbol move = (cfg.step action symbol move).prependOutput pre
    source
    theorem Turing.MultiTapeMachine.Config.receive_prependOutput {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} [DecidableEq Oracle] (cfg : Config k Symbol State Oracle input) (pre : List Symbol) (oracle : Oracle) (next : State) (answer : List Symbol) :
    (cfg.prependOutput pre).receive oracle next answer = (cfg.receive oracle next answer).prependOutput pre
    source
    theorem Turing.MultiTapeMachine.runConfigFrom_prependOutput {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [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 : ℕ) (cfg : Config k Symbol State Oracle input) (pre : List Symbol) :
    machine.runConfigFrom choose query fuel (cfg.prependOutput pre) = (fun (final : Config k Symbol State Oracle input) => final.prependOutput pre) <$> machine.runConfigFrom choose query fuel cfg

    An existing output prefix is retained without affecting any instructions or interactions.