TM Subroutines

Small concrete Turing machines used as composable building blocks for constructing larger machines via seqTM, ifTM, and loopTM.

Subroutine correctness theorems live in the proof modules under Complexitylib.Models.TuringMachine.Subroutines.Internal; reusable public statements are re-exported by focused surface modules when needed.

Main definitions

• TM.writeTM — write a symbol to output cell 1 and halt
• TM.rewindWorkTM — rewind a work tape head to cell 1
• TM.rewindInputTM — rewind the input tape head to cell 1
• TM.scanRightTM — scan a work tape right until blank
• TM.blankWorkTM — blank a started work tape while scanning right
• TM.clearWorkTM — blank a started work tape and rewind it to cell 1
• TM.copyInputToWorkTM — copy input tape contents to a work tape
• TM.copyInputToOutputTM — copy input tape contents to the output tape
• TM.copyWorkToWorkTM — copy one work tape's contents to another
• TM.compareWorkTapesTM — compare two work tapes cell by cell

inductive Complexity.TM.WritePhase : Type

State space of writeTM: rewind the output head to ▷, step right to cell 1, write the symbol, then halt.

• rewind : WritePhase
• goRight : WritePhase
• write : WritePhase
• done : WritePhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqWritePhase : DecidableEq WritePhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeWritePhase : Fintype WritePhase

Equations

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

def Complexity.TM.writeTM {n : ℕ} (sym : Γw) : TM n

Write sym to output cell 1 and halt. Phases: rewind output to ▷ → move right to cell 1 → write → halt.

Equations

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

@[reducible, inline]

abbrev Complexity.TM.writeOneTM {n : ℕ} : TM n

writeTM specialized to write Γw.one to output cell 1 (accept).

Equations

• Complexity.TM.writeOneTM = Complexity.TM.writeTM Complexity.Γw.one

@[reducible, inline]

abbrev Complexity.TM.writeZeroTM {n : ℕ} : TM n

writeTM specialized to write Γw.zero to output cell 1 (reject).

Equations

• Complexity.TM.writeZeroTM = Complexity.TM.writeTM Complexity.Γw.zero

inductive Complexity.TM.RewindPhase : Type

State space of rewindWorkTM/rewindInputTM: move the head left until it reads ▷, then move right once to land on cell 1 and halt.

• moveLeft : RewindPhase
• moveRight : RewindPhase
• done : RewindPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqRewindPhase : DecidableEq RewindPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeRewindPhase : Fintype RewindPhase

Equations

• Complexity.TM.instFintypeRewindPhase = { elems := {Complexity.TM.RewindPhase.moveLeft, Complexity.TM.RewindPhase.moveRight, Complexity.TM.RewindPhase.done}, complete := ⋯ }

def Complexity.TM.rewindWorkTM {n : ℕ} (idx : Fin n) : TM n

Rewind work tape idx to cell 1 (first data cell after ▷).

Equations

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

def Complexity.TM.rewindInputTM {n : ℕ} : TM n

Rewind the input tape to cell 1 (first data cell after ▷). Work and output tapes are only written with readBackWrite, so their contents are preserved under the usual no-start-under-head side conditions.

Equations

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

inductive Complexity.TM.ScanPhase : Type

State space of scanRightTM/blankWorkTM: scan right until reading Γ.blank, then halt.

• scanning : ScanPhase
• done : ScanPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqScanPhase : DecidableEq ScanPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeScanPhase : Fintype ScanPhase

Equations

• Complexity.TM.instFintypeScanPhase = { elems := {Complexity.TM.ScanPhase.scanning, Complexity.TM.ScanPhase.done}, complete := ⋯ }

def Complexity.TM.scanRightTM {n : ℕ} (idx : Fin n) : TM n

Scan work tape idx right until finding Γ.blank. On canonical binary tapes, its exact content- and frame-preserving behavior is specified by scanRightTM_reachesIn_frame and scanRightTM_hoareTime_frame.

Equations

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

def Complexity.TM.blankWorkTM {n : ℕ} (idx : Fin n) : TM n

Scan work tape idx right until finding Γ.blank, overwriting every visited nonblank cell with Γ.blank. This consumes a started Boolean string and leaves the tape blank to the right of the current head.

Equations

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

def Complexity.TM.clearWorkTM {n : ℕ} (idx : Fin n) : TM n

Blank a started work tape and rewind it to cell 1, yielding the standard started blank tape shape.

Equations

• Complexity.TM.clearWorkTM idx = (Complexity.TM.blankWorkTM idx).seqTM (Complexity.TM.rewindWorkTM idx)

inductive Complexity.TM.CopyPhase : Type

State space shared by the input/work/output copy machines: copy symbols rightward until the source reads Γ.blank, then halt.

• copying : CopyPhase
• done : CopyPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqCopyPhase : DecidableEq CopyPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeCopyPhase : Fintype CopyPhase

Equations

• Complexity.TM.instFintypeCopyPhase = { elems := {Complexity.TM.CopyPhase.copying, Complexity.TM.CopyPhase.done}, complete := ⋯ }

def Complexity.TM.copyInputToWorkTM {n : ℕ} (idx : Fin n) : TM n

Copy input tape data to work tape idx. Reads input right, writes to work tape. Stops when input reads Γ.blank. Skips ▷ at cell 0.

Equations

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

def Complexity.TM.copyInputToOutputTM {n : ℕ} : TM n

Copy the Boolean input to the output tape while scanning both tapes rightward. The first transition skips the left-end markers, each subsequent nonblank input symbol is written to the output, and the machine halts at the first input blank. Work-tape contents are preserved; heads reading the left-end marker take their required one-cell rightward bounce.

Equations

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

def Complexity.TM.copyWorkToWorkTM {n : ℕ} (src dst : Fin n) : TM n

Copy the contents of work tape src to work tape dst. Reads src right, writes the same bits to dst, and stops when src reads Γ.blank. The source tape contents are preserved by writing the currently read symbol back before moving right.

Equations

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

inductive Complexity.TM.ComparePhase : Type

State space of compareWorkTapesTM: compare cells while both tapes agree, ending in matchDone (equal) or mismatch (unequal) before halting.

• comparing : ComparePhase
• mismatch : ComparePhase
• matchDone : ComparePhase
• done : ComparePhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqComparePhase : DecidableEq ComparePhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeComparePhase : Fintype ComparePhase

Equations

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

def Complexity.TM.compareWorkTapesTM {n : ℕ} (idx₁ idx₂ : Fin n) : TM n

Compare work tapes idx₁ and idx₂ cell by cell. Both advance right together. Stops when both read Γ.blank. Writes Γ.one to output if match, Γ.zero if mismatch. Assumes output head is at cell 1.

Equations

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