A binary simulator for finite-alphabet multitape machines

Each source tape is represented by one binary track per source symbol. Input copying and rewinding cost 2 * n + 2 steps; each source transition costs one step, and halting costs one. The source model is OpenAI's finite multitape model, imported in LowerBound.Defs.

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.encode {Γ : Type u_1} [Inhabited Γ] (a b : Γ) : Option Bool

Encode a symbol by one track per alphabet symbol; blank is all blank tracks.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.encode a b = Complexity.SymbolTracks.encode a b

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.decode {Γ : Type u_1} [Inhabited Γ] (v : Γ → Option Bool) : Γ

Decode a vector of symbol tracks, inverse to the one-hot encoding.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.decode v = Complexity.SymbolTracks.decode v

def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.moveSign : HeadMove → SignType

Translate the three source head directions to CSLib head displacements.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.moveSign Complexity.DepthThreeLowerBound.HeadMove.left = SignType.neg
• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.moveSign Complexity.DepthThreeLowerBound.HeadMove.stay = SignType.zero
• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.moveSign Complexity.DepthThreeLowerBound.HeadMove.right = SignType.pos

inductive Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Control (Q : Type u_1) : Type u_1

Copy the input, rewind its work tracks, then run the source control.

• copy {Q : Type u_1} : Control Q

  Copy the input bits to the designated work tracks.

• rewind {Q : Type u_1} : Control Q

  Return all input work heads to the first cell.

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

  Simulate the source control state.

@[instance_reducible]

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

Equations

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Track (M : FiniteMultiTapeMachine) : Type

One binary work tape per source tape and source alphabet symbol.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.Track M = Fin (Fintype.card (M.K × M.Γ))

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.trackEquiv (M : FiniteMultiTapeMachine) : Track M ≃ M.K × M.Γ

Identify the numbered CSLib work tapes with source tape-symbol pairs.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.trackEquiv M = (Fintype.equivFin (M.K × M.Γ)).symm

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.track (M : FiniteMultiTapeMachine) (k : M.K) (a : M.Γ) : Track M

The binary work tape recording one symbol on one source tape.

Equations

• Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.track M k a = (Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.trackEquiv M).symm (k, a)

def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.idle (M : FiniteMultiTapeMachine) (state : Option (Control M.Q)) (output : Option Bool) (inputMove : SignType) : Turing.Action (Fintype.card (M.K × M.Γ)) Bool (Control M.Q)

A transition that leaves every work tape unchanged.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.runAction (M : FiniteMultiTapeMachine) (q : M.Q) (work : Track M → Option Bool) : Turing.Action (Fintype.card (M.K × M.Γ)) Bool (Control M.Q)

Simulate a source transition, or emit its verdict and halt.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.machine (M : FiniteMultiTapeMachine) : Turing.MultiTapeTM (Fintype.card (M.K × M.Γ)) Bool (Control M.Q)

A binary CSLib simulator with two initialization states and one state per source state.

Equations

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