Documentation

Complexity.Computability.Machines.Turing.MultiTape.Encodings.Configuration

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 #

Main results #

References #

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

source
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.

Instances For
    source
    @[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)
    source
    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.

    Instances For
      source
      @[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)
      source
      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.