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.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.
• Turing.BusyBeaver.step M { q := none, tape := tape } = none

def Turing.BusyBeaver.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

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

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

The initial configuration.

Equations

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

def Turing.BusyBeaver.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

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

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

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

• halts : (eval M []).Dom

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

The predicate that a Turing machine M has reached a halting state after n steps. For n = 0 this is the predicate that M has already halted.

In the BB setup, halting state can be attained in two manners:

1. The machine can reach a configutation s that has no transitions to other states, i.e. step M s = none
2. The machine can reach a "halting state configuration" s, i.e. s.q = none.

Equations

• M.HaltsAt s n = ((fun (x : Option (Turing.BusyBeaver.Cfg Γ Λ)) => x.bind (Turing.BusyBeaver.step M))^[n + 1] (some s) = none ∨ s.q = none)

theorem Turing.BusyBeaver.Machine.haltsAt_zero_iff {Γ Λ : Type} [Fintype Γ] [Fintype Λ] [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (s : Cfg Γ Λ) : M.HaltsAt s 0 ↔ step M s = none ∨ s.q = none

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

Equations

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