TM Combinators

This file provides TM constructions for composing machines, used to prove closure properties of complexity classes.

Main definitions

• TM.unionTM — Given tm₁ : TM n₁ deciding L₁ and tm₂ : TM n₂ deciding L₂, construct a TM (n₁ + 1 + n₂) that decides L₁ ∪ L₂.
• TM.complementTM — Given a TM deciding L, construct a TM (with the same number of work tapes) deciding Lᶜ by flipping the output bit.
• TM.seqTM — Sequential composition: run tm₁ to completion, then tm₂ on the same tapes.
• TM.ifTM — Conditional branching: run a test machine, then branch to a "then" or "else" machine based on its output.
• TM.loopTM — Loop combinator: repeatedly run a body machine then a test machine, halting when the test outputs Γ.one.
• TM.scannerTM — Generic finite-state scanner: fold a finite-state transition function over the input bits and emit a final symbol.
• TM.retargetInput — Given M : TM k, construct a TM (k + 1) that runs M but reads its "input" from work tape k instead of the input tape.

Design

The union machine has three phases:

1. Phase 1: Simulate tm₁, redirecting its output to work tape n₁ (a "fake output" tape). The real output tape stays pristine.
2. Transition: Rewind the fake output to cell 1 and check the result. If Γ.one (tm₁ accepted), write Γ.one to the real output and halt. Otherwise rewind the input tape and reset Phase-2 tapes to cell 0.
3. Phase 2: Simulate tm₂ using work tapes n₁+1..n₁+n₂ and the real output tape.

Work tape layout (0-indexed)

• 0 .. n₁-1 — Phase 1's work tapes (mirrors tm₁.work)
• n₁ — Phase 1's redirected output (mirrors tm₁.output)
• n₁+1 .. n₁+n₂ — Phase 2's work tapes (mirrors tm₂.work)

State space

Q₁ ⊕ UnionPhase ⊕ Q₂ where UnionPhase encodes the four transition states between Phase 1 and Phase 2.

def Complexity.TM.idleDir (head : Γ) : Dir3

Direction for an idle tape: move right if reading ▷, else stay. Satisfies δ_right_of_start for tapes not involved in the current phase.

Equations

• Complexity.TM.idleDir head = if head = Complexity.Γ.start then Complexity.Dir3.right else Complexity.Dir3.stay

def Complexity.TM.moveLeftDir (head : Γ) : Dir3

Direction for a tape we want to move left: move left unless reading ▷, in which case move right to satisfy δ_right_of_start. During actual execution the tape won't be at cell 0, so this always moves left.

Equations

• Complexity.TM.moveLeftDir head = if head = Complexity.Γ.start then Complexity.Dir3.right else Complexity.Dir3.left

theorem Complexity.TM.idleDir_start : idleDir Γ.start = Dir3.right

idleDir moves right when reading the start symbol ▷.

theorem Complexity.TM.idleDir_right_of_start {head : Γ} (h : head = Γ.start) : idleDir head = Dir3.right

If the head reads ▷, then idleDir moves right — the shape of the δ_right_of_start obligation for idle tapes.

theorem Complexity.TM.moveLeftDir_right_of_start {head : Γ} (h : head = Γ.start) : moveLeftDir head = Dir3.right

If the head reads ▷, then moveLeftDir moves right — the shape of the δ_right_of_start obligation for tapes being rewound.

def Complexity.TM.readBackWrite (g : Γ) : Γw

Write back the same symbol read from a tape, preserving cell contents. Maps ▷ to □ since Tape.write at position 0 is a no-op anyway.

Equations

• Complexity.TM.readBackWrite Complexity.Γ.zero = Complexity.Γw.zero
• Complexity.TM.readBackWrite Complexity.Γ.one = Complexity.Γw.one
• Complexity.TM.readBackWrite Complexity.Γ.blank = Complexity.Γw.blank
• Complexity.TM.readBackWrite Complexity.Γ.start = Complexity.Γw.blank

def Complexity.TM.allIdle {σ : Type} {k : ℕ} (newState : σ) (iHead : Γ) (wHeads : Fin k → Γ) (oHead : Γ) : σ × (Fin k → Γw) × Γw × Dir3 × (Fin k → Dir3) × Dir3

The "do nothing" transition output: all writes are □, all directions are idleDir. Used for states that only change the control state.

Equations

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

theorem Complexity.TM.rightOfStart_allIdle {k : ℕ} (iHead : Γ) (wHeads : Fin k → Γ) (oHead : Γ) : (iHead = Γ.start → idleDir iHead = Dir3.right) ∧ (∀ (i : Fin k), wHeads i = Γ.start → idleDir (wHeads i) = Dir3.right) ∧ (oHead = Γ.start → idleDir oHead = Dir3.right)

Proof that all-idle directions satisfy δ_right_of_start.

inductive Complexity.TM.UnionPhase : Type

Intermediate states between Phase 1 and Phase 2 of the union machine.

• rewindOut : UnionPhase
• checkResult : UnionPhase
• rewindIn : UnionPhase
• setup2 : UnionPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqUnionPhase : DecidableEq UnionPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeUnionPhase : Fintype UnionPhase

Equations

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

@[reducible, inline]

abbrev Complexity.TM.UnionQ (Q₁ Q₂ : Type) : Type

The state type for the union TM.

Equations

• Complexity.TM.UnionQ Q₁ Q₂ = (Q₁ ⊕ Complexity.TM.UnionPhase ⊕ Q₂)

def Complexity.TM.fakeOutIdx {n₁ n₂ : ℕ} : Fin (n₁ + 1 + n₂)

Index of the fake output tape (work tape n₁).

Equations

• Complexity.TM.fakeOutIdx = ⟨n₁, ⋯⟩

def Complexity.TM.phase1WorkReads {n₁ n₂ : ℕ} (wHeads : Fin (n₁ + 1 + n₂) → Γ) (i : Fin n₁) : Γ

Read tm₁'s work tapes from the composite work tapes.

Equations

• Complexity.TM.phase1WorkReads wHeads i = wHeads ⟨↑i, ⋯⟩

def Complexity.TM.phase2WorkReads {n₁ n₂ : ℕ} (wHeads : Fin (n₁ + 1 + n₂) → Γ) (j : Fin n₂) : Γ

Read tm₂'s work tapes from the composite work tapes.

Equations

• Complexity.TM.phase2WorkReads wHeads j = wHeads ⟨n₁ + 1 + ↑j, ⋯⟩

def Complexity.TM.unionTM {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) : TM (n₁ + 1 + n₂)

Construct a TM deciding L₁ ∪ L₂ from TMs deciding L₁ and L₂.

The composite machine has n₁ + 1 + n₂ work tapes:

• 0 .. n₁-1 for tm₁'s work tapes
• n₁ for tm₁'s redirected output
• n₁+1 .. n₁+n₂ for tm₂'s work tapes

Equations

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

inductive Complexity.TM.ComplementPhase : Type

Intermediate states for the complement machine's output-flipping phase.

• rewind : ComplementPhase
• flip : ComplementPhase
• done : ComplementPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqComplementPhase : DecidableEq ComplementPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeComplementPhase : Fintype ComplementPhase

Equations

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

@[reducible, inline]

abbrev Complexity.TM.ComplementQ (Q : Type) : Type

The state type for the complement TM.

Equations

• Complexity.TM.ComplementQ Q = (Q ⊕ Complexity.TM.ComplementPhase)

def Complexity.TM.flipBit (g : Γ) : Γw

Flip a readable symbol: 1 ↔ 0, blanks stay blank.

Equations

• Complexity.TM.flipBit Complexity.Γ.one = Complexity.Γw.zero
• Complexity.TM.flipBit Complexity.Γ.zero = Complexity.Γw.one
• Complexity.TM.flipBit Complexity.Γ.blank = Complexity.Γw.blank
• Complexity.TM.flipBit Complexity.Γ.start = Complexity.Γw.blank

def Complexity.TM.complementTM {n : ℕ} (tm : TM n) : TM n

Construct a TM deciding Lᶜ from a TM deciding L.

The complement machine has the same number of work tapes as the original. It runs in three stages:

1. Simulate: Run the original TM. When it halts, transition to rewind.
2. Rewind: Move the output head left to ▷ (cell 0), then right to cell 1.
3. Flip: Read output cell 1, write the flipped bit, and halt.

Equations

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

inductive Complexity.TM.IfPhase : Type

Intermediate states for the conditional branching machine.

• rewindOut : IfPhase
• check : IfPhase
• done : IfPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqIfPhase : DecidableEq IfPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeIfPhase : Fintype IfPhase

Equations

• Complexity.TM.instFintypeIfPhase = { elems := {Complexity.TM.IfPhase.rewindOut, Complexity.TM.IfPhase.check, Complexity.TM.IfPhase.done}, complete := Complexity.TM.instFintypeIfPhase._proof_1 }

@[reducible, inline]

abbrev Complexity.TM.IfQ (QT QThen QElse : Type) : Type

The state type for the conditional branching TM.

Equations

• Complexity.TM.IfQ QT QThen QElse = (QT ⊕ Complexity.TM.IfPhase ⊕ QThen ⊕ QElse)

def Complexity.TM.ifTM {n : ℕ} (tmTest tmThen tmElse : TM n) : TM n

Conditional branching: run tmTest to completion, read its output at cell 1, then run tmThen (if output = Γ.one) or tmElse (otherwise).

All three machines share the same n work tapes, input tape, and output tape. Work tape contents are preserved across all transitions via readBackWrite, maintaining shared state for the branch machines.

Phases

1. Test: Simulate tmTest. When it halts, enter rewind.
2. Rewind output: Move output head left to ▷ (cell 0).
3. Check: Move output head right to cell 1, read the test result. If Γ.one, enter tmThen.qstart. Otherwise, enter tmElse.qstart.
4. Branch: Simulate tmThen or tmElse. When the branch machine halts, transition to the done halt state.

Time

t_test + (output_head_pos + 2) + 1 + t_branch + 1 where output_head_pos ≤ t_test. Total: at most 2·t_test + t_branch + 4.

Equations

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

@[reducible, inline]

abbrev Complexity.TM.SeqQ (Q₁ Q₂ : Type) : Type

The state type for the sequential composition TM.

Equations

• Complexity.TM.SeqQ Q₁ Q₂ = (Q₁ ⊕ Q₂)

def Complexity.TM.seqTM {n : ℕ} (tm₁ tm₂ : TM n) : TM n

Sequential composition: run tm₁ to completion, then tm₂ on the same tapes.

Both machines share the same n work tapes, input tape, and output tape. When tm₁ halts, there is one transition step that:

• Changes state from Q₁ to Q₂ (entering tm₂.qstart)
• Preserves all tape cell contents (via readBackWrite)
• Moves any tape head at position 0 to position 1 (forced by δ_right_of_start)
• Leaves all other tape head positions unchanged

After the transition, tm₂ runs from the resulting tape state. Total time: t₁ + 1 + t₂ where t₁ and t₂ are the run times of tm₁ and tm₂ respectively.

Equations

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

inductive Complexity.TM.LoopPhase : Type

Intermediate states for the loop machine's output-checking phase.

• rewindOut : LoopPhase
• check : LoopPhase
• done : LoopPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqLoopPhase : DecidableEq LoopPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeLoopPhase : Fintype LoopPhase

Equations

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

@[reducible, inline]

abbrev Complexity.TM.LoopQ (QBody QTest : Type) : Type

The state type for the loop TM.

Equations

• Complexity.TM.LoopQ QBody QTest = (QBody ⊕ Complexity.TM.LoopPhase ⊕ QTest)

def Complexity.TM.loopTM {n : ℕ} (tmBody tmTest : TM n) : TM n

Loop combinator: repeatedly run tmBody then tmTest, halting when the test's output at cell 1 is Γ.one.

Both machines share the same n work tapes, input tape, and output tape. Work tape contents are preserved across transitions (via readBackWrite), allowing the body to accumulate state across iterations.

Phases

1. Body: Simulate tmBody. When it halts, transition to test.
2. Test: Simulate tmTest. When it halts, enter rewind.
3. Rewind output: Move output head left to ▷ (cell 0).
4. Check: Move right to cell 1, read the test result. If Γ.one, enter done (halt). Otherwise, transition back to body.

Use case

The UTM's main loop: loopTM simStepTM checkHaltTM runs one simulation step, then checks if the simulated machine has halted.

Equations

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

inductive Complexity.TM.ScannerPhase (S : Type) : Type

Control states of a generic finite-state scanner parameterized by a user-supplied scan-state type S. The machine has a one-time start step that advances off cell 0, then a stream of scan s states holding the current scan state, and finally a done halt state.

• start {S : Type} : ScannerPhase S
• scan {S : Type} (s : S) : ScannerPhase S
• done {S : Type} : ScannerPhase S

@[implicit_reducible]

instance Complexity.TM.instDecidableEqScannerPhase {S : Type} [DecidableEq S] : DecidableEq (ScannerPhase S)

Equations

• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.start Complexity.TM.ScannerPhase.start = isTrue ⋯
• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.start (Complexity.TM.ScannerPhase.scan s) = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.start Complexity.TM.ScannerPhase.done = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase (Complexity.TM.ScannerPhase.scan s) Complexity.TM.ScannerPhase.start = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase (Complexity.TM.ScannerPhase.scan s) Complexity.TM.ScannerPhase.done = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.done Complexity.TM.ScannerPhase.start = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.done (Complexity.TM.ScannerPhase.scan s) = isFalse ⋯
• Complexity.TM.instDecidableEqScannerPhase Complexity.TM.ScannerPhase.done Complexity.TM.ScannerPhase.done = isTrue ⋯
• Complexity.TM.instDecidableEqScannerPhase (Complexity.TM.ScannerPhase.scan s₁) (Complexity.TM.ScannerPhase.scan s₂) = if h : s₁ = s₂ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeScannerPhaseOfDecidableEq {S : Type} [DecidableEq S] [Fintype S] : Fintype (ScannerPhase S)

Equations

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

def Complexity.TM.scannerTM {S : Type} [DecidableEq S] [Fintype S] (s₀ : S) (scanStep : S → Bool → S) (finalOutput : S → Γw) : TM 0

Generic finite-state scanner.

A 0-work-tape TM parameterized by a scan-state type S, an initial state s₀, a transition function scanStep : S → Bool → S (called on each input bit), and a finalizer finalOutput : S → Γw (the symbol to emit when end-of-input is reached).

Semantics: runs left-to-right through the input, folding scanStep over the bits starting from s₀; when a blank is reached, writes finalOutput (finalState) to output cell 1 and halts.

This captures the common "read once, fold into a fixed-size state" pattern used by evenLength, allZeros/allOnes, containsZero/containsOne, lengthDivBy k, lastBit, and similar regular-language scanners.

Halts in |x| + 2 steps on every input (1 start + |x| scans + 1 halt).

Equations

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

def Complexity.TM.retargetInput {k : ℕ} (M : TM k) : TM (k + 1)

Given a DTM M : TM k, construct a DTM retargetInput M : TM (k + 1) that behaves like M but reads its "input" from work tape k (the last work tape) instead of the real input tape.

Tape layout:

• Real input tape: ignored (moved idly each step, never read).
• Work tapes 0..k-1: mirror M's work tapes.
• Work tape k: plays the role of M's input tape (read-only, no writes except a no-op readBackWrite that preserves cells).

When work tape k is initialized with Tape.init (z.map Γ.ofBool), the machine simulates M on input z.

Used in witnessLang NTM constructions where the verifier DTM's "input" (e.g. pair(x, y)) is built on a work tape rather than supplied on the real input tape.

Equations

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