Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Sampling

A uniform word sampler #

One fixed machine with one control state and no work tapes scans its input, emitting a fresh fair bit per symbol and halting at the right boundary. On an input of length n it writes a uniform word of length n in exactly n + 1 transitions. The last transition samples and discards a coin, as the common interpreter does on every live instruction; the results below concern closed distributions, not equality of programs with different numbers of coin queries.

Main definitions #

Main results #

References #

Adapted from Cslib/Computability/Probabilistic/Sampling.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine and input length.

source
def Turing.MultiTapePTM.uniformListMachine :
MultiTapePTM 0 Bool Unit

Emit one fair bit per input symbol, then halt without using work tapes.

Instances For
    source
    def Turing.MultiTapePTM.UniformListMachine.config (input : List Bool) (state : Option Unit) (index : ℕ) (output : List Bool) (h : index ≤ input.length) :
    MultiTapeMachine.Config 0 Bool Unit Empty input

    The scanner at an input position, with the output written so far.

    Instances For
      source
      theorem Turing.MultiTapePTM.UniformListMachine.step {input output : List Bool} {index : ℕ} (h : index < input.length) (bit : Bool) :
      (config input (some ()) index output ⋯).step { inputTape := 1, workTapes := Fin.elim0, output := some bit, state := some () } Empty.elim Empty.elim = config input (some ()) (index + 1) (output ++ [bit]) h

      Reading any remaining symbol writes the sampled bit and advances once.

      source
      theorem Turing.MultiTapePTM.UniformListMachine.eval_run_config (input : List Bool) (remaining index : ℕ) (output : List Bool) (h : index + remaining = input.length) :
      (uniformListMachine.runClosedConfigFrom (remaining + 1) (config input (some ()) index output ⋯)).eval = PMF.map (fun (tail : List Bool) => config input none input.length (output ++ tail) ⋯) (Cslib.BitString.uniformList remaining)

      The complete configuration distribution after scanning the remaining suffix and halting.

      source
      theorem Turing.MultiTapePTM.eval_runClosedConfig_uniformListMachine (input : List Bool) :
      (uniformListMachine.runClosedConfigFrom (input.length + 1) (MultiTapeMachine.initialConfig uniformListMachine input)).eval = PMF.map (fun (output : List Bool) => UniformListMachine.config input none input.length output ⋯) (Cslib.BitString.uniformList input.length)

      The final configuration retains the generated word and has halted at the right boundary.

      source
      theorem Turing.MultiTapePTM.eval_uniformListMachine (input : List Bool) :
      (uniformListMachine.runClosed (input.length + 1) input).eval = Cslib.BitString.uniformList input.length

      The scanner outputs a uniform word of the input length in a linear number of transitions.

      source
      theorem Turing.MultiTapePTM.uniformListMachine_halted (input : List Bool) (final : MultiTapeMachine.Config 0 Bool Unit Empty input) :
      final ∈ (uniformListMachine.runClosedConfigFrom (input.length + 1) (MultiTapeMachine.initialConfig uniformListMachine input)).eval.support → final.tapes.state = none

      Every supported configuration has actually halted by the linear clock.