Running the common machine with finite data

The finite interpreter executes the unchanged transition table using cslib's existing tapes. Its choice and query handlers are the same typed programs as the native interpreter's handlers. The bounded loop is an ordinary OracleComp.iterate program.

Equality of the resulting programs preserves every sampling and external interaction, including the complete private state of any later interpreter. The representation theorem is independent of efficient handlers or finite control. Efficient encoded realization remains subsequent work.

Main definitions

• Turing.MultiTapeMachine.finiteStep: one native instruction on finite storage.
• Turing.MultiTapeMachine.finiteRunFrom: a bounded loop followed by output projection.

Main results

• Turing.MultiTapeMachine.finiteRunFrom_eq: exact agreement with the native output program.
• Turing.MultiTapeMachine.finiteRunFrom_init: agreement from blank initial storage.

References

Generalizes Computability/Machines/Turing/MultiTape/Probabilistic/Finite.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common choice mechanism.

def Turing.MultiTapeMachine.finiteStep {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : FiniteConfig k Symbol State Oracle) : Cslib.OracleComp spec (FiniteConfig k Symbol State Oracle)

One native transition on finite storage, using the original choice and external handlers. A halted configuration remains unchanged without either effect.

def Turing.MultiTapeMachine.finiteRunFrom {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : FiniteConfig k Symbol State Oracle) : Cslib.OracleComp spec (List Symbol)

Execute a bounded functional loop and observe its accumulated output.

theorem Turing.MultiTapeMachine.finiteRunFrom_eq {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (finite : FiniteConfig k Symbol State Oracle) (cfg : Config k Symbol State Oracle finite.tapes.input) (h : finite.Represents cfg) : machine.finiteRunFrom choose query fuel finite = machine.runFrom choose query fuel cfg

The finite and native interpreters return the very same typed program. In particular, they preserve private state for every later interpretation of choices and oracle calls.

theorem Turing.MultiTapeMachine.finiteRunFrom_init {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (input : List Symbol) : machine.finiteRunFrom choose query fuel (FiniteConfig.init machine.initial input) = machine.run choose query fuel input

Finite blank storage realizes the standard native run, with identical choice and query programs and no assumptions on their distributions.