Fair-coin multi-tape machines

MultiTapePTM specializes the common table to one action per Boolean coin value. Its run is the common interpreter with a handler that samples a bit and selects the corresponding action. Even equal branches consume a bit; halted configurations consume no more bits.

The open run accepts a typed program supplying coins and a program answering each named oracle call. This separates the syntax from the interpretation: fair-coin semantics requires interpreting the coin program as an independent uniform bit. runClosed fixes this interpretation through ProbComp.uniform Bool for machines without oracle channels. No efficiency assertion about an arbitrary coin program or oracle handler is made here.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

Main definitions

• Turing.MultiTapePTM: the Boolean-indexed specialization of the common machine.
• Turing.MultiTapePTM.runConfigFrom: the run program with explicit coin and query programs.
• Turing.MultiTapePTM.runClosed: a closed fair-coin run using the finite-uniform interface.

@[reducible, inline]

abbrev Turing.MultiTapePTM (k : ℕ) (Symbol State : Type) (Oracle : Type := Empty) : Type

A machine with one transition per Boolean coin; by default it has no oracle channels.

def Turing.MultiTapePTM.runConfigFrom {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) : Cslib.OracleComp spec (MultiTapeMachine.Config k Symbol State Oracle input)

Run with the supplied coin program, retaining the whole configuration at clock exhaustion.

def Turing.MultiTapePTM.runFrom {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) : Cslib.OracleComp spec (List Symbol)

Observe the output word of an open run.

def Turing.MultiTapePTM.run {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (input : List Symbol) : Cslib.OracleComp spec (List Symbol)

Run from the initial configuration with explicit coin and oracle programs.

@[simp]

theorem Turing.MultiTapePTM.runFrom_zero {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) : machine.runFrom coin query 0 cfg = pure cfg.tapes.output

A zero clock observes the current output without drawing a coin or making a query.

theorem Turing.MultiTapePTM.runFrom_succ {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) : machine.runFrom coin query (fuel + 1) cfg = match cfg.tapes.state with | none => pure cfg.tapes.output | some state => do let bit ← coin match machine.tr state cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols bit with | MultiTapeMachine.Action.step action symbol move => machine.runFrom coin query fuel (cfg.step action symbol move) | MultiTapeMachine.Action.query op next => do let answer ← query op (cfg.channels op).queryBuffer machine.runFrom coin query fuel (cfg.receive op next answer)

A live instruction draws one coin, then performs one ordinary step or one external request. This equation is left out of the simp set to avoid expanding a symbolic clock.

noncomputable def Turing.MultiTapePTM.runClosed {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input : List Symbol) : Cslib.ProbComp (List Symbol)

The closed fair-coin run, with fresh uniform Boolean choices at each live transition.

theorem Turing.MultiTapePTM.length_output_eval_runClosed_le {k : ℕ} {Symbol State : Type} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (input output : List Symbol) (h : output ∈ (machine.runClosed fuel input).eval.support) : output.length ≤ fuel

Every supported closed output has length at most the machine's clock.

def Turing.MultiTapePTM.toNondeterministic {k : ℕ} {Symbol State Oracle : Type} (machine : MultiTapePTM k Symbol State Oracle) : MultiTapeMachine k Symbol State Oracle Set

Forget probabilities, retaining exactly the actions selected by some coin value.