Finite tape machines with a marked first input cell

Stack encodings distinguish the first cell and represent the empty word by a marker. This bundle keeps that format explicit, while allowing output symbols to differ from input symbols. The binary-track simulator can decode the output without rewriting the source tape.

structure Complexity.MathlibTM0.MarkedMachine : Type 1

A finite TM0 with a first-cell input marker and a separate output decoder.

• Alphabet : Type

  Source tape alphabet.

• State : Type

  Source control states.

• alphabetFinite : Fintype self.Alphabet

  The source alphabet is finite.

• alphabetInhabited : Inhabited self.Alphabet

  The default symbol is blank.

• stateFinite : Fintype self.State

  The source control is finite.

• stateInhabited : Inhabited self.State

  The default state is initial.

• bit : Bool → Bool → self.Alphabet

  Encode a bit, distinguishing the first cell from subsequent cells.

• empty : self.Alphabet

  The single cell representing empty input.

• readBit : self.Alphabet → Option Bool

  Decode output, stopping at the first symbol with no decoded bit.

• readBit_blank : self.readBit default = none

  Blank terminates output.

• code : Turing.TM0.Machine self.Alphabet self.State

  Source transitions.

inductive Complexity.MathlibTM0.MarkedMachine.Symbol (Γ : Type) : Type

Source symbols plus unused raw bits needed by the existing simulator bundle.

• raw {Γ : Type} : Bool → Symbol Γ

  A raw bit in the simulator's ordinary binary interface.

• source {Γ : Type} : Γ → Symbol Γ

  An actual source symbol.

@[instance_reducible]

instance Complexity.MathlibTM0.MarkedMachine.instFintypeSymbol {Γ✝ : Type} [Fintype Γ✝] : Fintype (Symbol Γ✝)

Equations

• Complexity.MathlibTM0.MarkedMachine.instFintypeSymbol = Fintype.ofEquiv (Bool ⊕ Γ✝) (Complexity.MathlibTM0.MarkedMachine.Symbol.proxyTypeEquiv Γ✝)

@[instance_reducible]

instance Complexity.MathlibTM0.MarkedMachine.instInhabitedSymbol {Γ : Type} [Inhabited Γ] : Inhabited (Symbol Γ)

Equations

• Complexity.MathlibTM0.MarkedMachine.instInhabitedSymbol = { default := Complexity.MathlibTM0.MarkedMachine.Symbol.source default }

def Complexity.MathlibTM0.MarkedMachine.Symbol.value {Γ : Type} [Inhabited Γ] : Symbol Γ → Γ

Forget the unused raw-bit symbols.

Equations

• (Complexity.MathlibTM0.MarkedMachine.Symbol.raw a).value = default
• (Complexity.MathlibTM0.MarkedMachine.Symbol.source a).value = a

def Complexity.MathlibTM0.MarkedMachine.inputCells (M : MarkedMachine) : Bool → List Bool → List M.Alphabet

Format an input suffix; only an empty complete input needs the empty marker.

Equations

• M.inputCells x✝ [] = if x✝ = true then [M.empty] else []
• M.inputCells x✝ (b :: bs) = M.bit x✝ b :: M.inputCells false bs

@[reducible, inline]

abbrev Complexity.MathlibTM0.MarkedMachine.Config (M : MarkedMachine) : Type

A source configuration with the bundle's blank and initial-state conventions.

Equations

• M.Config = Turing.TM0.Cfg M.Alphabet M.State

def Complexity.MathlibTM0.MarkedMachine.run (M : MarkedMachine) : ℕ → M.Config → Option M.Config

Execute exactly the specified number of source transitions.

Equations

• M.run 0 x✝ = some x✝
• M.run t.succ x✝ = (Turing.TM0.step M.code x✝).bind (M.run t)

def Complexity.MathlibTM0.MarkedMachine.OutputsWithin (M : MarkedMachine) (input output : List Bool) (time : ℕ) : Prop

A bounded source run whose complete decoded right-of-head output is specified.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Complexity.MathlibTM0.MarkedMachine.binary (M : MarkedMachine) : BinaryMachine

Add unused raw-bit symbols to reuse the existing binary-machine simulation.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Complexity.MathlibTM0.MarkedMachine.TargetState (M : MarkedMachine) : Type

The new copying phase, followed by the existing rewind, run, and emit phases.

Equations

• M.TargetState = (Bool ⊕ Complexity.MathlibTM0.Control M.State)

noncomputable def Complexity.MathlibTM0.MarkedMachine.machine (M : MarkedMachine) : Turing.MultiTapeTM (Fintype.card M.binary.Alphabet) Bool M.TargetState

Copy a marked source input, then delegate to the existing tape simulator.

Equations

• One or more equations did not get rendered due to their size.