Turing machines

This file defines the library's base model of computation: multi-tape deterministic and nondeterministic Turing machines over a fixed four-symbol alphabet, with named input/work/output tapes. The model's shape follows Arora–Barak (Computational Complexity: A Modern Approach, Definitions 1.1–1.4 and 2.1), with the conventions below enforced structurally.

Main definitions

• Γ — the tape alphabet {0, 1, □, ▷} (read alphabet)
• Γw — the writable alphabet {0, 1, □} (write alphabet; ▷ cannot be written)
• Dir3 — three-way tape head direction (left, right, stay)
• Tape — a one-sided infinite tape; cell 0 is leftmost and permanently ▷
• Cfg — a machine configuration with named tapes (input, work, output)
• TM — a deterministic multi-tape Turing machine (AB Definition 1.1)
• NTM — a nondeterministic TM with two transition functions (AB Definition 2.1)
• TM.stepRel, TM.reaches, TM.reachesIn — deterministic step relation and reachability
• NTM.trace — execute an NTM for a fixed choice sequence (canonical NTM execution)
• Tape.HasOutput — predicate: tape contains a given binary string as output
• TM.ComputesInTime — computing a function in bounded time (AB Definition 1.4)
• TM.Computes — computing a function (existential over time bound)
• TM.Accepts, TM.AcceptsInTime — deterministic acceptance
• NTM.Accepts, NTM.AcceptsInTime — nondeterministic acceptance (existential)
• Cfg.WithinAuxSpace, Cfg.WithinDecisionSpace — honest tape-space bounds
• TM.DecidesInTime, NTM.DecidesInTime — deciding a language within a time bound
• TM.DecidesInTimeSpace — deciding with simultaneous time and space bounds
• NTM.acceptCount, NTM.acceptProb — counting/probabilistic acceptance
• TM.toNTM — embed a DTM into an NTM

Design notes

• One-sided tapes: Tape uses head : ℕ and cells : ℕ → Γ. Cell 0 is leftmost; moving left at position 0 is a no-op (Nat subtraction saturates).
• Immutable cell 0: Tape.write is a no-op when the head is at position 0, ensuring ▷ at cell 0 is permanent. Combined with Γw (which excludes ▷), this guarantees ▷ appears only at cell 0 on every tape.
• Read vs write alphabet: The transition function reads Γ = {0, 1, □, ▷} but writes Γw = {0, 1, □}, so δ structurally cannot write ▷.
• Finite state: Q carries [Fintype Q]; the state space is finite.
• Output: Read from cell 1 of the output tape (first cell after ▷); machine output is the binary string written after ▷.
• Named tapes: Cfg has input, work, output fields rather than Fin k → Tape, making the read-only/read-write distinction structural.
• NTM execution: Defined via trace (a fixed choice sequence), not a relational step.

inductive Complexity.Γ : Type

The tape alphabet Γ = {0, 1, □, ▷}.

• zero : Γ
• one : Γ
• blank : Γ
• start : Γ

@[implicit_reducible]

instance Complexity.instReprΓ : Repr Γ

Equations

• Complexity.instReprΓ = { reprPrec := Complexity.instReprΓ.repr }

def Complexity.instReprΓ.repr : Γ → ℕ → Std.Format

Equations

• Complexity.instReprΓ.repr Complexity.Γ.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γ.zero")).group prec✝
• Complexity.instReprΓ.repr Complexity.Γ.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γ.one")).group prec✝
• Complexity.instReprΓ.repr Complexity.Γ.blank prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γ.blank")).group prec✝
• Complexity.instReprΓ.repr Complexity.Γ.start prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γ.start")).group prec✝

@[implicit_reducible]

instance Complexity.instDecidableEqΓ : DecidableEq Γ

Equations

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

@[implicit_reducible]

instance Complexity.instFintypeΓ : Fintype Γ

Equations

• Complexity.instFintypeΓ = { elems := {Complexity.Γ.zero, Complexity.Γ.one, Complexity.Γ.blank, Complexity.Γ.start}, complete := Complexity.instFintypeΓ._proof_1 }

@[implicit_reducible]

instance Complexity.instInhabitedΓ : Inhabited Γ

Equations

• Complexity.instInhabitedΓ = { default := Complexity.Γ.blank }

inductive Complexity.Γw : Type

The writable alphabet Γw = {0, 1, □}. The start symbol ▷ cannot be written by a transition function — this is enforced structurally by using Γw in the output of δ.

• zero : Γw
• one : Γw
• blank : Γw

@[implicit_reducible]

instance Complexity.instReprΓw : Repr Γw

Equations

• Complexity.instReprΓw = { reprPrec := Complexity.instReprΓw.repr }

def Complexity.instReprΓw.repr : Γw → ℕ → Std.Format

Equations

• Complexity.instReprΓw.repr Complexity.Γw.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γw.zero")).group prec✝
• Complexity.instReprΓw.repr Complexity.Γw.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γw.one")).group prec✝
• Complexity.instReprΓw.repr Complexity.Γw.blank prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Γw.blank")).group prec✝

@[implicit_reducible]

instance Complexity.instDecidableEqΓw : DecidableEq Γw

Equations

• Complexity.instDecidableEqΓw x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.instFintypeΓw : Fintype Γw

Equations

• Complexity.instFintypeΓw = { elems := {Complexity.Γw.zero, Complexity.Γw.one, Complexity.Γw.blank}, complete := Complexity.instFintypeΓw._proof_1 }

def Complexity.Γw.toΓ : Γw → Γ

Embed a writable symbol into the full alphabet.

Equations

• Complexity.Γw.zero.toΓ = Complexity.Γ.zero
• Complexity.Γw.one.toΓ = Complexity.Γ.one
• Complexity.Γw.blank.toΓ = Complexity.Γ.blank

@[implicit_reducible]

instance Complexity.instCoeΓwΓ : Coe Γw Γ

Equations

• Complexity.instCoeΓwΓ = { coe := Complexity.Γw.toΓ }

theorem Complexity.Γw.toΓ_ne_start (s : Γw) : s.toΓ ≠ Γ.start

A writable symbol is never the left-end marker.

def Complexity.Γ.ofBool : Bool → Γ

Convert a boolean to an alphabet symbol.

Equations

• Complexity.Γ.ofBool false = Complexity.Γ.zero
• Complexity.Γ.ofBool true = Complexity.Γ.one

theorem Complexity.Γ.ofBool_ne_start (b : Bool) : ofBool b ≠ start

A Boolean tape symbol is never the left-end marker.

theorem Complexity.Γ.ofBool_ne_blank (b : Bool) : ofBool b ≠ blank

A Boolean tape symbol is never blank.

def Complexity.Γw.ofBool : Bool → Γw

Convert a boolean to a writable symbol.

Equations

• Complexity.Γw.ofBool false = Complexity.Γw.zero
• Complexity.Γw.ofBool true = Complexity.Γw.one

theorem Complexity.Γw.ofBool_toΓ (b : Bool) : (ofBool b).toΓ = Γ.ofBool b

inductive Complexity.Dir3 : Type

Three-way tape head direction: left, right, or stay.

• left : Dir3
• right : Dir3
• stay : Dir3

def Complexity.instReprDir3.repr : Dir3 → ℕ → Std.Format

Equations

• Complexity.instReprDir3.repr Complexity.Dir3.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Dir3.left")).group prec✝
• Complexity.instReprDir3.repr Complexity.Dir3.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Dir3.right")).group prec✝
• Complexity.instReprDir3.repr Complexity.Dir3.stay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Dir3.stay")).group prec✝

@[implicit_reducible]

instance Complexity.instReprDir3 : Repr Dir3

Equations

• Complexity.instReprDir3 = { reprPrec := Complexity.instReprDir3.repr }

@[implicit_reducible]

instance Complexity.instDecidableEqDir3 : DecidableEq Dir3

Equations

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

@[implicit_reducible]

instance Complexity.instFintypeDir3 : Fintype Dir3

Equations

• Complexity.instFintypeDir3 = { elems := {Complexity.Dir3.left, Complexity.Dir3.right, Complexity.Dir3.stay}, complete := Complexity.instFintypeDir3._proof_1 }

structure Complexity.Tape : Type

A one-sided infinite tape. Cell 0 is the leftmost cell and permanently contains ▷. The head cannot move left of cell 0 (moving left at position 0 is a no-op via Nat subtraction). Writing at cell 0 is a no-op, preserving ▷.

• head : ℕ

  The head position; cell 0 is the leftmost cell.

• cells : ℕ → Γ

  The tape contents, one symbol per cell.

theorem Complexity.Tape.ext_iff {x y : Tape} : x = y ↔ x.head = y.head ∧ x.cells = y.cells

theorem Complexity.Tape.ext {x y : Tape} (head : x.head = y.head) (cells : x.cells = y.cells) : x = y

def Complexity.Tape.read (t : Tape) : Γ

Read the symbol under the head.

Equations

• t.read = t.cells t.head

def Complexity.Tape.write (t : Tape) (s : Γ) : Tape

Write a symbol at the head position. Writing at cell 0 is a no-op, preserving the start symbol ▷.

Equations

• t.write s = if t.head = 0 then t else { head := t.head, cells := Function.update t.cells t.head s }

theorem Complexity.Tape.write_head (t : Tape) (s : Γ) : (t.write s).head = t.head

Writing changes tape contents but preserves the head position.

def Complexity.Tape.move (t : Tape) (d : Dir3) : Tape

Move the head according to a three-way direction. Moving left at position 0 stays at 0 (Nat subtraction saturates).

Equations

• t.move Complexity.Dir3.left = { head := t.head - 1, cells := t.cells }
• t.move Complexity.Dir3.right = { head := t.head + 1, cells := t.cells }
• t.move Complexity.Dir3.stay = t

theorem Complexity.Tape.move_cells (t : Tape) (d : Dir3) : (t.move d).cells = t.cells

Moving changes the head position but preserves tape contents.

theorem Complexity.Tape.head_move_le (t : Tape) (d : Dir3) : (t.move d).head ≤ t.head + 1

Moving changes the head position by at most one.

def Complexity.Tape.HasOutput (t : Tape) (y : List Bool) : Prop

The tape contains output y : List Bool starting at cell 1: cells 1 through |y| match y, and cell |y| + 1 is blank. Output is the binary string written on the output tape after ▷.

Equations

• t.HasOutput y = ((∀ (i : ℕ) (h : i < y.length), t.cells (i + 1) = Complexity.Γ.ofBool y[i]) ∧ t.cells (y.length + 1) = Complexity.Γ.blank)

theorem Complexity.Tape.hasOutput_congr {t₁ t₂ : Tape} (h : t₁.cells = t₂.cells) (y : List Bool) : t₁.HasOutput y ↔ t₂.HasOutput y

HasOutput depends only on the tape cells, not the head position.

@[implicit_reducible]

instance Complexity.Tape.decidableHasOutput (t : Tape) (y : List Bool) : Decidable (t.HasOutput y)

Equations

• t.decidableHasOutput y = if h : (∀ (i : Fin y.length), t.cells (↑i + 1) = Complexity.Γ.ofBool y[↑i]) ∧ t.cells (y.length + 1) = Complexity.Γ.blank then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Complexity.Tape.writeAndMove (t : Tape) (s : Γ) (d : Dir3) : Tape

Write a symbol and move in one step.

Equations

• t.writeAndMove s d = (t.write s).move d

def Complexity.Tape.StartInvariant (t : Tape) : Prop

t.StartInvariant says the left-end marker ▷ sits at cell 0 and nowhere else — the standing shape of every tape reachable from an initial configuration, since writes exclude ▷ and cell 0 is immutable.

Equations

• t.StartInvariant = (t.cells 0 = Complexity.Γ.start ∧ ∀ (j : ℕ), 1 ≤ j → t.cells j ≠ Complexity.Γ.start)

theorem Complexity.Tape.StartInvariant.read_ne_start {t : Tape} (h : t.StartInvariant) (hhead : 1 ≤ t.head) : t.read ≠ Γ.start

Under the invariant, a head at position ≥ 1 never reads ▷.

theorem Complexity.Tape.StartInvariant.write {t : Tape} (h : t.StartInvariant) (s : Γw) : (t.write s.toΓ).StartInvariant

Writing (any Γw symbol) preserves the invariant.

theorem Complexity.Tape.StartInvariant.move {t : Tape} (h : t.StartInvariant) (d : Dir3) : (t.move d).StartInvariant

Moving preserves the invariant (cells unchanged).

theorem Complexity.Tape.StartInvariant.writeAndMove {t : Tape} (h : t.StartInvariant) (s : Γw) (d : Dir3) : (t.writeAndMove s.toΓ d).StartInvariant

Writing a Γw symbol and moving preserves the invariant.

theorem Complexity.Tape.head_writeAndMove_le (t : Tape) (s : Γ) (d : Dir3) : (t.writeAndMove s d).head ≤ t.head + 1

One write-and-move step advances the head by at most one.

def Complexity.Tape.init (contents : List Γ) : Tape

Initialize a tape: ▷ at cell 0, contents at cells 1, 2, ..., □ elsewhere. Head starts at position 0 (on ▷).

Equations

• Complexity.Tape.init contents = { head := 0, cells := fun (i : ℕ) => if i = 0 then Complexity.Γ.start else contents[i - 1]?.getD Complexity.Γ.blank }

@[simp]

theorem Complexity.Tape.init_head (contents : List Γ) : (init contents).head = 0

An initialized tape starts with its head on the left-end marker.

@[simp]

theorem Complexity.Tape.init_cells_zero (contents : List Γ) : (init contents).cells 0 = Γ.start

Cell zero of an initialized tape is the left-end marker.

theorem Complexity.Tape.init_cells_succ (contents : List Γ) (i : ℕ) : (init contents).cells (i + 1) = contents[i]?.getD Γ.blank

Cell i + 1 of an initialized tape contains item i, or blank when i lies beyond the initialized contents.

theorem Complexity.Tape.init_cells_ge (contents : List Γ) (i : ℕ) (h : contents.length ≤ i) : (init contents).cells (i + 1) = Γ.blank

Cells beyond the initialized contents are blank.

@[simp]

theorem Complexity.Tape.init_nil_cells_succ (i : ℕ) : (init []).cells (i + 1) = Γ.blank

Every positive-indexed cell of the empty initialized tape is blank.

theorem Complexity.Tape.init_nil_cells_ne_start (j : ℕ) (hj : 1 ≤ j) : (init []).cells j ≠ Γ.start

No positive-indexed cell of the empty initialized tape is a start marker.

theorem Complexity.Tape.init_ofBool_cells_lt (contents : List Bool) (i : ℕ) (h : i < contents.length) : (init (List.map Γ.ofBool contents)).cells (i + 1) = Γ.ofBool contents[i]

Within the initialized Boolean contents, cell i + 1 stores bit i.

theorem Complexity.Tape.init_ofBool_cells_ge (contents : List Bool) (i : ℕ) (h : contents.length ≤ i) : (init (List.map Γ.ofBool contents)).cells (i + 1) = Γ.blank

Beyond the initialized Boolean contents, cell i + 1 is blank.

theorem Complexity.Tape.init_ofBool_cells_ne_start (contents : List Bool) (j : ℕ) (hj : 1 ≤ j) : (init (List.map Γ.ofBool contents)).cells j ≠ Γ.start

No positive-indexed cell of a Boolean-initialized tape contains the left-end marker.

@[simp]

theorem Complexity.Tape.init_nil_move_right_read : ((init []).move Dir3.right).read = Γ.blank

Moving an empty initialized tape to cell one reads blank.

theorem Complexity.Tape.init_ofBool_move_right_read_ne_start (contents : List Bool) : ((init (List.map Γ.ofBool contents)).move Dir3.right).read ≠ Γ.start

A Boolean-initialized tape moved to its first data cell never reads the left-end marker.

theorem Complexity.Tape.StartInvariant.init (xs : List Γ) (hxs : ∀ a ∈ xs, a ≠ Γ.start) : (Tape.init xs).StartInvariant

An initialized tape whose contents avoid ▷ satisfies the invariant.

theorem Complexity.Tape.StartInvariant.init_ofBool (xs : List Bool) : (Tape.init (List.map Γ.ofBool xs)).StartInvariant

A Boolean-initialized tape satisfies the invariant.

theorem Complexity.Tape.StartInvariant.init_nil : (Tape.init []).StartInvariant

The empty initialized tape satisfies the invariant.

theorem Complexity.Tape.init_nil_move_right_cells_ne_start (j : ℕ) (hj : j ≥ 1) : ((init []).move Dir3.right).cells j ≠ Γ.start

After stepping onto cell 1 of an empty initialized tape, no positive cell holds the left-end marker.

theorem Complexity.Tape.init_ofBool_move_right_cells_ne_start (contents : List Bool) (j : ℕ) : 1 ≤ j → ((init (List.map Γ.ofBool contents)).move Dir3.right).cells j ≠ Γ.start

Moving the head does not introduce a left-end marker in the positive cells of a Boolean-initialized tape.

@[reducible, inline]

abbrev Complexity.Language : Type

A language is a set of binary strings.

Equations

• Complexity.Language = Set (List Bool)

structure Complexity.Cfg (n : ℕ) (Q : Type) : Type

A configuration of a Turing machine with n work tapes: a read-only input tape, n read-write work tapes, and a read-write output tape.

• state : Q

  The current machine state.

• input : Tape

  The read-only input tape.

• work : Fin n → Tape

  The n read-write work tapes.

• output : Tape

  The read-write output tape.

@[reducible, inline]

abbrev Complexity.Cfg.init {Q : Type} {n : ℕ} (qstart : Q) (x : List Bool) : Cfg n Q

Initial configuration for any TM: input on the input tape, all tapes start with ▷.

Equations

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

@[reducible, inline]

abbrev Complexity.Cfg.isHalted {Q : Type} {n : ℕ} (qhalt : Q) (c : Cfg n Q) : Prop

A configuration is halted when its state equals the halt state.

Equations

• Complexity.Cfg.isHalted qhalt c = (c.state = qhalt)

def Complexity.Cfg.WithinAuxSpace {n : ℕ} {Q : Type} (c : Cfg n Q) (inputLength space : ℕ) : Prop

The auxiliary-space bound for a configuration on an input of length inputLength. Work-tape cells through space are available, while the input itself and its first trailing blank are free; travel farther into the input tape's blank tail is charged against space.

This predicate deliberately omits the output tape. It is suitable for function computation only when the machine also satisfies the one-way output discipline TM.IsTransducer.

Equations

• c.WithinAuxSpace inputLength space = ((∀ (i : Fin n), (c.work i).head ≤ space) ∧ c.input.head ≤ inputLength + space + 1)

def Complexity.Cfg.WithinDecisionSpace {n : ℕ} {Q : Type} (c : Cfg n Q) (inputLength space : ℕ) : Prop

The space bound for a language-decider configuration. In addition to WithinAuxSpace, the output head is bounded by space + 1: cell 1 is the free verdict cell, and any farther two-way output-tape travel is charged.

Equations

• c.WithinDecisionSpace inputLength space = (c.WithinAuxSpace inputLength space ∧ c.output.head ≤ space + 1)

structure Complexity.TM (n : ℕ) : Type 1

A deterministic Turing machine with n work tapes.

The machine has a read-only input tape, n read-write work tapes, and a read-write output tape. The transition function reads Γ from all tape heads but writes only Γw (excluding ▷) to work and output tapes. Q is finite.

• Q : Type

  The (finite) type of machine states.

• decEq : DecidableEq self.Q
• finQ : Fintype self.Q
• qstart : self.Q

  The designated start state.

• qhalt : self.Q

  The designated halt state.

• δ : self.Q → Γ → (Fin n → Γ) → Γ → self.Q × (Fin n → Γw) × Γw × Dir3 × (Fin n → Dir3) × Dir3

  The transition function: from the current state and the symbols under the input, work, and output heads, produce the next state, the symbols to write on the work and output tapes, and a direction for every head.

• δ_right_of_start (q : self.Q) (iHead : Γ) (wHeads : Fin n → Γ) (oHead : Γ) : match self.δ q iHead wHeads oHead with | (fst, fst_1, fst_2, inDir, workDirs, outDir) => (iHead = Γ.start → inDir = Dir3.right) ∧ (∀ (i : Fin n), wHeads i = Γ.start → workDirs i = Dir3.right) ∧ (oHead = Γ.start → outDir = Dir3.right)

  Reading the left-end marker forces that head to move right, so no head ever falls off the left edge.

structure Complexity.NTM (n : ℕ) : Type 1

A nondeterministic Turing machine with two transition functions.

The same structure is used for probabilistic TMs — only the acceptance criterion differs (existential for NTM, counting for PTM). Q is finite.

• Q : Type

  The (finite) type of machine states.

• decEq : DecidableEq self.Q
• finQ : Fintype self.Q
• qstart : self.Q

  The designated start state.

• qhalt : self.Q

  The designated halt state.

• δ : Bool → self.Q → Γ → (Fin n → Γ) → Γ → self.Q × (Fin n → Γw) × Γw × Dir3 × (Fin n → Dir3) × Dir3

  The two transition functions, selected by the Bool choice bit; each has the same shape as the deterministic TM.δ.

• δ_right_of_start (b : Bool) (q : self.Q) (iHead : Γ) (wHeads : Fin n → Γ) (oHead : Γ) : match self.δ b q iHead wHeads oHead with | (fst, fst_1, fst_2, inDir, workDirs, outDir) => (iHead = Γ.start → inDir = Dir3.right) ∧ (∀ (i : Fin n), wHeads i = Γ.start → workDirs i = Dir3.right) ∧ (oHead = Γ.start → outDir = Dir3.right)

  Reading the left-end marker forces that head to move right, on both branches.

def Complexity.TM.step {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : Option (Cfg n tm.Q)

Step a deterministic TM by one step. Returns none if halted.

Equations

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

@[reducible, inline]

abbrev Complexity.TM.initCfg {n : ℕ} (tm : TM n) (x : List Bool) : Cfg n tm.Q

Initial configuration: input on the input tape, all tapes start with ▷.

Equations

• tm.initCfg x = Complexity.Cfg.init tm.qstart x

@[reducible, inline]

abbrev Complexity.TM.halted {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : Prop

A configuration is halted when its state is qhalt.

Equations

• tm.halted c = Complexity.Cfg.isHalted tm.qhalt c

theorem Complexity.TM.state_ne_qhalt_of_step {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} (h : tm.step c = some c') : c.state ≠ tm.qhalt

If step returns some, the machine was not halted.

def Complexity.TM.stepRel {n : ℕ} (tm : TM n) (c c' : Cfg n tm.Q) : Prop

One-step relation for a deterministic TM.

Equations

• tm.stepRel c c' = (tm.step c = some c')

def Complexity.TM.reaches {n : ℕ} (tm : TM n) : Cfg n tm.Q → Cfg n tm.Q → Prop

Reflexive-transitive closure of the step relation.

Equations

• tm.reaches = Relation.ReflTransGen tm.stepRel

inductive Complexity.TM.reachesIn {n : ℕ} (tm : TM n) : ℕ → Cfg n tm.Q → Cfg n tm.Q → Prop

Reachability in exactly t steps.

• zero {n : ℕ} {tm : TM n} {c : Cfg n tm.Q} : tm.reachesIn 0 c c
• step {n : ℕ} {tm : TM n} {c c'' : Cfg n tm.Q} {t : ℕ} {c' : Cfg n tm.Q} : tm.step c = some c'' → tm.reachesIn t c'' c' → tm.reachesIn (t + 1) c c'

def Complexity.TM.Accepts {n : ℕ} (tm : TM n) (x : List Bool) : Prop

DTM accepts x: reaches qhalt with output cell 1 (after ▷) = 1.

Equations

• tm.Accepts x = ∃ (c' : Complexity.Cfg n tm.Q), tm.reaches (tm.initCfg x) c' ∧ tm.halted c' ∧ c'.output.cells 1 = Complexity.Γ.one

def Complexity.TM.AcceptsInTime {n : ℕ} (tm : TM n) (x : List Bool) (T : ℕ) : Prop

DTM accepts x within T steps.

Equations

• tm.AcceptsInTime x T = ∃ (c' : Complexity.Cfg n tm.Q), ∃ t ≤ T, tm.reachesIn t (tm.initCfg x) c' ∧ tm.halted c' ∧ c'.output.cells 1 = Complexity.Γ.one

def Complexity.TM.DecidesInTime {n : ℕ} (tm : TM n) (L : Language) (T : ℕ → ℕ) : Prop

DTM decides L within time bound T(n): halts on all inputs within T(|x|) steps, outputting 1 for x ∈ L and 0 for x ∉ L.

Equations

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

def Complexity.TM.ComputesInTime {n : ℕ} (tm : TM n) (f : List Bool → List Bool) (T : ℕ → ℕ) : Prop

DTM computes function f in time T(n): for every input x, the machine halts within T(|x|) steps with f(x) written on the output tape.

Equations

• tm.ComputesInTime f T = ∀ (x : List Bool), ∃ (c' : Complexity.Cfg n tm.Q), ∃ t ≤ T x.length, tm.reachesIn t (tm.initCfg x) c' ∧ tm.halted c' ∧ c'.output.HasOutput (f x)

def Complexity.TM.Computes {n : ℕ} (tm : TM n) (f : List Bool → List Bool) : Prop

DTM computes function f (existential version of ComputesInTime).

Equations

• tm.Computes f = ∃ (T : ℕ → ℕ), tm.ComputesInTime f T

def Complexity.TM.DecidesInSpace {n : ℕ} (tm : TM n) (L : Language) (S : ℕ → ℕ) : Prop

DTM decides L using at most S(|x|) auxiliary space. Every reachable configuration has work heads at position at most S(|x|), input head at position at most |x| + S(|x|) + 1, and output head at position at most S(|x|) + 1. Thus the input region, its first trailing blank, and output verdict cell 1 are free, but neither infinite tape can become uncharged two-way workspace. The machine halts on all inputs with correct output.

Equations

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

def Complexity.TM.DecidesInTimeSpace {n : ℕ} (tm : TM n) (L : Language) (T S : ℕ → ℕ) : Prop

DTM decides L within time T(|x|) and space S(|x|) simultaneously: a single machine halts in bounded time with correct output, and every reachable configuration satisfies the honest auxiliary-space convention of Cfg.WithinDecisionSpace.

Equations

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

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

The output tape head never moves left — the machine is a transducer. This prevents earlier output from being reread as workspace while allowing unbounded output length. ComputesInSpace requires this discipline; the decision-space predicates separately bound two-way output-head travel.

Equations

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

def Complexity.TM.ComputesInSpace {n : ℕ} (tm : TM n) (f : List Bool → List Bool) (S : ℕ → ℕ) : Prop

DTM computes function f using at most S(|x|) auxiliary space. Work-tape travel and input-head travel beyond the input's first trailing blank are bounded by Cfg.WithinAuxSpace. The output length is not bounded: instead, IsTransducer makes the output one-way so it cannot serve as read-write workspace.

Equations

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

theorem Complexity.TM.reachesIn_trans {n : ℕ} (tm : TM n) {t₁ t₂ : ℕ} {c₁ c₂ c₃ : Cfg n tm.Q} (h₁ : tm.reachesIn t₁ c₁ c₂) (h₂ : tm.reachesIn t₂ c₂ c₃) : tm.reachesIn (t₁ + t₂) c₁ c₃

Transitivity: if c₁ reaches c₂ in t₁ steps and c₂ reaches c₃ in t₂ steps, then c₁ reaches c₃ in t₁ + t₂ steps.

theorem Complexity.TM.reaches_of_reachesIn {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} (h : tm.reachesIn t c c') : tm.reaches c c'

Bounded reachability implies unbounded reachability.

theorem Complexity.TM.accepts_of_acceptsInTime {n : ℕ} {tm : TM n} {x : List Bool} {T : ℕ} (h : tm.AcceptsInTime x T) : tm.Accepts x

AcceptsInTime implies Accepts — forget the time bound.

theorem Complexity.TM.AcceptsInTime.mono {n : ℕ} {tm : TM n} {x : List Bool} {T T' : ℕ} (hle : T ≤ T') (h : tm.AcceptsInTime x T) : tm.AcceptsInTime x T'

DTM acceptance is monotone in the time bound.

theorem Complexity.TM.DecidesInTime.mono {n : ℕ} {tm : TM n} {L : Language} {T T' : ℕ → ℕ} (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.DecidesInTime L T) : tm.DecidesInTime L T'

DTM decision is monotone under pointwise enlargement of the time bound.

theorem Complexity.TM.ComputesInTime.mono {n : ℕ} {tm : TM n} {f : List Bool → List Bool} {T T' : ℕ → ℕ} (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.ComputesInTime f T) : tm.ComputesInTime f T'

DTM computation is monotone under pointwise enlargement of the time bound.

def Complexity.NTM.trace {n : ℕ} (tm : NTM n) (T : ℕ) : (Fin T → Bool) → Cfg n tm.Q → Cfg n tm.Q

Execute an NTM for T steps with a fixed choice sequence. Stops early if the machine reaches qhalt.

Equations

• One or more equations did not get rendered due to their size.
• tm.trace 0 x_3 x✝ = x✝

@[reducible, inline]

abbrev Complexity.NTM.initCfg {n : ℕ} (tm : NTM n) (x : List Bool) : Cfg n tm.Q

Initial configuration: input on the input tape, all tapes start with ▷.

Equations

• tm.initCfg x = Complexity.Cfg.init tm.qstart x

@[reducible, inline]

abbrev Complexity.NTM.halted {n : ℕ} (tm : NTM n) (c : Cfg n tm.Q) : Prop

A configuration is halted when its state is qhalt.

Equations

• tm.halted c = Complexity.Cfg.isHalted tm.qhalt c

theorem Complexity.NTM.trace_halted {n : ℕ} (tm : NTM n) {c : Cfg n tm.Q} (T : ℕ) (choices : Fin T → Bool) (h : tm.halted c) : tm.trace T choices c = c

Once halted, the NTM trace stays at the same configuration regardless of the remaining choices.

def Complexity.NTM.Accepts {n : ℕ} (tm : NTM n) (x : List Bool) : Prop

NTM accepts x: there exists a time bound and choice sequence leading to qhalt with output cell 1 = 1.

Equations

• tm.Accepts x = ∃ (T : ℕ) (choices : Fin T → Bool), have c' := tm.trace T choices (tm.initCfg x); tm.halted c' ∧ c'.output.cells 1 = Complexity.Γ.one

def Complexity.NTM.AcceptsInTime {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : Prop

NTM accepts x within T steps: there exists a choice sequence of length T leading to qhalt with output cell 1 = 1.

Equations

• tm.AcceptsInTime x T = ∃ (choices : Fin T → Bool), have c' := tm.trace T choices (tm.initCfg x); tm.halted c' ∧ c'.output.cells 1 = Complexity.Γ.one

theorem Complexity.NTM.accepts_of_acceptsInTime {n : ℕ} {tm : NTM n} {x : List Bool} {T : ℕ} (h : tm.AcceptsInTime x T) : tm.Accepts x

AcceptsInTime implies Accepts — package the time bound existentially.

theorem Complexity.NTM.accepts_iff_exists_acceptsInTime {n : ℕ} {tm : NTM n} {x : List Bool} : tm.Accepts x ↔ ∃ (T : ℕ), tm.AcceptsInTime x T

Accepts is exactly ∃ T, AcceptsInTime x T.

theorem Complexity.NTM.trace_mono {n : ℕ} (tm : NTM n) {T T' : ℕ} (hle : T ≤ T') {choices : Fin T → Bool} {choices' : Fin T' → Bool} {c : Cfg n tm.Q} (hagree : ∀ (i : Fin T), choices' ⟨↑i, ⋯⟩ = choices i) (h : tm.halted (tm.trace T choices c)) : tm.trace T' choices' c = tm.trace T choices c

Running the NTM trace for more steps preserves the final configuration: if the machine halts within T steps and the extended choice sequence agrees with the original on the first T positions, the extra steps are no-ops.

theorem Complexity.NTM.AcceptsInTime.mono {n : ℕ} {tm : NTM n} {x : List Bool} {T T' : ℕ} (hle : T ≤ T') (h : tm.AcceptsInTime x T) : tm.AcceptsInTime x T'

NTM acceptance is monotone in the time bound: AcceptsInTime x T implies AcceptsInTime x T' for any T' ≥ T. Extra steps are no-ops once halted.

def Complexity.NTM.AllPathsHaltIn {n : ℕ} (tm : NTM n) (T : ℕ → ℕ) : Prop

All computation paths of the NTM halt within T(|x|) steps, for every input x and every choice sequence. This is the core time-boundedness condition shared by DecidesInTime, BPTIME, and NTM.IsPPT.

Equations

• tm.AllPathsHaltIn T = ∀ (x : List Bool) (choices : Fin (T x.length) → Bool), tm.halted (tm.trace (T x.length) choices (tm.initCfg x))

def Complexity.NTM.DecidesInTime {n : ℕ} (tm : NTM n) (L : Language) (T : ℕ → ℕ) : Prop

NTM decides L within time bound T(n): all computation paths halt within T(|x|) steps, and accepting paths exist iff x ∈ L (AB Definition 2.1).

Equations

• tm.DecidesInTime L T = (tm.AllPathsHaltIn T ∧ ∀ (x : List Bool), x ∈ L ↔ tm.AcceptsInTime x (T x.length))

theorem Complexity.NTM.AllPathsHaltIn.mono {n : ℕ} {tm : NTM n} {T T' : ℕ → ℕ} (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.AllPathsHaltIn T) : tm.AllPathsHaltIn T'

All-paths halting is monotone in the time bound: once halted, the extra steps are no-ops.

theorem Complexity.NTM.acceptsInTime_of_le_of_allPathsHaltIn {n : ℕ} {tm : NTM n} {T T' : ℕ → ℕ} {x : List Bool} (hle : ∀ (m : ℕ), T m ≤ T' m) (hN : tm.AllPathsHaltIn T) (h : tm.AcceptsInTime x (T' x.length)) : tm.AcceptsInTime x (T x.length)

With all paths halting within T, timed acceptance transfers DOWN from any pointwise-larger bound: by T(|x|) every path is already frozen.

theorem Complexity.NTM.DecidesInTime.mono {n : ℕ} {tm : NTM n} {L : Language} {T T' : ℕ → ℕ} (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.DecidesInTime L T) : tm.DecidesInTime L T'

Deciding within T transfers to any pointwise-larger bound T': halting is monotone, and acceptance transfers both ways (up by monotonicity, down by the all-paths-halt freeze).

noncomputable def Complexity.NTM.acceptCount {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : ℕ

Count of accepting choice sequences of length T.

Meaningful when the machine halts on all paths within T steps — use in conjunction with NTM.DecidesInTime or an explicit all-paths-halt hypothesis.

Equations

• tm.acceptCount x T = {choices : Fin T → Bool | have c' := tm.trace T choices (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Complexity.Γ.one}.card

noncomputable def Complexity.NTM.acceptProb {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : ℚ

Acceptance probability = |accepting paths| / 2^T.

Meaningful when the machine halts on all paths within T steps.

Equations

• tm.acceptProb x T = ↑(tm.acceptCount x T) / 2 ^ T

noncomputable def Complexity.NTM.outputCount {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) (y : List Bool) : ℕ

Count of choice sequences of length T on which the machine halts with output y (using Tape.HasOutput).

Meaningful when the machine halts on all paths within T steps.

Equations

• tm.outputCount x T y = {choices : Fin T → Bool | have c' := tm.trace T choices (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.HasOutput y}.card

noncomputable def Complexity.NTM.outputProb {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) (y : List Bool) : ℚ

Probability that the machine outputs y on input x = |output-matching paths| / 2^T.

Meaningful when the machine halts on all paths within T steps. This generalizes acceptProb from accept/reject to arbitrary output strings, as needed for cryptographic definitions.

Equations

• tm.outputProb x T y = ↑(tm.outputCount x T y) / 2 ^ T

def Complexity.NTM.DecidesInSpace {n : ℕ} (tm : NTM n) (L : Language) (S : ℕ → ℕ) : Prop

NTM decides L using at most S(|x|) auxiliary space. Every intermediate configuration on every path obeys Cfg.WithinDecisionSpace: work heads are bounded by S, the finite input plus first blank is free but farther input travel is charged, and only output verdict cell 1 is free. There exists a time bound within which all paths halt and decide correctly.

Equations

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

def Complexity.NTM.IsTransducer {n : ℕ} (tm : NTM n) : Prop

The output tape head never moves left — the machine is a transducer. This prevents earlier output from being reread as workspace while allowing unbounded output length. Decision-space predicates separately bound two-way output-head travel.

Equations

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

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

Embed a DTM into an NTM by using the same transition for both choices.

Equations

• tm.toNTM = { Q := tm.Q, decEq := tm.decEq, finQ := tm.finQ, qstart := tm.qstart, qhalt := tm.qhalt, δ := fun (x : Bool) => tm.δ, δ_right_of_start := ⋯ }