Encodings of finite binary machine configurations

The encoding stores the input, control, unary input position, work tapes, output and every query and answer buffer. Its length bound charges replies separately from the machine clock: a short oracle run may receive a long word.

Main definitions

• Turing.MultiTapeTM.encFiniteCfg: encode ordinary finite binary storage.
• Turing.MultiTapeTM.encChannels: encode the query buffer and answer tape of every channel.
• Turing.MultiTapeTM.encFiniteConfig: include the fixed family of oracle channels.

Main results

• Turing.MultiTapeTM.length_encFiniteConfig_le: linear encoded storage under SpaceBound.

References

Adapts Computability/Probabilistic/Configuration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the existing finite configuration and encodings.

noncomputable def Turing.MultiTapeTM.encFiniteCfg {k : ℕ} {State : Type} [Finite State] : FiniteCfg k Bool State ↪ List Bool

Store the input, control, unary input position, complete work tapes and accumulated output.

@[simp]

theorem Turing.MultiTapeTM.encFiniteCfg_apply {k : ℕ} {State : Type} [Finite State] (cfg : FiniteCfg k Bool State) : encFiniteCfg cfg = (encPair encBits (encPair (encFinite (Option State)) (encPair encUnary (encPair (encPi (encBiTape encBool)) encBits)))) (cfg.input, cfg.state, ↑cfg.inputPos, cfg.workTapes, cfg.output)

@[reducible, inline]

noncomputable abbrev Turing.MultiTapeTM.encChannels {Oracle : Type} [Fintype Oracle] : (Oracle → List Bool × Cslib.Turing.BiTape Bool) ↪ List Bool

The oracle channels of a configuration, as a table in Fintype.equivFin order of the oracles. Each entry is a pair: the framed pending request word, then the complete answer tape.

noncomputable def Turing.MultiTapeTM.encFiniteConfig {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : MultiTapeMachine.FiniteConfig k Bool State Oracle ↪ List Bool

Store the ordinary finite configuration and all pending requests and answer tapes.

@[simp]

theorem Turing.MultiTapeTM.encFiniteConfig_apply {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] (cfg : MultiTapeMachine.FiniteConfig k Bool State Oracle) : encFiniteConfig cfg = (encPair encFiniteCfg (encPi (encPair encBits (encBiTape encBool)))) (cfg.tapes, cfg.channels)

theorem Turing.MultiTapeTM.length_encFiniteConfig_le {k : ℕ} {State : Type} [Finite State] {Oracle : Type} [Fintype Oracle] : ∃ (c : ℕ), ∀ (inputSize steps answerSize : ℕ) (cfg : MultiTapeMachine.FiniteConfig k Bool State Oracle), MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps answerSize cfg → (encFiniteConfig cfg).length ≤ c * (inputSize + steps + answerSize + 1)

The whole encoding is linear in input length, elapsed steps and the largest installed reply. The constant depends only on the fixed control, channel type and number of work tapes.