Marked tape computations over finite input and output alphabets

The binary simulator parses explicit finite-alphabet codewords before writing source cells. It rejects malformed codes before starting the source. Source execution reuses symbol tracks, and output emission writes complete codewords. Input and output alphabets and their chosen numberings are independent.

structure Complexity.MathlibTM0.AlphabetMachine (Input Output : Type) : Type 1

A finite tape machine with marked input symbols and a separate output alphabet.

• Alphabet : Type

  Source tape alphabet.

• State : Type

  Source control states.

• alphabetFinite : Fintype self.Alphabet

  Source alphabet finiteness.

• alphabetInhabited : Inhabited self.Alphabet

  Default source symbol is blank.

• stateFinite : Fintype self.State

  Source control finiteness.

• stateInhabited : Inhabited self.State

  Default control is initial.

• inputSymbol : Bool → Input → self.Alphabet

  Encode an input letter, distinguishing the first cell.

• empty : self.Alphabet

  The single cell representing empty input.

• readSymbol : self.Alphabet → Option Output

  Decode an output letter, stopping on a symbol with no output letter.

• readSymbol_blank : self.readSymbol default = none

  Blank terminates output.

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

  Source transition function.

@[reducible, inline]

abbrev Complexity.MathlibTM0.AlphabetMachine.simulatorSource {Input Output : Type} (M : AlphabetMachine Input Output) : MarkedMachine

Reuse the existing source simulator; its binary endpoints are never entered.

Equations

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

def Complexity.MathlibTM0.AlphabetMachine.inputCells {Input Output : Type} (M : AlphabetMachine Input Output) : Bool → List Input → List M.Alphabet

Source cells for a complete input or an unmarked suffix.

Equations

• M.inputCells x✝ [] = if x✝ = true then [M.empty] else []
• M.inputCells x✝ (a :: xs) = M.inputSymbol x✝ a :: M.inputCells false xs

def Complexity.MathlibTM0.AlphabetMachine.OutputsWithin {Input Output : Type} (M : AlphabetMachine Input Output) (input : List Input) (output : List Output) (time : ℕ) : Prop

A bounded source run specifying every decoded output cell.

Equations

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

inductive Complexity.MathlibTM0.AlphabetMachine.Phase (inputSize outputSize : ℕ) (Q : Type) : Type

Parse a symbol code, rewind, run the existing simulator, or finish a codeword.

• copy {inputSize outputSize : ℕ} {Q : Type} : Bool → Option (Fin (inputSize + 1)) → Phase inputSize outputSize Q

  none waits for an opening delimiter; some i counts unary index bits.

• rewind {inputSize outputSize : ℕ} {Q : Type} : Bool → Phase inputSize outputSize Q

  Moving backwards alternates between closing and opening delimiters.

• source {inputSize outputSize : ℕ} {Q : Type} : Control Q → Phase inputSize outputSize Q

  Existing source execution control; emission is replaced by encoded output.

• emit {inputSize outputSize : ℕ} {Q : Type} : Fin (outputSize + 1) → Phase inputSize outputSize Q

  Emit the remaining unary index bits and then the closing delimiter.

@[instance_reducible]

instance Complexity.MathlibTM0.AlphabetMachine.instFintypePhase {inputSize✝ outputSize✝ : ℕ} {Q✝ : Type} [Fintype Q✝] : Fintype (Phase inputSize✝ outputSize✝ Q✝)

Equations

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

def Complexity.MathlibTM0.AlphabetMachine.pause {k : ℕ} {Q : Type} (state : Option Q) (output : Option Bool) (move : SignType) : Turing.Action k Bool Q

An action preserving every work tape and head.

Equations

• Complexity.MathlibTM0.AlphabetMachine.pause state output move = { inputTape := move, workTapes := fun (x : Fin k) => (none, 0), output := output, state := state }

noncomputable def Complexity.MathlibTM0.AlphabetMachine.machine {Input Output : Type} (M : AlphabetMachine Input Output) (input : FiniteAlphabetCode Input) (output : FiniteAlphabetCode Output) : Turing.MultiTapeTM (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase input.size output.size M.State)

Parse finite-alphabet inputs, simulate the source, and encode its complete output.

Equations

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