Finite data for multi-tape configurations

FiniteCfg replaces the native integer-indexed work tapes by CSLib's BiTape data. The input, control, output and action types retain their original meanings. Its simulation relation allows the native heads to have any absolute positions; the finite tapes store their contents relative to their current heads.

MultiTapeMachine.FiniteConfig adds finite query buffers and read-only answer tapes. It uses the same named channels and the same local actions and query instructions as the shared machine core. Each channel has finite storage; encoding all channels as finite data additionally requires the channel type to be finite. The representation laws do not need that restriction.

Main definitions

• Turing.FiniteCfg: finite input, work tapes, output and control.
• Turing.MultiTapeMachine.FiniteConfig: finite storage with oracle channels.
• Turing.MultiTapeMachine.FiniteConfig.SpaceBound: input, work, output, query and reply budgets.

Main results

• Turing.MultiTapeMachine.FiniteConfig.Represents.step: preserve native observations.
• Turing.MultiTapeMachine.FiniteConfig.Represents.receive: preserve the channel reset semantics.
• Turing.MultiTapeMachine.FiniteConfig.SpaceBound.step: per-instruction storage growth.

References

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using Bolton Bailey's upstream BiTape and the common native machine configurations.

structure Turing.FiniteCfg (k : ℕ) (Symbol : Type u_1) (State : Type u_2) : Type (max u_1 u_2)

A configuration stored entirely as finite data. The input is included so the representation has one fixed type across all runtime inputs.

• input : List Symbol

  The immutable input word.

• state : Option State

  The current control, or none when halted.

• inputPos : Fin (self.input.length + 2)

  The native input position, including the two boundary cells.

• workTapes : Fin k → Cslib.Turing.BiTape Symbol

  Work tapes centered at their current heads.

• output : List Symbol

  Symbols already written to the output.

theorem Turing.FiniteCfg.ext_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {x y : FiniteCfg k Symbol State} : x = y ↔ x.input = y.input ∧ x.state = y.state ∧ x.inputPos ≍ y.inputPos ∧ x.workTapes = y.workTapes ∧ x.output = y.output

theorem Turing.FiniteCfg.ext {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {x y : FiniteCfg k Symbol State} (input : x.input = y.input) (state : x.state = y.state) (inputPos : x.inputPos ≍ y.inputPos) (workTapes : x.workTapes = y.workTapes) (output : x.output = y.output) : x = y

def Turing.FiniteCfg.toCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) : Cfg k Symbol State finite.input

The integer-indexed view with each work head placed at zero. Absolute work-head positions are irrelevant to observations, so the representation relation also admits translated views.

def Turing.FiniteCfg.inputSymbol {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) : Option Symbol

Observe the native read-only input geometry.

theorem Turing.FiniteCfg.inputSymbol_eq_getD {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) : finite.inputSymbol = (none :: List.map some finite.input)[↑finite.inputPos]?.getD none

Reading the native input is list lookup with an initial blank and a blank default.

def Turing.FiniteCfg.workTapeSymbols {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) : Fin k → Option Symbol

Observe one symbol per work tape.

def Turing.FiniteCfg.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) (action : Action k Symbol State) : FiniteCfg k Symbol State

Apply a native action to finite storage.

def Turing.FiniteCfg.init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (state : State) (input : List Symbol) : FiniteCfg k Symbol State

Initial finite storage uses the native input-head convention and blank work tapes.

structure Turing.FiniteCfg.Represents {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (finite : FiniteCfg k Symbol State) (cfg : Cfg k Symbol State finite.input) : Prop

The finite data and native configuration have identical observations and corresponding work-tape contents at every displacement from their heads.

• state : finite.state = cfg.state

  Control states agree.

• inputPos : finite.inputPos = cfg.inputPos

  Input positions agree.

• workTapes (tape : Fin k) : (finite.workTapes tape).Represents (cfg.workTapes tape) (cfg.workTapePos tape)

  Each finite work tape represents the native tape at its native head position.

• output : finite.output = cfg.output

  Accumulated outputs agree.

theorem Turing.FiniteCfg.represents_init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (state : State) (input : List Symbol) : (init state input).Represents (Cfg.init state input)

theorem Turing.FiniteCfg.Represents.inputSymbol {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {finite : FiniteCfg k Symbol State} {cfg : Cfg k Symbol State finite.input} (h : finite.Represents cfg) : finite.inputSymbol = cfg.inputSymbol

Related configurations read the same input cell.

theorem Turing.FiniteCfg.Represents.workTapeSymbols {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {finite : FiniteCfg k Symbol State} {cfg : Cfg k Symbol State finite.input} (h : finite.Represents cfg) : finite.workTapeSymbols = cfg.workTapeSymbols

Related configurations read the same work cells.

theorem Turing.FiniteCfg.Represents.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {finite : FiniteCfg k Symbol State} {cfg : Cfg k Symbol State finite.input} (h : finite.Represents cfg) (action : Action k Symbol State) : (finite.step action).Represents (action.apply cfg)

The same native action preserves the representation relation.

structure Turing.MultiTapeMachine.FiniteConfig (k : ℕ) (Symbol : Type u_1) (State : Type u_2) (Oracle : Type u_3) : Type (max (max u_1 u_2) u_3)

Finite tape storage for a shared-core configuration. Each channel stores its pending request and an answer tape centered at its current head. A finite channel type makes the whole configuration a finite collection of finite data.

• tapes : FiniteCfg k Symbol State

  The ordinary input, work, control and output components.

• channels : Oracle → List Symbol × Cslib.Turing.BiTape Symbol

  Per-channel pending requests and read-only answer tapes.

theorem Turing.MultiTapeMachine.FiniteConfig.ext {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {x y : FiniteConfig k Symbol State Oracle} (tapes : x.tapes = y.tapes) (channels : x.channels = y.channels) : x = y

theorem Turing.MultiTapeMachine.FiniteConfig.ext_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {x y : FiniteConfig k Symbol State Oracle} : x = y ↔ x.tapes = y.tapes ∧ x.channels = y.channels

def Turing.MultiTapeMachine.FiniteConfig.answerSymbols {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (finite : FiniteConfig k Symbol State Oracle) : Oracle → Option Symbol

The current answer symbols supplied to the shared transition table.

def Turing.MultiTapeMachine.FiniteConfig.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (finite : FiniteConfig k Symbol State Oracle) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : FiniteConfig k Symbol State Oracle

An ordinary step applies the tape action and moves each answer head.

def Turing.MultiTapeMachine.FiniteConfig.receive {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} [DecidableEq Oracle] (finite : FiniteConfig k Symbol State Oracle) (oracle : Oracle) (next : State) (answer : List Symbol) : FiniteConfig k Symbol State Oracle

A query clears just its selected buffer and installs the reply at position zero.

def Turing.MultiTapeMachine.FiniteConfig.init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (state : State) (input : List Symbol) : FiniteConfig k Symbol State Oracle

Initial finite storage has empty buffers and blank answer tapes.

structure Turing.MultiTapeMachine.FiniteConfig.SpaceBound {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (inputSize steps answerSize : ℕ) (finite : FiniteConfig k Symbol State Oracle) : Prop

Storage bounds after a number of native transitions. Replies can be longer than the clock; their size is therefore tracked separately from the work tapes and pending query buffers.

• input : finite.tapes.input.length ≤ inputSize

  The input is stored once.

• work (tape : Fin k) : (finite.tapes.workTapes tape).spaceUsed ≤ steps + 1

  Work space grows by at most one cell per transition on each tape.

• output : finite.tapes.output.length ≤ steps

  At most one output symbol is written per transition.

• query (channel : Oracle) : (finite.channels channel).1.length ≤ steps

  At most one query symbol per channel is written per transition.

• answer (channel : Oracle) : (finite.channels channel).2.spaceUsed ≤ steps + answerSize + 1

  Answer storage includes the installed reply and head movements since installation.

theorem Turing.MultiTapeMachine.FiniteConfig.SpaceBound.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {inputSize steps answerSize inputSize' steps' answerSize' : ℕ} {finite : FiniteConfig k Symbol State Oracle} (h : SpaceBound inputSize steps answerSize finite) (hi : inputSize ≤ inputSize') (ht : steps ≤ steps') (ha : answerSize ≤ answerSize') : SpaceBound inputSize' steps' answerSize' finite

Storage bounds may be enlarged independently.

theorem Turing.MultiTapeMachine.FiniteConfig.spaceBound_init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (state : State) (input : List Symbol) (answerSize : ℕ) : SpaceBound input.length 0 answerSize (init state input)

Initially only the input occupies nonblank storage.

theorem Turing.MultiTapeMachine.FiniteConfig.SpaceBound.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {inputSize steps answerSize : ℕ} {finite : FiniteConfig k Symbol State Oracle} (h : SpaceBound inputSize steps answerSize finite) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : SpaceBound inputSize (steps + 1) answerSize (finite.step action symbol move)

A local native transition respects the per-step storage bounds.

theorem Turing.MultiTapeMachine.FiniteConfig.SpaceBound.receive {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} [DecidableEq Oracle] {inputSize steps answerSize : ℕ} {finite : FiniteConfig k Symbol State Oracle} (h : SpaceBound inputSize steps answerSize finite) (channel : Oracle) (next : State) (answer : List Symbol) (hanswer : answer.length ≤ answerSize) : SpaceBound inputSize (steps + 1) answerSize (finite.receive channel next answer)

Installing a bounded reply preserves the storage bounds and clears only its own query.

structure Turing.MultiTapeMachine.FiniteConfig.Represents {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (finite : FiniteConfig k Symbol State Oracle) (cfg : Config k Symbol State Oracle finite.tapes.input) : Prop

The observation-preserving relation to the shared native configuration.

• tapes : finite.tapes.Represents cfg.tapes

  Ordinary configurations correspond.

• queries (oracle : Oracle) : (finite.channels oracle).1 = (cfg.channels oracle).queryBuffer

  Pending requests agree exactly, including requests not yet submitted.

• answers (oracle : Oracle) : (finite.channels oracle).2.Represents (fun (position : ℤ) => if 0 ≤ position then (cfg.channels oracle).answer[position.toNat]? else none) (cfg.channels oracle).answerPos

  Answer tapes agree at every displacement from their heads.

theorem Turing.MultiTapeMachine.FiniteConfig.represents_init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} (state : State) (input : List Symbol) : (init state input).Represents { tapes := Cfg.init state input }

The finite and native initial configurations correspond.

theorem Turing.MultiTapeMachine.FiniteConfig.Represents.answerSymbols {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {finite : FiniteConfig k Symbol State Oracle} {cfg : Config k Symbol State Oracle finite.tapes.input} (h : finite.Represents cfg) : finite.answerSymbols = cfg.answerSymbols

The transition table sees the same answer symbols in both representations.

theorem Turing.MultiTapeMachine.FiniteConfig.Represents.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} {finite : FiniteConfig k Symbol State Oracle} {cfg : Config k Symbol State Oracle finite.tapes.input} (h : finite.Represents cfg) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : (finite.step action symbol move).Represents (cfg.step action symbol move)

An ordinary shared-core action preserves all finite representations.

theorem Turing.MultiTapeMachine.FiniteConfig.Represents.receive {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Oracle : Type u_3} [DecidableEq Oracle] {finite : FiniteConfig k Symbol State Oracle} {cfg : Config k Symbol State Oracle finite.tapes.input} (h : finite.Represents cfg) (oracle : Oracle) (next : State) (answer : List Symbol) : (finite.receive oracle next answer).Represents (cfg.receive oracle next answer)

Submission resets precisely the selected channel, retaining every other pending query and answer head. The installed reply has the native position-zero geometry.