Finite-state Turing machines

A machine has a finite transition table and a tape from Mathlib. This module preserves the execution definitions and the two Goldbach tables from google-deepmind/cryptids. The tables are embedded as Lean literals so importing the project needs no external files.

structure ConjectureMachines.Machine (states symbols : ℕ) : Type

A transition table: for a state and the symbol under the head, either the symbol to write, the direction to move and the state to enter, or none to halt.

• transition : Fin states → Fin symbols → Option (Fin symbols × Turing.Dir × Fin states)

  The action for each state and scanned symbol.

structure ConjectureMachines.Cfg (states symbols : ℕ) [NeZero symbols] : Type

A configuration: the current state and the tape, whose head is the symbol under the head.

• state : Fin states

  The current control state.

• tape : Turing.Tape (Fin symbols)

  The tape and head position.

def ConjectureMachines.step {states symbols : ℕ} [NeZero symbols] (M : Machine states symbols) : Cfg states symbols → Option (Cfg states symbols)

One step, or none when the transition is missing.

Equations

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

def ConjectureMachines.init {states symbols : ℕ} [NeZero states] [NeZero symbols] : Cfg states symbols

The start state on the all-blank tape.

Equations

• ConjectureMachines.init = { state := 0, tape := Turing.Tape.mk₁ [] }

def ConjectureMachines.Halts {states symbols : ℕ} [NeZero states] [NeZero symbols] (M : Machine states symbols) : Prop

M halts when started in state 0 on the all-blank tape.

Equations

• ConjectureMachines.Halts M = (StateTransition.eval (ConjectureMachines.step M) ConjectureMachines.init).Dom

def ConjectureMachines.Machine.ofRows {states symbols : ℕ} (rows : List (List (Option (Fin symbols × Turing.Dir × Fin states)))) : Machine states symbols

Build a Machine states symbols from a list of per-state transition rows.

Equations

• ConjectureMachines.Machine.ofRows rows = { transition := fun (q : Fin states) (a : Fin symbols) => (rows.getD ↑q []).getD (↑a) none }

structure ConjectureMachines.BundledMachine (symbols : ℕ) : Type

A Turing machine over symbols tape symbols bundled with its non-zero state count.

• states : ℕ

  The number of control states.

• neZeroStates : NeZero self.states
• toMachine : Machine self.states symbols

  The transition table with this state count.

@[reducible, inline]

abbrev ConjectureMachines.Machine.bundle {states symbols : ℕ} (M : Machine (states + 1) symbols) : BundledMachine symbols

Bundle a Machine (states + 1) symbols into a BundledMachine symbols.

Equations

• M.bundle = { states := states + 1, neZeroStates := ⋯, toMachine := M }

@[reducible, inline]

abbrev ConjectureMachines.BundledMachine.Halts {symbols : ℕ} [NeZero symbols] (M : BundledMachine symbols) : Prop

M halts when started in state 0 on the all-blank tape.

Equations

• M.Halts = ConjectureMachines.Halts M.toMachine

def ConjectureMachines.Machines.goldbach25Rows : List (List (Option (Fin 2 × Turing.Dir × Fin 25)))

Rows of the 25-state machine of Yijun Leng, from the upstream baseline table.

Equations

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

def ConjectureMachines.Machines.goldbach25 : Machine 25 2

The 25-state Goldbach baseline.

Equations

• ConjectureMachines.Machines.goldbach25 = ConjectureMachines.Machine.ofRows ConjectureMachines.Machines.goldbach25Rows

def ConjectureMachines.Machines.goldbach21Rows : List (List (Option (Fin 2 × Turing.Dir × Fin 21)))

Rows of the 21-state machine of Maxence Faldor and Moritz Firsching.

Equations

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

def ConjectureMachines.Machines.goldbach21 : Machine 21 2

The 21-state Goldbach machine.

Equations

• ConjectureMachines.Machines.goldbach21 = ConjectureMachines.Machine.ofRows ConjectureMachines.Machines.goldbach21Rows

def ConjectureMachines.run {states symbols : ℕ} [NeZero states] [NeZero symbols] (M : Machine states symbols) (n : ℕ) : Option (Cfg states symbols)

The configuration n steps in from init, or none once M has halted.

Equations

• ConjectureMachines.run M n = (fun (c : Option (ConjectureMachines.Cfg states symbols)) => c.bind (ConjectureMachines.step M))^[n] (some ConjectureMachines.init)

def ConjectureMachines.Runs {states symbols : ℕ} [NeZero states] [NeZero symbols] (M : Machine states symbols) (n : ℕ) : Prop

M, started in state 0 on the all-blank tape, has not halted within n steps.

Equations

• ConjectureMachines.Runs M n = ((ConjectureMachines.run M n).isSome = true)

@[instance_reducible]

instance ConjectureMachines.instDecidableRuns {states symbols : ℕ} [NeZero states] [NeZero symbols] (M : Machine states symbols) (n : ℕ) : Decidable (Runs M n)

Equations

• ConjectureMachines.instDecidableRuns M n = ConjectureMachines.instDecidableRuns._aux_1 M n