Documentation

Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed

Configuration laws for closed fair-coin programs #

Closed machines have no oracle channels and draw fresh fair bits through ProbComp.uniform Bool. These specializations of the common machine laws let probabilistic realizations work directly with configuration distributions. Actual halting is required when padding or sequencing clocks.

Main definitions #

Main results #

References #

Specializations of the common halting, sequencing and deterministic embedding rules, adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

source
noncomputable def Turing.MultiTapePTM.runClosedConfigFrom {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
Cslib.ProbComp (MultiTapeMachine.Config k Symbol State Empty input)

Retain the complete configuration of a closed run with fresh fair coins.

Instances For
    source
    theorem Turing.MultiTapePTM.runClosed_eq_map {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input : List Symbol) :
    machine.runClosed fuel input = (fun (final : MultiTapeMachine.Config k Symbol State Empty input) => final.tapes.output) <$> machine.runClosedConfigFrom fuel (MultiTapeMachine.initialConfig machine input)

    The closed output is the projection of the final configuration program.

    source
    theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_add_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (cfg : MultiTapeMachine.Config k Symbol State Empty input) (fuel padding : ℕ) (hhalt : ∀ final ∈ (machine.runClosedConfigFrom fuel cfg).eval.support, final.tapes.state = none) :
    (machine.runClosedConfigFrom (fuel + padding) cfg).eval = (machine.runClosedConfigFrom fuel cfg).eval

    Padding a halting run preserves the complete configuration distribution.

    source
    theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_eq_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (cfg : MultiTapeMachine.Config k Symbol State Empty input) {fuel larger : ℕ} (hle : fuel ≤ larger) (hhalt : ∀ final ∈ (machine.runClosedConfigFrom fuel cfg).eval.support, final.tapes.state = none) :
    (machine.runClosedConfigFrom larger cfg).eval = (machine.runClosedConfigFrom fuel cfg).eval

    Any larger clock gives the same configuration distribution after a halting bound.

    source
    theorem Turing.MultiTapePTM.eval_runClosed_eq_of_halted {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (input : List Symbol) {fuel larger : ℕ} (hle : fuel ≤ larger) (hhalt : ∀ final ∈ (machine.runClosedConfigFrom fuel (MultiTapeMachine.initialConfig machine input)).eval.support, final.tapes.state = none) :
    (machine.runClosed larger input).eval = (machine.runClosed fuel input).eval

    Padding a halting bound preserves the closed output distribution.

    source
    theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_seq {k : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (first : MultiTapePTM k Symbol State₀) (second : MultiTapePTM k Symbol State₁) (cfg : MultiTapeMachine.Config k Symbol State₀ Empty input) (firstTime secondTime : ℕ) (hfirst : ∀ result ∈ (first.runClosedConfigFrom firstTime cfg).eval.support, result.tapes.state = none) (hsecond : ∀ result ∈ (first.runClosedConfigFrom firstTime cfg).eval.support, ∀ final ∈ (second.runClosedConfigFrom secondTime (MultiTapeMachine.Sequential.start second result)).eval.support, final.tapes.state = none) :
    ((first.seq second).runClosedConfigFrom (firstTime + secondTime) (MultiTapeMachine.Sequential.left second cfg)).eval = do let result ← (first.runClosedConfigFrom firstTime cfg).eval PMF.map MultiTapeMachine.Sequential.right (second.runClosedConfigFrom secondTime (MultiTapeMachine.Sequential.start second result)).eval

    Shared-tape sequencing preserves distributions once both phases have actually halted.

    source
    theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeTM k Symbol State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Empty input) :
    ((ofDeterministic machine).runClosedConfigFrom fuel cfg).eval = PMF.pure { tapes := MultiTapeTM.runFrom cfg.tapes fuel, channels := cfg.channels }

    A deterministic embedding has a point-mass configuration distribution.