Finite Mathlib TM0 machines with binary input and output

The source has a finite alphabet and state set. Input bits are mapped to source symbols. A halted source configuration supplies the complete binary output at and to the right of its tape head. The CSLib simulator copies and rewinds its input, simulates each source transition on symbol tracks, then emits that output.

structure Complexity.MathlibTM0.BinaryMachine : Type 1

A finite Mathlib machine with a faithful binary encoding of its input and output.

• Alphabet : Type

  Source tape alphabet.

• State : Type

  Source control states.

• alphabetFinite : Fintype self.Alphabet

  The tape alphabet is finite.

• alphabetInhabited : Inhabited self.Alphabet

  The default symbol is blank.

• stateFinite : Fintype self.State

  The control state set is finite.

• stateInhabited : Inhabited self.State

  The default control state is initial.

• bit : Bool → self.Alphabet

  Encode an input or output bit as a source symbol.

• readBit : self.Alphabet → Option Bool

  Decode an output bit, stopping on a nonbinary symbol.

• readBit_bit (b : Bool) : self.readBit (self.bit b) = some b

  Encoded bits decode faithfully.

• readBit_blank : self.readBit default = none

  Blank terminates the output.

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

  The source transition function.

@[reducible, inline]

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

A configuration of the source machine.

Equations

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

@[reducible, inline]

abbrev Complexity.MathlibTM0.BinaryMachine.step (M : BinaryMachine) : M.Config → Option M.Config

One transition, using the alphabet and initial-state instances of the bundle.

Equations

• M.step = Turing.TM0.step M.code

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

Run exactly the given number of source transitions, failing if a step is unavailable.

Equations

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

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

A halted source run whose entire right-of-head tape is the encoded binary output.

Equations

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

inductive Complexity.MathlibTM0.Control (Q : Type u_1) : Type u_1

Simulator phases: input copying, rewind, source execution, and output emission.

• copy {Q : Type u_1} : Control Q

  Copy input bits to symbol tracks.

• rewind {Q : Type u_1} : Control Q

  Rewind the symbol tracks to the first input cell.

• run {Q : Type u_1} : Q → Control Q

  Execute one source control state.

• emit {Q : Type u_1} : Control Q

  Emit the binary output at and right of the halted source head.

@[instance_reducible]

instance Complexity.MathlibTM0.instFintypeControl {Q✝ : Type u_1} [Fintype Q✝] : Fintype (Control Q✝)

Equations

• Complexity.MathlibTM0.instFintypeControl = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Q✝ ⊕ Unit) (Complexity.MathlibTM0.Control.proxyTypeEquiv Q✝)

@[reducible, inline]

abbrev Complexity.MathlibTM0.Track (M : BinaryMachine) : Type

One binary work tape per source alphabet symbol.

Equations

• Complexity.MathlibTM0.Track M = Fin (Fintype.card M.Alphabet)

noncomputable def Complexity.MathlibTM0.trackEquiv (M : BinaryMachine) : Track M ≃ M.Alphabet

Associate each work tape with its source alphabet symbol.

Equations

• Complexity.MathlibTM0.trackEquiv M = (Fintype.equivFin M.Alphabet).symm

def Complexity.MathlibTM0.idle (M : BinaryMachine) (state : Option (Control M.State)) (output : Option Bool) (inputMove : SignType) : Turing.Action (Fintype.card M.Alphabet) Bool (Control M.State)

A transition leaving the work tapes unchanged.

Equations

• Complexity.MathlibTM0.idle M state output inputMove = { inputTape := inputMove, workTapes := fun (x : Fin (Fintype.card M.Alphabet)) => (none, 0), output := output, state := state }

def Complexity.MathlibTM0.moveSign : Turing.Dir → SignType

The displacement corresponding to one source move.

Equations

• Complexity.MathlibTM0.moveSign Turing.Dir.left = SignType.neg
• Complexity.MathlibTM0.moveSign Turing.Dir.right = SignType.pos

noncomputable def Complexity.MathlibTM0.runAction (M : BinaryMachine) (q : M.State) (work : Track M → Option Bool) : Turing.Action (Fintype.card M.Alphabet) Bool (Control M.State)

Simulate a source transition, switching to output emission when the source halts.

Equations

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

noncomputable def Complexity.MathlibTM0.machine (M : BinaryMachine) : Turing.MultiTapeTM (Fintype.card M.Alphabet) Bool (Control M.State)

The finite binary CSLib simulator.

Equations

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