Simulating Complexitylib machines on CSLib multi-tape machines

This file defines a CSLib multi-tape machine (Turing.MultiTapeTM) over the binary alphabet that simulates a Complexitylib machine tm : TM n step for step.

The two models differ in four ways, and the simulator handles each:

• Left-end markers. Our tapes carry ▷ in cell 0, but CSLib's binary tapes hold only 0, 1, and blank. Each of our work tapes and our output tape is therefore simulated by two CSLib tapes whose heads move together: a data tape holding cells 1, 2, … and a marker tape holding a single 1 at position 0, written in the simulator's first step. The marker tape reads 1 exactly when the head is on our cell 0, where writes are no-ops and left moves stay put.
• Output. Our output tape is read-write, while CSLib emits output symbols one at a time. When tm halts, the simulator rewinds its copy of the output tape to cell 1, reads the verdict there, and emits it as a single bit.
• Input head range. CSLib's input head stops one cell past the input, but ours can run arbitrarily far into the blank tail. The last CSLib work tape counts how far our head is past that last cell. It holds 1 at position 0 and is never written again, so it reads 1 exactly when the count is zero.
• The left input boundary. CSLib reads a blank both before and after the input. An InputZone flag in the state records whether our input head is on ▷. After a left move from inside the input the flag is probe, and the next read settles it: the only position left of the input's end that reads blank is position 0.

Main definitions

• Complexity.TM.MultiTapeState — the simulator's states
• Complexity.TM.toMultiTape — the CSLib machine simulating tm
• Complexity.TM.toMultiTapeFun — the variant whose final phase copies the whole output string instead of the verdict bit, for function computation

def Complexity.Dir3.toSign : Dir3 → SignType

A head direction as a CSLib head movement.

Equations

• Complexity.Dir3.left.toSign = -1
• Complexity.Dir3.right.toSign = 1
• Complexity.Dir3.stay.toSign = 0

def Complexity.Γ.ofCell : Option Bool → Γ

Read a binary CSLib cell as one of our symbols, with CSLib's blank as □.

Equations

• Complexity.Γ.ofCell none = Complexity.Γ.blank
• Complexity.Γ.ofCell (some b) = Complexity.Γ.ofBool b

def Complexity.Γw.toCell : Γw → Option Bool

Store a writable symbol in a binary CSLib cell, with □ as CSLib's blank.

Equations

• Complexity.Γw.zero.toCell = some false
• Complexity.Γw.one.toCell = some true
• Complexity.Γw.blank.toCell = none

inductive Complexity.TM.InputZone : Type

Where the simulated input head is, as far as the simulator's finite control knows.

• left : InputZone

  On the left-end marker.

• inner : InputZone

  Past the left-end marker.

• probe : InputZone

  Just moved left from within the input: on ▷ exactly when the input symbol now read is blank.

@[instance_reducible]

instance Complexity.TM.instDecidableEqInputZone : DecidableEq InputZone

Equations

• Complexity.TM.instDecidableEqInputZone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeInputZone : Fintype InputZone

Equations

• Complexity.TM.instFintypeInputZone = { elems := {Complexity.TM.InputZone.left, Complexity.TM.InputZone.inner, Complexity.TM.InputZone.probe}, complete := ⋯ }

def Complexity.TM.InputZone.atLeft : InputZone → Option Bool → Bool

Whether the input head is on the left-end marker, given the zone flag and the CSLib input symbol under the head.

Equations

• Complexity.TM.InputZone.left.atLeft x✝ = true
• Complexity.TM.InputZone.inner.atLeft x✝ = false
• Complexity.TM.InputZone.probe.atLeft x✝ = x✝.isNone

inductive Complexity.TM.MultiTapeState (Q : Type) : Type

The states of the simulator for a machine with states Q.

• init {Q : Type} : MultiTapeState Q

  Write the position-0 markers.

• run {Q : Type} (q : Q) (zone : InputZone) : MultiTapeState Q

  Simulate state q of the original machine.

• rewind {Q : Type} : MultiTapeState Q

  Move the simulated output head back to the left-end marker.

• verdict {Q : Type} : MultiTapeState Q

  Read the verdict in output cell 1 and halt.

def Complexity.TM.instDecidableEqMultiTapeState.decEq {Q✝ : Type} [DecidableEq Q✝] (x✝ x✝¹ : MultiTapeState Q✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.init Complexity.TM.MultiTapeState.init = isTrue ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.init (Complexity.TM.MultiTapeState.run q zone) = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.init Complexity.TM.MultiTapeState.rewind = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.init Complexity.TM.MultiTapeState.verdict = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq (Complexity.TM.MultiTapeState.run q zone) Complexity.TM.MultiTapeState.init = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq (Complexity.TM.MultiTapeState.run q zone) Complexity.TM.MultiTapeState.rewind = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq (Complexity.TM.MultiTapeState.run q zone) Complexity.TM.MultiTapeState.verdict = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.rewind Complexity.TM.MultiTapeState.init = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.rewind (Complexity.TM.MultiTapeState.run q zone) = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.rewind Complexity.TM.MultiTapeState.rewind = isTrue ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.rewind Complexity.TM.MultiTapeState.verdict = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.verdict Complexity.TM.MultiTapeState.init = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.verdict (Complexity.TM.MultiTapeState.run q zone) = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.verdict Complexity.TM.MultiTapeState.rewind = isFalse ⋯
• Complexity.TM.instDecidableEqMultiTapeState.decEq Complexity.TM.MultiTapeState.verdict Complexity.TM.MultiTapeState.verdict = isTrue ⋯

@[instance_reducible]

instance Complexity.TM.instDecidableEqMultiTapeState {Q✝ : Type} [DecidableEq Q✝] : DecidableEq (MultiTapeState Q✝)

Equations

• Complexity.TM.instDecidableEqMultiTapeState = Complexity.TM.instDecidableEqMultiTapeState.decEq

@[instance_reducible]

instance Complexity.TM.instFintypeMultiTapeState {Q✝ : Type} [Fintype Q✝] : Fintype (MultiTapeState Q✝)

Equations

• Complexity.TM.instFintypeMultiTapeState = Fintype.ofEquiv (Unit ⊕ (_ : Q✝) × Complexity.TM.InputZone ⊕ Unit ⊕ Unit) (Complexity.TM.MultiTapeState.proxyTypeEquiv Q✝)

@[reducible, inline]

abbrev Complexity.TM.simTapes (n : ℕ) : ℕ

The number of CSLib work tapes simulating a machine with n work tapes: a data tape and a marker tape for each of our n + 1 read-write tapes, and the input overshoot counter.

Equations

• Complexity.TM.simTapes n = n + 1 + (n + 1) + 1

def Complexity.TM.dataIdx {n : ℕ} (i : Fin (n + 1)) : Fin (simTapes n)

CSLib data tape of our read-write tape i; tape Fin.last n is our output tape.

Equations

• Complexity.TM.dataIdx i = Fin.castAdd 1 (Fin.castAdd (n + 1) i)

def Complexity.TM.markIdx {n : ℕ} (i : Fin (n + 1)) : Fin (simTapes n)

CSLib marker tape of our read-write tape i.

Equations

• Complexity.TM.markIdx i = Fin.castAdd 1 (Fin.natAdd (n + 1) i)

def Complexity.TM.overIdx {n : ℕ} : Fin (simTapes n)

CSLib work tape counting how far the input head is past the input.

Equations

• Complexity.TM.overIdx = Fin.natAdd (n + 1 + (n + 1)) 0

def Complexity.TM.tapeLayout {n : ℕ} {α : Type u_1} (data mark : Fin (n + 1) → α) (over : α) : Fin (simTapes n) → α

Assemble per-tape actions into CSLib's tape order.

Equations

• Complexity.TM.tapeLayout data mark over = Fin.append (Fin.append data mark) ![over]

def Complexity.TM.simRead {n : ℕ} (w : Fin (simTapes n) → Option Bool) (i : Fin (n + 1)) : Γ

Our symbol under the head of simulated tape i, from the CSLib symbols w under all heads.

Equations

• Complexity.TM.simRead w i = if w (Complexity.TM.markIdx i) = some true then Complexity.Γ.start else Complexity.Γ.ofCell (w (Complexity.TM.dataIdx i))

def Complexity.TM.oneSidedMove (atStart : Bool) (d : Dir3) : SignType

The CSLib head move simulating move d on a one-sided tape. On ▷ (cell 0) a left move stays put, matching Tape.move.

Equations

• Complexity.TM.oneSidedMove atStart d = if (atStart && decide (d = Complexity.Dir3.left)) = true then 0 else d.toSign

def Complexity.TM.oneSidedWrite (atStart : Bool) (w : Γw) : Option (Option Bool)

The CSLib write simulating a write of w on a one-sided tape. On ▷ (cell 0) the write is dropped, matching Tape.write.

Equations

• Complexity.TM.oneSidedWrite atStart w = if atStart = true then none else some w.toCell

def Complexity.TM.inputAction (atLeft : Bool) (i ov : Option Bool) : Dir3 → SignType × SignType × InputZone

The moves simulating an input-head move d: the CSLib input head move, the overshoot counter move, and the next zone. atLeft says the head is on ▷, i is the CSLib input symbol, and ov is the counter tape's symbol, which is 1 exactly when the counter is zero.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.inputAction atLeft i ov Complexity.Dir3.right = if (!atLeft && i.isNone) = true then (0, 1, Complexity.TM.InputZone.inner) else (1, 0, Complexity.TM.InputZone.inner)
• Complexity.TM.inputAction atLeft i ov Complexity.Dir3.stay = (0, 0, if atLeft = true then Complexity.TM.InputZone.left else Complexity.TM.InputZone.inner)

def Complexity.TM.toMultiTapeTr {n : ℕ} (tm : TM n) (q : MultiTapeState tm.Q) (i : Option Bool) (w : Fin (simTapes n) → Option Bool) : Turing.Action (simTapes n) Bool (MultiTapeState tm.Q)

The simulator's transition function.

Equations

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

def Complexity.TM.toMultiTape {n : ℕ} (tm : TM n) : Turing.MultiTapeTM (simTapes n) Bool (MultiTapeState tm.Q)

The CSLib multi-tape machine simulating tm. Our work tape i and our output tape (i = n) each use a data tape and a marker tape, and the last tape counts input-head overshoot. It emits the single bit true to accept and false to reject.

Equations

• tm.toMultiTape = { q₀ := Complexity.TM.MultiTapeState.init, tr := tm.toMultiTapeTr }

def Complexity.TM.toMultiTapeFunTr {n : ℕ} (tm : TM n) (q : MultiTapeState tm.Q) (i : Option Bool) (w : Fin (simTapes n) → Option Bool) : Turing.Action (simTapes n) Bool (MultiTapeState tm.Q)

The transition function of the function-computing simulator: the decision simulator's, except that the final state copies the simulated output cell under the head to CSLib's output and moves right, halting at the first blank.

Equations

• One or more equations did not get rendered due to their size.
• tm.toMultiTapeFunTr q i w = tm.toMultiTapeTr q i w

def Complexity.TM.toMultiTapeFun {n : ℕ} (tm : TM n) : Turing.MultiTapeTM (simTapes n) Bool (MultiTapeState tm.Q)

The CSLib multi-tape machine computing the function tm computes: it simulates tm, rewinds the simulated output tape, and copies the output string to CSLib's output.

Equations

• tm.toMultiTapeFun = { q₀ := Complexity.TM.MultiTapeState.init, tr := tm.toMultiTapeFunTr }