Codes for multi-tape Turing machines

DefinitionDecoding a Turing machine head move#✓fully proved

Decode a head move: 0 moves left, 1 stays, anything else moves right.

def decodeMove (m : ℕ) : SignType :=
  if m = 0 then -1 else if m = 1 then 0 else 1
Used by 3
Used byThe evaluator simulates the machine step for step · Decoding a coded action · Decoding the coding of an action

StructureCoded actions#✓fully proved

A coded action for a machine with \(k\) work tapes consists of a coded input-head move; for each of the \(k\) work tapes, an optional symbol to write, the symbol being a bit or the blank (so a blank can be written), together with a coded head move; an optional output bit; and an optional next state in \(\mathbb{N}\), where no next state means halting. A head move is coded by a natural number: \(0\) moves left, \(1\) stays, and any other number moves right.

structure CodeAction (k : ℕ) where
  /-- The coded input-head move. -/
  inputMove : ℕ
  /-- For each work tape: an optional symbol to write and the coded head move. -/
  work : Fin k → Option (Option Bool) × ℕ
  /-- An optional output bit. -/
  out : Option Bool
  /-- The next state, `none` to halt. -/
  next : Option ℕ
Used by 24
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Action of a code at a key · The code of a machine takes its coded actions · Applying a coded action · Codes for multi-tape machines · Decoding numbers to codes · Code round-trip · Numeric coding of codes · Coding an action · Injectivity of the numeric coding of codes · Coded actions as tuples · Multi-tape codes as tables · Halting action · The code of a machine simulates it · Next states of a code lie in its state set · The code of a finite-state binary machine · The evaluator is primitive recursive · Codes denote finite-state machines · States of a multi-tape code · The evaluator simulates the machine step for step · Decoding a coded action · Decoding the coding of an action

DefinitionCoded actions as tuples#✓fully proved

The bijection between coded actions and tuples \((m, w, b, q)\) that sends an action to its coded input head move \(m \in \mathbb{N}\), its work tape instructions \(w\) (for each of the \(k\) work tapes, an optional symbol to write and a coded head move), its optional output bit \(b\) and its optional next state \(q\).

def equivProd :
    CodeAction k ≃ ℕ × (Fin k → Option (Option Bool) × ℕ) × Option Bool × Option ℕ where
  toFun a := (a.inputMove, a.work, a.out, a.next)
  invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
Uses 1 · Used by 8
Statement usesCoded actions
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Decoding numbers to codes · Code round-trip · Numeric coding of codes · Injectivity of the numeric coding of codes · The evaluator is primitive recursive

DefinitionDecoding a coded action#✓fully proved

A coded action \(a\) stands for the action of CSLib's multi-tape model that moves the input head by the decoded input move of \(a\), on each work tape writes the optional symbol that \(a\) gives for that tape and moves its head by the decoded move, emits the optional output bit of \(a\), and enters the next state of \(a\) (halting when there is none).

def toAction (a : CodeAction k) : Action k Bool ℕ where
  inputTape := decodeMove a.inputMove
  workTapes i := ((a.work i).1, decodeMove (a.work i).2)
  output := a.out
  state := a.next
Uses 2 · Used by 4
Statement usesCoded actions · Decoding a Turing machine head move
Used byThe code of a machine simulates it · The evaluator simulates the machine step for step · Decoding the coding of an action · Transition function of a code

DefinitionHalting action#✓fully proved

The default action of a missing table entry: halt without moving any head, writing any symbol or emitting an output bit.

def halt : CodeAction k := ⟨1, fun _ ↦ (none, 1), none, none⟩
Uses 1 · Used by 4
Statement usesCoded actions
Used byAction of a code at a key · The code of a machine takes its coded actions · Next states of a code lie in its state set · The evaluator is primitive recursive

AbbreviationKeys of a code's table#✓fully proved

A key of a table entry for a machine with \(k\) work tapes is a triple \((q, a, w)\) of a state \(q \in \mathbb{N}\), the symbol \(a\) under the input head and the symbols \(w = (w_i)_{i < k}\) under the \(k\) work heads, where each symbol is a bit or the blank.

abbrev CodeKey (k : ℕ) := ℕ × Option Bool × (Fin k → Option Bool)
Used by 16
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Action of a code at a key · The code of a machine takes its coded actions · Codes for multi-tape machines · Decoding numbers to codes · Code round-trip · Numeric coding of codes · Injectivity of the numeric coding of codes · Multi-tape codes as tables · Next states of a code lie in its state set · The code of a finite-state binary machine · The evaluator is primitive recursive · Codes denote finite-state machines · States of a multi-tape code

StructureCodes for multi-tape machines#✓fully proved

A code for a machine with \(k\) work tapes over the binary alphabet, with states in \(\mathbb{N}\), is a finite list of table entries, each a key (a state together with the symbols under the input head and the \(k\) work heads) paired with a coded action. The table is looked up by key, the first matching entry wins, and a missing key halts the machine.

structure Code (k : ℕ) where
  /-- The table entries. -/
  table : List (CodeKey k × CodeAction k)
Uses 2 · Used by 38
Statement usesCoded actions · Keys of a code's table
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Action of a code at a key · The code of a machine takes its coded actions · Computation by a code is finite-state computation · Computability over codes · A code computes exactly what its clocked evaluator returns · Deciding by a code is finite-state decidability · Decidability over codes · Decoding numbers to codes · Code round-trip · Numeric coding of codes · Injectivity of the numeric coding of codes · Multi-tape codes as tables · Clocked evaluator · Evaluator agreement · Monotonicity of the clocked evaluator for multi-tape codes · Every finite-state machine has a code · Transition function of a code on bounded states · The code of a machine simulates it · A code's machine simulates its finite-state machine · The evaluator returns within the clock exactly when the machine runs in time · DSPACE over codes · DTIME over codes · Next states of a code lie in its state set · The code of a finite-state binary machine · The evaluator is primitive recursive · The evaluator tracks the machine run · State bound of a code · Codes denote finite-state machines · States of a multi-tape code · Evaluator step · The evaluator simulates the machine step for step · Step of the machine of a code · The finite-state machine of a code · The multi-tape machine of a code · Transition function of a code

DefinitionMulti-tape codes as tables#✓fully proved

The bijection between codes for machines with \(k\) work tapes and finite lists of table entries, each a pair of a key and a coded action, that sends a code to its table.

def equivTable : Code k ≃ List (CodeKey k × CodeAction k) where
  toFun := table
  invFun := mk
  left_inv _ := rfl
  right_inv _ := rfl
Uses 3 · Used by 8
Statement usesCodes for multi-tape machines · Coded actions · Keys of a code's table
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Decoding numbers to codes · Code round-trip · Numeric coding of codes · Injectivity of the numeric coding of codes · The evaluator is primitive recursive

DefinitionNumeric coding of codes#✓fully proved

The natural number coding a code \(c\): its encoding under the standard primitive recursive coding of codes, which identifies a code with its table, a list of pairs of a key and a coded action.

def encode (c : Code k) : ℕ := Encodable.encode c
Uses 5 · Used by 2
Statement usesCodes for multi-tape machines · Multi-tape codes as tables · Coded actions · Coded actions as tuples · Keys of a code's table
Used byCode round-trip · Injectivity of the numeric coding of codes

DefinitionDecoding numbers to codes#✓fully proved

The code coded by a natural number \(n\), if any: decoding under the standard primitive recursive coding of codes, which identifies a code with its table, a list of pairs of a key and a coded action. The result is empty when \(n\) codes no code.

def decode (n : ℕ) : Option (Code k) := Encodable.decode n
Uses 5 · Used by 1
Statement usesCodes for multi-tape machines · Multi-tape codes as tables · Coded actions · Coded actions as tuples · Keys of a code's table
Used byCode round-trip

TheoremCode round-trip#✓fully proved

For every code \(c\) with \(k\) work tapes, decoding the natural number \(\operatorname{encode}(c)\) returns \(c\): \(\operatorname{decode}(\operatorname{encode}(c))\) is defined and equals \(c\).

@[simp]
theorem decode_encode (c : Code k) : decode (encode c) = some c
Uses 7
Statement usesCodes for multi-tape machines · Decoding numbers to codes · Numeric coding of codes
Proof usesMulti-tape codes as tables · Coded actions · Coded actions as tuples · Keys of a code's table

TheoremInjectivity of the numeric coding of codes#✓fully proved

If two codes \(c\) and \(c'\) with the same number of work tapes have the same numeric code, then \(c = c'\).

theorem encode_injective : Function.Injective (encode (k := k))
Uses 6
Statement usesCodes for multi-tape machines · Numeric coding of codes
Proof usesMulti-tape codes as tables · Coded actions · Coded actions as tuples · Keys of a code's table

DefinitionAction of a code at a key#✓fully proved

For a code \(c\) with \(k\) work tapes, a state \(q \in \mathbb{N}\), a symbol \(a\) under the input head and symbols \(w = (w_i)_{i < k}\) under the work heads (each symbol a bit or the blank), the action of \(c\) at \((q, a, w)\) is the coded action of the first table entry of \(c\) whose key is \((q, a, w)\), or, if there is no such entry, the halting action, which moves no head, writes and emits nothing, and has no next state.

def act (c : Code k) (q : ℕ) (a : Option Bool) (w : Fin k → Option Bool) : CodeAction k :=
  ((@List.lookup _ _ instBEqOfDecidableEq (q, a, w) c.table)).getD CodeAction.halt
Uses 4 · Used by 7
Statement usesCodes for multi-tape machines · Coded actions · Halting action · Keys of a code's table
Used byThe code of a machine takes its coded actions · The code of a machine simulates it · Next states of a code lie in its state set · The evaluator is primitive recursive · Evaluator step · The evaluator simulates the machine step for step · Transition function of a code

DefinitionTransition function of a code#✓fully proved

The transition function of a code \(c\) sends a state \(q\), the symbol \(a\) under the input head and the symbols \(w\) under the work heads (each a bit or blank) to the action of CSLib's multi-tape model that the coded action of \(c\) at \((q, a, w)\) stands for. That coded action is the one of the first table entry of \(c\) with key \((q, a, w)\), or, if there is none, the one that halts without moving, writing or emitting.

def tr (c : Code k) (q : ℕ) (a : Option Bool) (w : Fin k → Option Bool) : Action k Bool ℕ :=
  (c.act q a w).toAction
Uses 3 · Used by 7
Statement usesCodes for multi-tape machines · Action of a code at a key · Decoding a coded action
Used byTransition function of a code on bounded states · The code of a machine simulates it · A code's machine simulates its finite-state machine · Codes denote finite-state machines · The evaluator simulates the machine step for step · Step of the machine of a code · The multi-tape machine of a code

DefinitionThe multi-tape machine of a code#✓fully proved

The machine of a code \(c\) for \(k\) work tapes is the machine of CSLib's multi-tape model with \(k\) work tapes, the binary alphabet and states in \(\mathbb{N}\) whose initial state is \(0\) and whose transition function is the transition function of \(c\).

noncomputable def toTM (c : Code k) : MultiTapeTM k Bool ℕ := MultiTapeTM.ofTr 0 c.tr
Uses 2 · Used by 20
Statement usesCodes for multi-tape machines · Transition function of a code
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Computation by a code is finite-state computation · Computability over codes · A code computes exactly what its clocked evaluator returns · Deciding by a code is finite-state decidability · Decidability over codes · Evaluator agreement · Monotonicity of the clocked evaluator for multi-tape codes · Every finite-state machine has a code · The code of a machine simulates it · A code's machine simulates its finite-state machine · The evaluator returns within the clock exactly when the machine runs in time · DSPACE over codes · DTIME over codes · The evaluator tracks the machine run · Codes denote finite-state machines · The evaluator simulates the machine step for step · Step of the machine of a code

TheoremStep of the machine of a code#✓fully proved

For a code \(c\), a binary input \(x\) and a configuration \(C\) of the machine of \(c\) on \(x\), the step of the machine of \(c\) sends \(C\) to its successor under the transition function of \(c\): \(C\) itself if it has halted, and otherwise the result of applying to \(C\) the action that the transition function of \(c\) selects for the state of \(C\) and the symbols under its heads.

theorem step_toTM (c : Code k) {x : List Bool} (cfg : Cfg k Bool ℕ x) :
    c.toTM.step cfg = stepWith c.tr cfg
Uses 5 · Used by 2
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · Transition function of a code · Successor under a transition function
Proof usesStep of a machine given by a transition function
Used byCodes denote finite-state machines · The evaluator simulates the machine step for step

DefinitionStates of a multi-tape code#✓fully proved

The states of a code \(c\) for machines with \(k\) work tapes form the finite set of natural numbers consisting of the initial state \(0\) and the next state of every table entry of \(c\) that does not halt.

def states (c : Code k) : Finset ℕ :=
  insert 0 (c.table.filterMap fun e ↦ e.2.next).toFinset
Uses 3 · Used by 5
Statement usesCodes for multi-tape machines · Coded actions · Keys of a code's table
Used byA code's machine simulates its finite-state machine · Next states of a code lie in its state set · State bound of a code · Codes denote finite-state machines · The finite-state machine of a code

TheoremNext states of a code lie in its state set#✓fully proved

For a code \(c\), a state \(q\), an input symbol \(a\) and work tape symbols \(w\), if the action of \(c\) at \((q, a, w)\) has a next state \(q'\) (rather than halting), then \(q'\) belongs to the set of states of \(c\).

theorem next_act_mem_states (c : Code k) {q q' : ℕ} {a : Option Bool} {w : Fin k → Option Bool}
    (h : (c.act q a w).next = some q') : q' ∈ c.states
Uses 6 · Used by 2
Statement usesCodes for multi-tape machines · Action of a code at a key · States of a multi-tape code · Coded actions
Proof usesHalting action · Keys of a code's table
Used byA code's machine simulates its finite-state machine · Codes denote finite-state machines

TheoremCodes denote finite-state machines#✓fully proved

Let \(c\) be a code for a machine with \(k\) work tapes. For every binary input \(x\) and every number of steps \(t\), if the machine of \(c\), run for \(t\) steps from its initial configuration on \(x\), has not halted and is in state \(q\), then \(q\) lies in the finite set of states of \(c\).

theorem state_runFrom_mem_states (c : Code k) (x : List Bool) (t : ℕ) {q : ℕ}
    (h : (c.toTM.runFrom (c.toTM.initCfg x) t).state = some q) : q ∈ c.states
Uses 9
Statement usesCodes for multi-tape machines · States of a multi-tape code · The multi-tape machine of a code
Proof usesNext states of a code lie in its state set · Step of the machine of a code · Transition function of a code · Coded actions · Keys of a code's table · Successor under a transition function

AbbreviationWork tapes as zippers#✓fully proved

A work tape is a pair of finite lists of cells, each cell a bit or blank: the cells left of the head, nearest first, and the cells from the head rightwards; cells beyond both lists are blank.

abbrev Tape := List (Option Bool) × List (Option Bool)
Used by 13
Used byApplying a coded action · Cell of a zipper tape · Explicit configurations of the code evaluator · Explicit configurations as tuples · Initial configuration of the clocked evaluator · Moving the head of a zipper tape · The evaluator is primitive recursive · Symbol under the head of a zipper tape · Explicit configurations representing machine configurations · The evaluator tracks the machine run · Evaluator step · The evaluator simulates the machine step for step · Writing on a zipper tape

DefinitionSymbol under the head of a zipper tape#✓fully proved

The symbol read from a work tape given as a zipper \((l, r)\) is the first cell of \(r\), or the blank if \(r\) is empty.

def read (t : Tape) : Option Bool := t.2.headI
Uses 1 · Used by 3
Statement usesWork tapes as zippers
Used byThe evaluator is primitive recursive · Evaluator step · The evaluator simulates the machine step for step

DefinitionWriting on a zipper tape#✓fully proved

Writing an optional symbol on a work tape leaves the tape unchanged when no symbol is given; given a symbol \(s\) (a bit or blank), it replaces the cell under the head by \(s\) and keeps all other cells.

def write : Option (Option Bool) → Tape → Tape
  | none, t => t
  | some s, t => (t.1, s :: t.2.tail)
Uses 1 · Used by 3
Statement usesWork tapes as zippers
Used byApplying a coded action · The evaluator is primitive recursive · The evaluator simulates the machine step for step

DefinitionMoving the head of a zipper tape#✓fully proved

For a coded move \(m\) and a work tape given as a zipper \((l, r)\): if \(m = 0\) the head moves one cell left, removing the first cell of \(l\) (the blank if \(l\) is empty) and putting it in front of \(r\); if \(m = 1\) the tape is unchanged; otherwise the head moves one cell right, removing the first cell of \(r\) (the blank if \(r\) is empty) and putting it in front of \(l\).

def move (m : ℕ) (t : Tape) : Tape :=
  if m = 0 then (t.1.tail, t.1.headI :: t.2)
  else if m = 1 then t
  else (t.2.headI :: t.1, t.2.tail)
Uses 1 · Used by 3
Statement usesWork tapes as zippers
Used byApplying a coded action · The evaluator is primitive recursive · The evaluator simulates the machine step for step

DefinitionCell of a zipper tape#✓fully proved

For a work tape \(t\) in zipper form and an integer \(j\), the cell of \(t\) at \(j\) is the symbol at offset \(j\) from the head: for \(j = n \ge 0\) it is entry \(n\) (counting from \(0\)) of the list of cells from the head rightwards, and for \(j = -(n + 1)\) it is entry \(n\) of the list of cells left of the head, nearest first; in either case it is the blank when the list has no entry \(n\).

def cell (t : Tape) : ℤ → Option Bool
  | .ofNat n => t.2.getD n none
  | .negSucc n => t.1.getD n none
Uses 1 · Used by 3
Statement usesWork tapes as zippers
Used byExplicit configurations representing machine configurations · The evaluator tracks the machine run · The evaluator simulates the machine step for step

StructureExplicit configurations of the code evaluator#✓fully proved

An explicit configuration for a machine with \(k\) work tapes consists of an optional state in \(\mathbb{N}\) (none when the machine has halted); the input head position, a natural number shifted by one, so that position \(0\) is the cell left of the input; the \(k\) work tapes, each a zipper (the cells left of the head, nearest first, and the cells from the head rightwards, all further cells blank); and the output written so far, a binary word.

structure Config (k : ℕ) where
  /-- The state, `none` when halted. -/
  state : Option ℕ
  /-- The input head position, shifted by one. -/
  inputPos : ℕ
  /-- The work tapes. -/
  tapes : Fin k → Tape
  /-- The output so far. -/
  output : List Bool
Uses 1 · Used by 10
Statement usesWork tapes as zippers
Used byApplying a coded action · Explicit configurations as tuples · Clocked evaluator · Evaluator agreement · Initial configuration of the clocked evaluator · The evaluator is primitive recursive · Explicit configurations representing machine configurations · The evaluator tracks the machine run · Evaluator step · The evaluator simulates the machine step for step

DefinitionExplicit configurations as tuples#✓fully proved

The bijection between explicit configurations and tuples \((q, p, t, o)\) that sends a configuration to its optional state \(q\) (empty when halted), its shifted input head position \(p \in \mathbb{N}\), its family \(t\) of \(k\) work tapes (each a zipper) and its output \(o\) so far, a list of bits.

def equivProd : Config k ≃ Option ℕ × ℕ × (Fin k → Tape) × List Bool where
  toFun e := (e.state, e.inputPos, e.tapes, e.output)
  invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
Uses 2 · Used by 1
Statement usesExplicit configurations of the code evaluator · Work tapes as zippers
Used byThe evaluator is primitive recursive

DefinitionInitial configuration of the clocked evaluator#✓fully proved

The initial explicit configuration has state \(0\), the input head on the first input cell (position \(1\), positions being shifted by one), every work tape blank (both halves of its zipper empty), and empty output.

def init : Config k := ⟨some 0, 1, fun _ ↦ ([], []), []⟩
Uses 2 · Used by 4
Statement usesExplicit configurations of the code evaluator · Work tapes as zippers
Used byClocked evaluator · Evaluator agreement · The evaluator is primitive recursive · The evaluator tracks the machine run

DefinitionInput symbol under the input head#✓fully proved

For an input \(x\) and a shifted input head position \(p\), the input symbol is the blank if \(p = 0\); otherwise it is the entry of \(x\) at index \(p - 1\) (counting from \(0\)) if \(p - 1 < |x|\), and the blank if \(p - 1 \ge |x|\).

def inputSym (x : List Bool) (p : ℕ) : Option Bool := if p = 0 then none else x[p - 1]?
Used by 3
Used byThe evaluator is primitive recursive · Evaluator step · The evaluator simulates the machine step for step

DefinitionInput head move of the clocked evaluator#✓fully proved

For an input of length \(n\), a shifted input head position \(p\) and a coded move \(m\), the new position is \(p - 1\) (truncated at \(0\)) if \(m = 0\), \(p\) if \(m = 1\), and \(\min(p + 1, n + 1)\) otherwise, so a move right never passes position \(n + 1\), one cell beyond the input.

def moveInput (n p m : ℕ) : ℕ := if m = 0 then p - 1 else if m = 1 then p else min (p + 1) (n + 1)
Used by 3
Used byApplying a coded action · The evaluator is primitive recursive · The evaluator simulates the machine step for step

DefinitionApplying a coded action#✓fully proved

Given an input word \(x\), a coded action \(a\) and an explicit configuration \(e\), applying \(a\) to \(e\) gives the configuration whose state is the next state of \(a\); whose input head position is that of \(e\), say \(p\), moved by the coded input move of \(a\), where a left move gives \(p - 1\) (truncated at \(0\)), staying gives \(p\), and a right move gives \(\min(p + 1, |x| + 1)\); whose work tape \(i\) is work tape \(i\) of \(e\) after writing the optional symbol of \(a\) for tape \(i\) under the head and then moving the head by the coded move of \(a\) for tape \(i\); and whose output is the output of \(e\) followed by the output bit of \(a\), if any.

def apply (x : List Bool) (a : CodeAction k) (e : Config k) : Config k where
  state := a.next
  inputPos := moveInput x.length e.inputPos a.inputMove
  tapes i := Tape.move (a.work i).2 (Tape.write (a.work i).1 (e.tapes i))
  output := e.output ++ a.out.toList
Uses 6 · Used by 3
Statement usesExplicit configurations of the code evaluator · Input head move of the clocked evaluator · Work tapes as zippers · Moving the head of a zipper tape · Writing on a zipper tape · Coded actions
Used byThe evaluator is primitive recursive · Evaluator step · The evaluator simulates the machine step for step

DefinitionEvaluator step#✓fully proved

One step of the evaluator for a code \(c\) on a binary input \(x\) leaves an explicit configuration \(e\) unchanged if \(e\) has halted; if \(e\) is in state \(q\), it applies to \(e\) the coded action of \(c\) at \(q\), the input symbol at the input head position of \(e\) and the symbols under the heads of the work tapes of \(e\).

def step (c : Code k) (x : List Bool) (e : Config k) : Config k :=
  match e.state with
  | none => e
  | some q => e.apply x (c.act q (inputSym x e.inputPos) fun i ↦ (e.tapes i).read)
Uses 7 · Used by 5
Statement usesCodes for multi-tape machines · Explicit configurations of the code evaluator · Applying a coded action · Input symbol under the input head · Work tapes as zippers · Symbol under the head of a zipper tape · Action of a code at a key
Used byClocked evaluator · Evaluator agreement · The evaluator is primitive recursive · The evaluator tracks the machine run · The evaluator simulates the machine step for step

DefinitionClocked evaluator#✓fully proved

The clocked evaluator runs a code \(c\) on a binary input \(x\) for \(T\) steps: it applies the evaluator's step \(T\) times to the initial explicit configuration. If the resulting configuration is halted, it returns that configuration's output; otherwise it returns no result.

def evalSteps (c : Code k) (x : List Bool) (T : ℕ) : Option (List Bool) :=
  match ((Config.step c x)^[T] Config.init).state with
  | none => some ((Config.step c x)^[T] Config.init).output
  | some _ => none
Uses 4 · Used by 8
Statement usesCodes for multi-tape machines · Explicit configurations of the code evaluator · Initial configuration of the clocked evaluator · Evaluator step
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · A code computes exactly what its clocked evaluator returns · Evaluator agreement · Monotonicity of the clocked evaluator for multi-tape codes · The evaluator returns within the clock exactly when the machine runs in time · The evaluator is primitive recursive

StructureExplicit configurations representing machine configurations#✓fully proved

An explicit configuration \(e\) represents a configuration \(C\) of CSLib's multi-tape model on input \(x\) when they have the same state, the same shifted input head position and the same output, and for every work tape \(i\) and every cell \(z \in \mathbb{Z}\), the content of cell \(z\) of tape \(i\) in \(C\) equals the cell of tape \(i\) of \(e\) at offset \(z - p_i\) from its head, where \(p_i\) is the head position of tape \(i\) in \(C\).

structure Represents {x : List Bool} (e : Config k) (cfg : Cfg k Bool ℕ x) : Prop where
  state : e.state = cfg.state
  inputPos : e.inputPos = cfg.inputPos.val
  output : e.output = cfg.output
  tapes : ∀ i z, cfg.workTapes i z = (e.tapes i).cell (z - cfg.workTapePos i)
Uses 3 · Used by 3
Statement usesExplicit configurations of the code evaluator · Work tapes as zippers · Cell of a zipper tape
Used byEvaluator agreement · The evaluator tracks the machine run · The evaluator simulates the machine step for step

TheoremThe evaluator simulates the machine step for step#✓fully proved

Let \(c\) be a code and \(x\) a binary input. If an explicit configuration \(e\) represents a configuration \(C\) of the machine of \(c\) on \(x\), then the evaluator's step of \(e\) for \(c\) on \(x\) represents the successor of \(C\) under the machine of \(c\).

theorem Represents.step (c : Code k) {x : List Bool} {e : Config k} {cfg : Cfg k Bool ℕ x}
    (h : Represents e cfg) : Represents (Config.step c x e) (c.toTM.step cfg)
Uses 20 · Used by 1
Statement usesCodes for multi-tape machines · Explicit configurations of the code evaluator · Evaluator step · Explicit configurations representing machine configurations · The multi-tape machine of a code
Proof usesApplying a coded action · Input symbol under the input head · Input head move of the clocked evaluator · Work tapes as zippers · Cell of a zipper tape · Moving the head of a zipper tape · Symbol under the head of a zipper tape · Writing on a zipper tape · Action of a code at a key · Step of the machine of a code · Transition function of a code · Coded actions · Decoding a coded action · Decoding a Turing machine head move · Successor under a transition function
Used byThe evaluator tracks the machine run

TheoremThe evaluator tracks the machine run#✓fully proved

For a code \(c\), an input \(x\) and every \(t\), the explicit configuration obtained from the initial one by \(t\) steps of the evaluator for \(c\) on \(x\) represents the configuration that the machine of \(c\) reaches after \(t\) steps from its initial configuration on \(x\).

theorem represents_iterate (c : Code k) (x : List Bool) (t : ℕ) :
    Represents ((Config.step c x)^[t] Config.init) (c.toTM.runFrom (c.toTM.initCfg x) t)
Uses 9 · Used by 1
Statement usesCodes for multi-tape machines · Explicit configurations of the code evaluator · Initial configuration of the clocked evaluator · Evaluator step · Explicit configurations representing machine configurations · The multi-tape machine of a code
Proof usesThe evaluator simulates the machine step for step · Work tapes as zippers · Cell of a zipper tape
Used byEvaluator agreement

TheoremEvaluator agreement#✓fully proved

For every code \(c\), binary input \(x\), clock \(T \in \mathbb{N}\) and binary word \(o\), the clocked evaluator of \(c\) on \(x\) with clock \(T\) returns \(o\) if and only if the machine of \(c\), run for \(T\) steps from its initial configuration on \(x\), has halted and its output is \(o\).

theorem evalSteps_eq_some_iff (c : Code k) (x : List Bool) (T : ℕ) (o : List Bool) :
    c.evalSteps x T = some o ↔
      (c.toTM.runFrom (c.toTM.initCfg x) T).Halted ∧
        (c.toTM.runFrom (c.toTM.initCfg x) T).output = o
Uses 8 · Used by 3
Statement usesCodes for multi-tape machines · Clocked evaluator · The multi-tape machine of a code
Proof usesExplicit configurations of the code evaluator · Initial configuration of the clocked evaluator · Evaluator step · Explicit configurations representing machine configurations · The evaluator tracks the machine run
Used byA code computes exactly what its clocked evaluator returns · Monotonicity of the clocked evaluator for multi-tape codes · The evaluator returns within the clock exactly when the machine runs in time

TheoremThe evaluator returns within the clock exactly when the machine runs in time#✓fully proved

For a code \(c\), an input \(x\) and a clock \(T\), the clocked evaluator of \(c\) on \(x\) with clock \(T\) returns an output if and only if the machine of \(c\) runs in time \(T\) on \(x\), that is, every computation path of that machine on \(x\) with at least \(T\) steps ends in a halted configuration.

theorem isSome_evalSteps_iff_runsInTime (c : Code k) (x : List Bool) (T : ℕ) :
    (c.evalSteps x T).isSome ↔ c.toTM.RunsInTime x T
Uses 5
Statement usesCodes for multi-tape machines · Clocked evaluator · The multi-tape machine of a code
Proof usesEvaluator agreement · Time bounds of deterministic machines

TheoremMonotonicity of the clocked evaluator for multi-tape codes#✓fully proved

For a code \(c\) for machines with \(k\) work tapes, a binary input \(x\), a binary word \(o\) and clocks \(T \le T'\) in \(\mathbb{N}\), if the clocked evaluator of \(c\) on \(x\) returns \(o\) with clock \(T\), then it also returns \(o\) with clock \(T'\).

theorem evalSteps_mono (c : Code k) {x : List Bool} {T T' : ℕ} {o : List Bool}
    (h : c.evalSteps x T = some o) (hT : T ≤ T') : c.evalSteps x T' = some o
Uses 4
Statement usesCodes for multi-tape machines · Clocked evaluator
Proof usesEvaluator agreement · The multi-tape machine of a code

TheoremA code computes exactly what its clocked evaluator returns#✓fully proved

For a code \(c\) with \(k\) work tapes and binary words \(x\) and \(o\), the machine of \(c\) computes \(o\) on input \(x\), that is, it eventually halts on \(x\) with output \(o\), if and only if there is a clock \(T \in \mathbb{N}\) such that the clocked evaluator of \(c\) run on \(x\) for \(T\) steps returns \(o\).

theorem computes_iff_exists_evalSteps (c : Code k) (x o : List Bool) :
    c.toTM.Computes x o ↔ ∃ T, c.evalSteps x T = some o
Uses 4 · Used by 3
Statement usesCodes for multi-tape machines · Clocked evaluator · The multi-tape machine of a code
Proof usesEvaluator agreement
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement

TheoremThe evaluator is primitive recursive#✓fully proved

The evaluator is primitive recursive in the code, the input and the clock.

theorem primrec_evalSteps :
    Primrec fun p : Code k × List Bool × ℕ ↦ p.1.evalSteps p.2.1 p.2.2
Uses 19 · Used by 3
Statement usesCodes for multi-tape machines · Multi-tape codes as tables · Clocked evaluator · Coded actions · Coded actions as tuples · Keys of a code's table
Proof usesExplicit configurations of the code evaluator · Applying a coded action · Explicit configurations as tuples · Initial configuration of the clocked evaluator · Input symbol under the input head · Input head move of the clocked evaluator · Evaluator step · Work tapes as zippers · Moving the head of a zipper tape · Symbol under the head of a zipper tape · Writing on a zipper tape · Action of a code at a key · Halting action
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement

DefinitionCoding head moves#✓fully proved

A head move is coded as a natural number: left is \(0\), stay is \(1\) and right is \(2\). Decoding a move code recovers the move.

def encodeMove : SignType → ℕ
  | .neg => 0
  | .zero => 1
  | .pos => 2
Used by 2
Used byCoding an action · Decoding the coding of an action

DefinitionCoding an action#✓fully proved

Let \(e : Q \to \mathbb{N}\) number the states \(Q\) of a binary multi-tape machine with \(k\) work tapes. The coded action of an action \(a\) of the machine under \(e\) records as its input-head move the code of the input-head move of \(a\) (left \(0\), stay \(1\), right \(2\)); for each work tape it records what \(a\) writes there and the code of the head move of \(a\) there; it records the output bit of \(a\), if any; and its next state is \(e(q)\) when \(a\) enters the state \(q\), and it halts when \(a\) halts.

def encodeAction {State : Type*} (e : State → ℕ) (a : Action k Bool State) : CodeAction k where
  inputMove := encodeMove a.inputTape
  work i := ((a.workTapes i).1, encodeMove (a.workTapes i).2)
  out := a.output
  next := a.state.map e
Uses 2 · Used by 4
Statement usesCoded actions · Coding head moves
Used byThe code of a machine takes its coded actions · The code of a machine simulates it · The code of a finite-state binary machine · Decoding the coding of an action

TheoremDecoding the coding of an action#✓fully proved

Let \(Q\) be a type, \(e : Q \to \mathbb{N}\) a map and \(a\) an action of a binary machine with \(k\) work tapes and states in \(Q\). The action that the coded action of \(a\), with its successor state numbered by \(e\), stands for is \(a\) with its successor state relabelled by \(e\).

theorem toAction_encodeAction {State : Type*} (e : State → ℕ) (a : Action k Bool State) :
    (encodeAction e a).toAction = relabelAction e a
Uses 6 · Used by 1
Statement usesDecoding a coded action · Coding an action · Relabelling the successor state of an action
Proof usesCoded actions · Decoding a Turing machine head move · Coding head moves
Used byThe code of a machine simulates it

DefinitionState bound of a code#✓fully proved

The states of a code \(c\) are the initial state \(0\) and every successor state named in its table. The state bound of \(c\) is one more than the largest of them; it is a strict upper bound on the states of \(c\).

def stateBound (c : Code k) : ℕ := c.states.sup id + 1
Uses 2 · Used by 5
Statement usesCodes for multi-tape machines · States of a multi-tape code
Used byComputation by a code is finite-state computation · Deciding by a code is finite-state decidability · Transition function of a code on bounded states · A code's machine simulates its finite-state machine · The finite-state machine of a code

DefinitionA number as a bounded state#✓fully proved

For natural numbers \(N\) and \(q\), this is \(q\) as an element of \(\{0, \dots, N - 1\}\) if \(q < N\), and no value otherwise.

def finState (N q : ℕ) : Option (Fin N) := if h : q < N then some ⟨q, h⟩ else none
Used by 2
Used byTransition function of a code on bounded states · A code's machine simulates its finite-state machine

DefinitionTransition function of a code on bounded states#✓fully proved

Let \(c\) be a code with \(k\) work tapes and let \(N\) be its state bound. For a state \(q < N\), a symbol \(a\) under the input head and symbols \(w\) under the \(k\) work heads (each a bit or blank), this is the action of \(c\) at \((q, a, w)\) with the same input-head move, work-tape writes and moves, and output, and with its successor state read as a state below \(N\); a successor state that is not below \(N\) is replaced by halting.

def finTr (c : Code k) (q : Fin c.stateBound) (a : Option Bool) (w : Fin k → Option Bool) :
    Action k Bool (Fin c.stateBound) :=
  ⟨(c.tr q a w).inputTape, (c.tr q a w).workTapes, (c.tr q a w).output,
    (c.tr q a w).state.bind (finState c.stateBound)⟩
Uses 4 · Used by 2
Statement usesCodes for multi-tape machines · A number as a bounded state · State bound of a code · Transition function of a code
Used byA code's machine simulates its finite-state machine · The finite-state machine of a code

DefinitionThe finite-state machine of a code#✓fully proved

For a code \(c\) with \(k\) work tapes and state bound \(N\), this is the binary machine with \(k\) work tapes and states \(0, 1, \dots, N - 1\) that starts in state \(0\) and, in a state \(q < N\) reading \(a\) under the input head and \(w\) under the work heads, takes the action of \(c\) at \((q, a, w)\), with a successor state not below \(N\) replaced by halting. Since every state the machine of \(c\) can enter is below \(N\), it is the machine of \(c\) with its states restricted to those below \(N\).

noncomputable def toFinTM (c : Code k) : MultiTapeTM k Bool (Fin c.stateBound) :=
  MultiTapeTM.ofTr ⟨0, c.zero_lt_stateBound⟩ c.finTr
Uses 4 · Used by 3
Statement usesCodes for multi-tape machines · Transition function of a code on bounded states · State bound of a code · States of a multi-tape code
Used byComputation by a code is finite-state computation · Deciding by a code is finite-state decidability · A code's machine simulates its finite-state machine

TheoremA code's machine simulates its finite-state machine#✓fully proved

For every code \(c\), the machine of \(c\) simulates the finite-state machine of \(c\) up to the relabelling that sends each state \(q < N\), where \(N\) is the state bound of \(c\), to the natural number \(q\).

theorem isRelabelling_toFinTM (c : Code k) : IsRelabelling Fin.val c.toFinTM c.toTM
Uses 11 · Used by 2
Statement usesCodes for multi-tape machines · State bound of a code · The finite-state machine of a code · The multi-tape machine of a code · Simulation up to a state relabelling
Proof usesA number as a bounded state · Transition function of a code on bounded states · Next states of a code lie in its state set · States of a multi-tape code · Transition function of a code · Relabelling the successor state of an action
Used byComputation by a code is finite-state computation · Deciding by a code is finite-state decidability

TheoremComputation by a code is finite-state computation#✓fully proved

Let \(c\) be a code with \(k\) work tapes, let \(g : \alpha \to \beta\) be a function, let inputs in \(\alpha\) and outputs in \(\beta\) be encoded by injective maps into binary words, and let \(t, s : \alpha \to \mathbb{N}\). If the machine of \(c\), started on the encoding of any input \(x\), halts with the encoding of \(g(x)\) as output, halts within \(t(x)\) steps, and visits at most \(s(x)\) work-tape cells, then some binary multi-tape machine with finitely many states computes \(g\) within the same bounds in the same sense.

theorem computableInTimeAndSpace {α β : Type*} {g : α → β} {encIn : α ↪ List Bool}
    {encOut : β ↪ List Bool} {t s : α → ℕ} (c : Code k)
    (h : c.toTM.ComputesFunInTimeAndSpace encIn encOut g t s) :
    MultiTapeTM.ComputableInTimeAndSpace g encIn encOut t s
Uses 6 · Used by 1
Statement usesCodes for multi-tape machines · The multi-tape machine of a code
Proof usesA code's machine simulates its finite-state machine · State bound of a code · The finite-state machine of a code · Relabelling preserves computing a function within time and space bounds
Used byComputability over codes

TheoremDeciding by a code is finite-state decidability#✓fully proved

Let \(c\) be a code with \(k\) work tapes, let \(L\) be a set of binary words, and let \(t\) and \(s\) map binary words to natural numbers. If the machine of \(c\) decides \(L\), that is, started on any binary word \(w\) it halts with the one-bit output \(\mathrm{true}\) if \(w \in L\) and \(\mathrm{false}\) otherwise, and if on every binary word \(w\) it halts within \(t(w)\) steps and visits at most \(s(w)\) work-tape cells, then some binary multi-tape machine with finitely many states decides \(L\) within the same bounds.

theorem decidableInTimeAndSpace {L : Set (List Bool)} {t s : List Bool → ℕ} (c : Code k)
    (hd : Decides c.toTM L) (ht : ∀ w, c.toTM.RunsInTime w (t w))
    (hs : ∀ w, c.toTM.RunsInSpace w (s w)) :
    MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl _) t s
Uses 10 · Used by 3
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · A multi-tape machine deciding a language
Proof usesA code's machine simulates its finite-state machine · State bound of a code · The finite-state machine of a code · Relabelling preserves deciding a language · Relabelling preserves space bounds · Relabelling preserves time bounds · Decidability within time and space bounds, unfolded
Used byDecidability over codes · DSPACE over codes · DTIME over codes

DefinitionThe code of a finite-state binary machine#✓fully proved

Let \(M\) be a machine over the binary alphabet with \(k\) work tapes and a finite set of states \(Q\), and let \(e : Q \to \mathbb{N}\). The code of \(M\) with states numbered by \(e\) has one table entry for each state \(q \in Q\), symbol \(a\) under the input head and symbols \(w\) under the \(k\) work heads (each a bit or blank): its key is \((e(q), a, w)\) and its value is the coded action of \(M\) in state \(q\) reading \(a\) and \(w\), with the successor state numbered by \(e\). The entries are listed in an unspecified order.

When \(e\) is injective and sends the initial state of \(M\) to \(0\), the machine of this code simulates \(M\) up to the relabelling \(e\).

noncomputable def ofTM {State : Type*} [Fintype State] (tm : MultiTapeTM k Bool State)
    (e : State → ℕ) : Code k :=
  ⟨(Finset.univ : Finset (State × Option Bool × (Fin k → Option Bool))).toList.map
    fun x ↦ ((e x.1, x.2.1, x.2.2), encodeAction e (tm.tr x.1 x.2.1 x.2.2))⟩
Uses 4 · Used by 3
Statement usesCodes for multi-tape machines · Coded actions · Keys of a code's table · Coding an action
Used byThe code of a machine takes its coded actions · Every finite-state machine has a code · The code of a machine simulates it

TheoremThe code of a machine takes its coded actions#✓fully proved

Let \(M\) be a binary multi-tape machine with \(k\) work tapes and a finite set of states \(Q\), and let \(e : Q \to \mathbb{N}\) be injective. For every state \(q \in Q\), every symbol \(a\) under the input head and every tuple \(w\) of symbols under the \(k\) work heads (each a bit or blank), the coded action of the code of \(M\) under \(e\) at state \(e(q)\) and symbols \(a\), \(w\) is the coding, with successor states numbered by \(e\), of the action of \(M\) in state \(q\) on \(a\) and \(w\).

theorem act_ofTM {State : Type*} [Fintype State] (tm : MultiTapeTM k Bool State) {e : State → ℕ}
    (he : Function.Injective e) (q : State) (a : Option Bool) (w : Fin k → Option Bool) :
    (ofTM tm e).act (e q) a w = encodeAction e (tm.tr q a w)
Uses 7 · Used by 1
Statement usesAction of a code at a key · The code of a finite-state binary machine · Coded actions · Coding an action
Proof usesCodes for multi-tape machines · Halting action · Keys of a code's table
Used byThe code of a machine simulates it

TheoremThe code of a machine simulates it#✓fully proved

Let \(M\) be a machine over the binary alphabet with \(k\) work tapes, a finite set of states \(Q\) and initial state \(q_0\), and let \(e : Q \to \mathbb{N}\) be injective with \(e(q_0) = 0\). Then the machine of the code of \(M\) with states numbered by \(e\) simulates \(M\) up to the relabelling \(e\).

theorem isRelabelling_ofTM {State : Type*} [Fintype State] (tm : MultiTapeTM k Bool State)
    {e : State → ℕ} (he : Function.Injective e) (h₀ : e tm.q₀ = 0) :
    IsRelabelling e tm (ofTM tm e).toTM
Uses 12 · Used by 1
Statement usesThe code of a finite-state binary machine · The multi-tape machine of a code · Simulation up to a state relabelling
Proof usesCodes for multi-tape machines · Action of a code at a key · The code of a machine takes its coded actions · Transition function of a code · Coded actions · Decoding a coded action · Coding an action · Relabelling the successor state of an action · Decoding the coding of an action
Used byEvery finite-state machine has a code

TheoremNumbering a finite type from a chosen element#✓fully proved

For every finite type \(Q\) and every \(q_0 \in Q\) there is an injective map \(e : Q \to \mathbb{N}\) with \(e(q_0) = 0\).

theorem exists_injective_nat_eq_zero {State : Type*} [Finite State] (q₀ : State) :
    ∃ e : State → ℕ, Function.Injective e ∧ e q₀ = 0
Used by 1
Used byEvery finite-state machine has a code

TheoremEvery finite-state machine has a code#✓fully proved

A binary machine with finitely many states is simulated, up to an injective state relabelling, by the machine of some code.

theorem exists_code_isRelabelling {State : Type*} [Finite State]
    (tm : MultiTapeTM k Bool State) :
    ∃ (c : Code k) (e : State → ℕ), Function.Injective e ∧ IsRelabelling e tm c.toTM
Uses 6 · Used by 5
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · Simulation up to a state relabelling
Proof usesNumbering a finite type from a chosen element · The code of a machine simulates it · The code of a finite-state binary machine
Used byA predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Computability over codes · Decidability over codes

TheoremComputability over codes#✓fully proved

Let \(g : \alpha \to \beta\) be a function, let inputs in \(\alpha\) and outputs in \(\beta\) be encoded by injective maps into binary words, and let \(t, s : \alpha \to \mathbb{N}\). Say a machine computes \(g\) within \(t\) and \(s\) when, started on the encoding of any input \(x\), it halts with the encoding of \(g(x)\) as output, halts within \(t(x)\) steps, and visits at most \(s(x)\) work-tape cells. Then some binary multi-tape machine with finitely many states computes \(g\) within \(t\) and \(s\) if and only if, for some number \(k\) of work tapes, the machine of some code with \(k\) work tapes computes \(g\) within \(t\) and \(s\).

theorem computableInTimeAndSpace_iff_exists_code {α β : Type*} {g : α → β}
    {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} :
    MultiTapeTM.ComputableInTimeAndSpace g encIn encOut t s ↔
      ∃ (k : ℕ) (c : Code k), c.toTM.ComputesFunInTimeAndSpace encIn encOut g t s
Uses 6
Statement usesCodes for multi-tape machines · The multi-tape machine of a code
Proof usesComputation by a code is finite-state computation · Every finite-state machine has a code · Simulation up to a state relabelling · Relabelling preserves computing a function within time and space bounds

TheoremDecidability over codes#✓fully proved

Let \(L\) be a set of binary words and let \(t\) and \(s\) map binary words to natural numbers. Say a machine decides \(L\) within \(t\) and \(s\) when, started on any binary word \(w\), it halts with the one-bit output \(\mathrm{true}\) if \(w \in L\) and \(\mathrm{false}\) otherwise, halts within \(t(w)\) steps, and visits at most \(s(w)\) work-tape cells. Then some binary multi-tape machine with finitely many states decides \(L\) within \(t\) and \(s\) if and only if, for some number \(k\) of work tapes, the machine of some code with \(k\) work tapes decides \(L\) within \(t\) and \(s\).

theorem decidableInTimeAndSpace_iff_exists_code {L : Set (List Bool)} {t s : List Bool → ℕ} :
    MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl _) t s ↔
      ∃ (k : ℕ) (c : Code k), Decides c.toTM L ∧ (∀ w, c.toTM.RunsInTime w (t w)) ∧
        ∀ w, c.toTM.RunsInSpace w (s w)
Uses 10 · Used by 2
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · A multi-tape machine deciding a language
Proof usesDeciding by a code is finite-state decidability · Every finite-state machine has a code · Simulation up to a state relabelling · Relabelling preserves deciding a language · Relabelling preserves space bounds · Relabelling preserves time bounds · Decidability within time and space bounds, unfolded
Used byDSPACE over codes · DTIME over codes

TheoremDTIME over codes#✓fully proved

For every \(t : \mathbb{N} \to \mathbb{N}\) and every language \(L\) of binary words, \(L \in \mathsf{DTIME}(t)\) if and only if there are natural numbers \(c_1, c_2, k\) and a code \(c\) with \(k\) work tapes such that the machine of \(c\) decides \(L\), on every input \(w\) runs in time \(c_1 t(|w|) + c_2\), and for some \(s : \mathbb{N} \to \mathbb{N}\) on every input \(w\) runs in space \(s(|w|)\).

theorem mem_DTIME_iff_exists_code {t : ℕ → ℕ} {L : Set (List Bool)} :
    L ∈ DTIME t ↔ ∃ (c₁ c₂ k : ℕ) (c : Code k), Decides c.toTM L ∧
      TimeBoundedBy c.toTM (fun n ↦ c₁ * t n + c₂) ∧ ∃ s, SpaceBoundedBy c.toTM s
Uses 8
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · Deterministic time classes on multi-tape machines · A multi-tape machine deciding a language · Space-bounded multi-tape machine · Time-bounded multi-tape machine
Proof usesDeciding by a code is finite-state decidability · Decidability over codes

TheoremDSPACE over codes#✓fully proved

For every \(s : \mathbb{N} \to \mathbb{N}\) and every language \(L\) of binary words, \(L \in \mathsf{DSPACE}(s)\) if and only if there are natural numbers \(c_1, c_2, k\) and a code \(c\) with \(k\) work tapes such that the machine of \(c\) decides \(L\), on every input \(w\) runs in space \(c_1 s(|w|) + c_2\), and for some \(t : \mathbb{N} \to \mathbb{N}\) on every input \(w\) runs in time \(t(|w|)\).

theorem mem_DSPACE_iff_exists_code {s : ℕ → ℕ} {L : Set (List Bool)} :
    L ∈ DSPACE s ↔ ∃ (c₁ c₂ k : ℕ) (c : Code k), Decides c.toTM L ∧
      SpaceBoundedBy c.toTM (fun n ↦ c₁ * s n + c₂) ∧ ∃ t, TimeBoundedBy c.toTM t
Uses 8
Statement usesCodes for multi-tape machines · The multi-tape machine of a code · Deterministic space classes on multi-tape machines · A multi-tape machine deciding a language · Space-bounded multi-tape machine · Time-bounded multi-tape machine
Proof usesDeciding by a code is finite-state decidability · Decidability over codes
59 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.