Basic definitions for Turing Machines (TMs)

inductive Cslib.Computability.Turing.SingleTape.TrLabel (Symbol : Type u_1) : Type u_1

The transition labels used by a single-tape Turing Machine.

• read {Symbol : Type u_1} (x : Symbol) : TrLabel Symbol

  Read x from the tape.

• write {Symbol : Type u_1} (x : Symbol) : TrLabel Symbol

  Write x on the tape.

• move {Symbol : Type u_1} (d : Turing.Dir) : TrLabel Symbol

  Move the head of the tape.

• skip {Symbol : Type u_1} : TrLabel Symbol

  Do nothing.

def Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape {Symbol : Type u_1} [DecidableEq Symbol] (otape : Option (Turing.BiTape Symbol)) (μ : TrLabel Symbol) : Option (Turing.BiTape Symbol)

Applies a transition label to a tape, returning none if it is not possible. The input is taken as an Option to make the function composable.

Equations

• Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape (some tape) (Cslib.Computability.Turing.SingleTape.TrLabel.read x) = if some x = tape.head then some tape else none
• Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape (some tape) (Cslib.Computability.Turing.SingleTape.TrLabel.write x) = some (tape.write (some x))
• Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape (some tape) (Cslib.Computability.Turing.SingleTape.TrLabel.move d) = some (tape.move d)
• Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape (some tape) Cslib.Computability.Turing.SingleTape.TrLabel.skip = some tape
• Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape otape μ = none

theorem Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape_isSome {Symbol : Type u_1} [DecidableEq Symbol] {μ : TrLabel Symbol} {ot : Option (Turing.BiTape Symbol)} (h : (applyToTape ot μ).isSome = true) : ot.isSome = true

theorem Cslib.Computability.Turing.SingleTape.TrLabel.applyToTape_foldl_isSome {Symbol : Type u_1} [DecidableEq Symbol] {μs : List (TrLabel Symbol)} {ot : Option (Turing.BiTape Symbol)} (h : (List.foldl applyToTape ot μs).isSome = true) : ot.isSome = true

structure Cslib.Computability.Turing.SingleTape.Cfg (State : Type u_1) (Symbol : Type u_2) : Type (max u_1 u_2)

Configuration of a single-tape Turing machine.

• state : State

  The state that the machine is in.

• tape : Turing.BiTape Symbol

  Tape of the machine (memory).

theorem Cslib.Computability.Turing.SingleTape.Cfg.ext {State : Type u_1} {Symbol : Type u_2} {x y : Cfg State Symbol} (state : x.state = y.state) (tape : x.tape = y.tape) : x = y

theorem Cslib.Computability.Turing.SingleTape.Cfg.ext_iff {State : Type u_1} {Symbol : Type u_2} {x y : Cfg State Symbol} : x = y ↔ x.state = y.state ∧ x.tape = y.tape

def Cslib.Computability.Turing.SingleTape.Cfg.mk₁ {State : Type u_1} {Symbol : Type u_2} (s : State) (xs : List Symbol) : Cfg State Symbol

Helper builder for a configuration with a given tape content.

Equations

• Cslib.Computability.Turing.SingleTape.Cfg.mk₁ s xs = { state := s, tape := Cslib.Turing.BiTape.mk₁ xs }

def Cslib.Computability.Turing.SingleTape.Cfg.spaceUsed {State : Type u_1} {Symbol : Type u_2} (cfg : Cfg State Symbol) : ℕ

The space used by a configuration is the space used by its tape.

Equations

• cfg.spaceUsed = cfg.tape.spaceUsed