Polynomial-time finite configuration operations

Ordinary and oracle structure construction, observations, fixed native actions, channel replies and initialization are certified in plain polynomial time (Turing.MultiTapeTM.ComputableInPolyTime), by composition of pair, list, table and tape rules. Copying the input, work tapes, accumulated output and every channel is charged by their encodings. Tidy forms of the observations and oracle transitions, derived from the plain rules, remain for the tidy proofs that still use them.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_state, .finiteCfg_inputSymbol, .finiteCfg_workTapeSymbols, .finiteCfg_output: plain observations.
• Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_step: execute a fixed native action.
• Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_init: initialize finite storage.
• Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_mk, .finiteConfig_tapes, .finiteConfig_channels, .finiteConfig_answerSymbols: assemble and observe oracle storage.
• Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_step, .finiteConfig_receive: local transitions and channel reset with a computed reply.
• Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_init: initialize oracle storage.

References

Adapts Computability/Probabilistic/Configuration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to plain polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_mk {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {word : α → List Bool} {state : α → Option State} {position : (a : α) → Fin ((word a).length + 2)} {work : α → Fin k → Cslib.Turing.BiTape Bool} {output : α → List Bool} (hword : ComputableInPolyTime word input encBits) (hstate : ComputableInPolyTime state input (encFinite (Option State))) (hposition : ComputableInPolyTime (fun (a : α) => ↑(position a)) input encUnary) (hwork : ComputableInPolyTime work input (encPi (encBiTape encBool))) (houtput : ComputableInPolyTime output input encBits) : ComputableInPolyTime (fun (a : α) => { input := word a, state := state a, inputPos := position a, workTapes := work a, output := output a }) input encFiniteCfg

Assemble an ordinary configuration from its certified components.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_input {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.input encFiniteCfg encBits

Read the stored input word.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_state {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.state encFiniteCfg (encFinite (Option State))

Read the finite control.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_inputPos {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime (fun (cfg : FiniteCfg k Bool State) => ↑cfg.inputPos) encFiniteCfg encUnary

Read the input head's unary position.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_workTapes {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.workTapes encFiniteCfg (encPi (encBiTape encBool))

Read the complete family of work tapes.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_output {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.output encFiniteCfg encBits

Read all accumulated output.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_inputSymbol {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.inputSymbol encFiniteCfg (encFinEnum (Option Bool))

Observe the read-only input, including both blank boundary cells.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_workTapeSymbols {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime FiniteCfg.workTapeSymbols encFiniteCfg (encFinEnum (Fin k → Option Bool))

Observe all work heads as a single fixed finite value.

theorem Turing.MultiTapeTM.ComputableInPolyTime.moveInputPos {α : Type} {input : α ↪ List Bool} {word : α → List Bool} {position : (a : α) → Fin ((word a).length + 2)} (hword : ComputableInPolyTime word input encBits) (hposition : ComputableInPolyTime (fun (a : α) => ↑(position a)) input encUnary) (move : SignType) : ComputableInPolyTime (fun (a : α) => ↑(Turing.moveInputPos (position a) move)) input encUnary

Clamped native input-head movement is efficient on the stored unary position.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_step {k : ℕ} {State : Type} [Finite State] (action : Action k Bool State) : ComputableInPolyTime (fun (cfg : FiniteCfg k Bool State) => cfg.step action) encFiniteCfg encFiniteCfg

Execute a fixed ordinary native action, including all retained storage.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_init {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {word : α → List Bool} (hword : ComputableInPolyTime word input encBits) (state : State) : ComputableInPolyTime (fun (a : α) => FiniteCfg.init state (word a)) input encFiniteCfg

Initialize with the native input-head convention and blank work tapes.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_mk {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {Oracle : Type} [Fintype Oracle] {tapes : α → FiniteCfg k Bool State} {channels : α → Oracle → List Bool × Cslib.Turing.BiTape Bool} (htapes : ComputableInPolyTime tapes input encFiniteCfg) (hchannels : ComputableInPolyTime channels input encChannels) : ComputableInPolyTime (fun (a : α) => { tapes := tapes a, channels := channels a }) input encFiniteConfig

Assemble ordinary storage and its family of oracle channels.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_tapes {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableInPolyTime MultiTapeMachine.FiniteConfig.tapes encFiniteConfig encFiniteCfg

Read the ordinary finite storage.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_channels {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableInPolyTime MultiTapeMachine.FiniteConfig.channels encFiniteConfig encChannels

Read all query buffers and answer tapes.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_answerSymbols {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableInPolyTime MultiTapeMachine.FiniteConfig.answerSymbols encFiniteConfig (encFinite (Oracle → Option Bool))

Observe every answer head as a single fixed finite value.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_step {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] (action : Action k Bool State) (symbol : Oracle → Option Bool) (move : Oracle → SignType) : ComputableInPolyTime (fun (cfg : MultiTapeMachine.FiniteConfig k Bool State Oracle) => cfg.step action symbol move) encFiniteConfig encFiniteConfig

Execute a fixed local action, including all pending requests and stored answers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_receive {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {Oracle : Type} [Fintype Oracle] [DecidableEq Oracle] {cfg : α → MultiTapeMachine.FiniteConfig k Bool State Oracle} {answer : α → List Bool} (hcfg : ComputableInPolyTime cfg input encFiniteConfig) (hanswer : ComputableInPolyTime answer input encBits) (channel : Oracle) (next : State) : ComputableInPolyTime (fun (a : α) => (cfg a).receive channel next (answer a)) input encFiniteConfig

Install a computed reply, clear its selected request and retain all other channels.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finiteConfig_init {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {Oracle : Type} [Fintype Oracle] {word : α → List Bool} (hword : ComputableInPolyTime word input encBits) (state : State) : ComputableInPolyTime (fun (a : α) => MultiTapeMachine.FiniteConfig.init state (word a)) input encFiniteConfig

Initialize every channel with an empty request and blank answer tape.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_state {k : ℕ} {State : Type} [Finite State] : ComputableTidilyInPolyTime FiniteCfg.state encFiniteCfg (encFinite (Option State))

Read the finite control.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_output {k : ℕ} {State : Type} [Finite State] : ComputableTidilyInPolyTime FiniteCfg.output encFiniteCfg encBits

Read all accumulated output.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_inputSymbol {k : ℕ} {State : Type} [Finite State] : ComputableTidilyInPolyTime FiniteCfg.inputSymbol encFiniteCfg (encFinEnum (Option Bool))

Observe the read-only input, including both blank boundary cells.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols {k : ℕ} {State : Type} [Finite State] : ComputableTidilyInPolyTime FiniteCfg.workTapeSymbols encFiniteCfg (encFinEnum (Fin k → Option Bool))

Observe all work heads as a single fixed finite value.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_tapes {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableTidilyInPolyTime MultiTapeMachine.FiniteConfig.tapes encFiniteConfig encFiniteCfg

Read the ordinary finite storage.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_channels {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableTidilyInPolyTime MultiTapeMachine.FiniteConfig.channels encFiniteConfig encChannels

Read all query buffers and answer tapes.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_answerSymbols {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ComputableTidilyInPolyTime MultiTapeMachine.FiniteConfig.answerSymbols encFiniteConfig (encFinite (Oracle → Option Bool))

Observe every answer head as a single fixed finite value.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_step {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] (action : Action k Bool State) (symbol : Oracle → Option Bool) (move : Oracle → SignType) : ComputableTidilyInPolyTime (fun (cfg : MultiTapeMachine.FiniteConfig k Bool State Oracle) => cfg.step action symbol move) encFiniteConfig encFiniteConfig

Execute a fixed local action, including all pending requests and stored answers.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_receive {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {Oracle : Type} [Fintype Oracle] [DecidableEq Oracle] {cfg : α → MultiTapeMachine.FiniteConfig k Bool State Oracle} {answer : α → List Bool} (hcfg : ComputableTidilyInPolyTime cfg input encFiniteConfig) (hanswer : ComputableTidilyInPolyTime answer input encBits) (channel : Oracle) (next : State) : ComputableTidilyInPolyTime (fun (a : α) => (cfg a).receive channel next (answer a)) input encFiniteConfig

Install a computed reply, clear its selected request and retain all other channels.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_init {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} {Oracle : Type} [Fintype Oracle] {word : α → List Bool} (hword : ComputableTidilyInPolyTime word input encBits) (state : State) : ComputableTidilyInPolyTime (fun (a : α) => MultiTapeMachine.FiniteConfig.init state (word a)) input encFiniteConfig

Initialize every channel with an empty request and blank answer tape.