Turing Machines, Busy Beaver version.

A variant on the definition of the TM0 model in Mathlib: while the statements the TM can make in the usual TM0 are split into two categories (either write at the current position or move left/right), we want to combine the two to stick to the BB convention: first write at the current position and then move left/right.

Note that this Turing Machine model also works with states of type Option Γ. This is because in the busy beaver context, the turing machines also have an addition "halting" state

See also https://git.sr.ht/~vigoux/busybeaver for a different approach to formalising these objects.

structure Turing.BusyBeaver.Stmt (Γ : Type u_1) : Type u_1

A Turing machine "statement" is just a command to write a symbol on the tape (at the current position) and then move left or right

• write :: (
• symbol : Γ
• dir : Dir
• )

instance Turing.BusyBeaver.instInhabitedStmt {a✝ : Type u_3} [Inhabited a✝] : Inhabited (Stmt a✝)

Equations

• Turing.BusyBeaver.instInhabitedStmt = { default := { symbol := default, dir := default } }

def Turing.BusyBeaver.Machine (Γ : Type u_1) (Λ : Type u_2) [Inhabited Λ] : Type (max (max u_1 u_2) u_1 u_2)

A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Option Λ and a Stmt describing what to do: a command to write a symbol and move left or right. Notice that there are two ways of halting at a given (state, head) pair: either the machine halts immediatly (i.e. the function returns none), or the machine moves to the "halting state", i.e. none : Option Λ and performs one last action.

Typically, both Λ and Γ are required to be inhabited; the default value for Γ is the "blank" tape value, and the default value of Λ is the initial state.

Equations

• Turing.BusyBeaver.Machine Γ Λ = (Λ → Γ → Option (Option Λ × Turing.BusyBeaver.Stmt Γ))

instance Turing.BusyBeaver.Machine.inhabited (Γ : Type u_1) (Λ : Type u_2) [Inhabited Λ] : Inhabited (Machine Γ Λ)

Equations

• Turing.BusyBeaver.Machine.inhabited Γ Λ = id inferInstance

structure Turing.BusyBeaver.Cfg (Γ : Type u_1) (Λ : Type u_2) [Inhabited Γ] : Type (max u_1 u_2)

The configuration state of a Turing machine during operation consists of a label (machine state), and a tape. The tape is represented in the form (a, L, R), meaning the tape looks like L.rev ++ [a] ++ R with the machine currently reading the a. The lists are automatically extended with blanks as the machine moves around.

• q : Option Λ

  The current machine state.

• tape : Tape Γ

  The current state of the tape: current symbol, left and right parts.

instance Turing.BusyBeaver.Cfg.inhabited {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] : Inhabited (Cfg Γ Λ)

Equations

• Turing.BusyBeaver.Cfg.inhabited = { default := { q := default, tape := default } }

def Turing.BusyBeaver.Machine.step {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) : Cfg Γ Λ → Option (Cfg Γ Λ)

Execution semantics of the Turing machine.

Equations

• One or more equations did not get rendered due to their size.
• M.step { q := none, tape := tape } = none

def Turing.BusyBeaver.Machine.Reaches {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) : Cfg Γ Λ → Cfg Γ Λ → Prop

The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂.

Equations

• M.Reaches = Relation.ReflTransGen fun (a b : Turing.BusyBeaver.Cfg Γ Λ) => b ∈ M.step a

def Turing.BusyBeaver.Machine.init {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (l : List Γ) : Cfg Γ Λ

The initial configuration.

Equations

• Turing.BusyBeaver.Machine.init l = { q := some default, tape := Turing.Tape.mk₁ l }

def Turing.BusyBeaver.Machine.eval {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (l : List Γ) : Part (ListBlank Γ)

Evaluate a Turing machine on initial input to a final state, if it terminates.

Equations

• M.eval l = Part.map (fun (c : Turing.BusyBeaver.Cfg Γ Λ) => c.tape.right₀) (Turing.eval M.step (Turing.BusyBeaver.Machine.init l))

def Turing.BusyBeaver.Machine.multiStep {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (config : Cfg Γ Λ) (n : ℕ) : Option (Cfg Γ Λ)

Equations

• M.multiStep config n = (fun (x : Option (Turing.BusyBeaver.Cfg Γ Λ)) => x.bind M.step)^[n] (some config)

@[simp]

theorem Turing.BusyBeaver.Machine.multiStep_zero {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (config : Cfg Γ Λ) : M.multiStep config 0 = some config

@[simp]

theorem Turing.BusyBeaver.Machine.multiStep_one {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (config : Cfg Γ Λ) : M.multiStep config 1 = M.step config

@[simp]

theorem Turing.BusyBeaver.Machine.multiStep_succ {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (config : Cfg Γ Λ) (n : ℕ) : M.multiStep config (n + 1) = (M.multiStep config n).bind M.step

theorem Turing.BusyBeaver.Machine.multiStep_eq_none_of_le_of_multiStep_eq_none {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] {M : Machine Γ Λ} {config : Cfg Γ Λ} {m n : ℕ} (hmn : m ≤ n) (hm : M.multiStep config m = none) : M.multiStep config n = none

def Turing.BusyBeaver.Machine.IsHaltingInput {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (l : List Γ) : Prop

M.IsHaltingInput l is the predicate that M is a halting configuration for M.

Equations

• M.IsHaltingInput l = (M.eval l).Dom

def Turing.BusyBeaver.Machine.IsHaltingConfiguration {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (s : Cfg Γ Λ) : Prop

M.HaltsAtConfiguration s is the predicate that M is a halting configuration for M.

Equations

• M.IsHaltingConfiguration s = ((M.step s).isNone = true)

class Turing.BusyBeaver.Machine.IsHalting {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) : Prop

The property that a Turing Machine M eventually halts when starting from an empty tape

• halts : M.IsHaltingInput []

def Turing.BusyBeaver.Machine.HaltsAfter {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (s : Cfg Γ Λ) (n : ℕ) : Prop

The predicate that a machine starting at configuration s stops after at most n steps, i.e. reaches a configuration from which there are no defined transitions.

Equations

• M.HaltsAfter s n = (M.multiStep s (n + 1) = none)

theorem Turing.BusyBeaver.Machine.haltsAfter_zero_iff {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (s : Cfg Γ Λ) : M.HaltsAfter s 0 ↔ M.step s = none

theorem Turing.BusyBeaver.Machine.isHalting_iff_exists_haltsAt {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) : M.IsHalting ↔ ∃ (n : ℕ), M.HaltsAfter (init []) n

noncomputable def Turing.BusyBeaver.Machine.haltingNumber {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) : PartENat

Equations

• M.haltingNumber = sInf {x : PartENat | ∃ (n : ℕ) (_ : M.HaltsAfter (Turing.BusyBeaver.Machine.init []) n), ↑n = x}

theorem Turing.BusyBeaver.Machine.haltingNumber_def {Γ : Type u_3} {Λ : Type u_4} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (n : ℕ) (hn : ∃ (a : Cfg Γ Λ), M.multiStep (init []) n = some a) (ha' : M.multiStep (init []) (n + 1) = none) : M.haltingNumber = ↑n