Turing Machine Halting in Lean

Harold Cooper

I recently fooled around with the theorem-proving language Lean, and proved whether some very simple Turing machines halt or not. These are my notes on how I did that.

The code is also on github and can be run in the web-based Lean editor.

Basic definitions

There’s some existing Turing machinery in the Lean community’s extensive mathlib library, so first we import that:

import computability.turing_machine

Then we define our set of machine states Λ and set of tape symbols Γ1 and mark both types as inhabited by specifying their default elements, because the imported code uses such types:

inductive Λ -- states
| A
| B
| C

inductive Γ -- symbols
| zero
| one

instance Λ.inhabited : inhabited Λ := ⟨Λ.A⟩
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

And for convenience we define an initial machine configuration, of the initial state (A) and an empty tape:

def cfg₀ : turing.TM0.cfg Γ Λ := turing.TM0.init []

We want to be able to repeatedly run a Turing machine one step at a time, but the existing turing.TM0.step function is inconvenient for this, because it takes a configuration turing.TM0.cfg Γ Λ as input but outputs a different type option (turing.TM0.cfg Γ Λ). So we use option.bind to define a more convenient function whose input and output are the same type:

def step'
  (M : turing.TM0.machine Γ Λ)
  (x : option (turing.TM0.cfg Γ Λ)) :
  option (turing.TM0.cfg Γ Λ) :=
x.bind (turing.TM0.step M)

Now we can easily use Lean’s f^[n] iteration shorthand to define a function which steps a given number of times:

def multistep
  (M : turing.TM0.machine Γ Λ)
  (n : ℕ)
  (cfg : turing.TM0.cfg Γ Λ) :
  option (turing.TM0.cfg Γ Λ) :=
step' M^[n] (some cfg)

Some little proofs

Now for fun we can prove some theorems about multistep.

If multistep M n cfg = none then multistep M (n + m) cfg = none for any m, i.e. once the machine has halted it stays halted. We prove this by induction on m:

theorem multistep_none_add
  {cfg M n m}
  (hn : multistep M n cfg = none) :
  multistep M (n + m) cfg = none :=
begin
  induction m with m hm,
  { exact hn, },
  { rw [multistep, nat.add_succ, function.iterate_succ_apply',
        ← multistep, hm],
    refl, },
end

And we can prove the same thing for m≥n instead of m+n, by using mathlib’s theorem nat.add_sub_of_le to rewrite m as n+(m-n), followed by multistep_none_add from above:

theorem multistep_none_ge
  {cfg M n}
  {m ≥ n}
  (hn : multistep M n cfg = none) :
  multistep M m cfg = none :=
begin
  rw ← nat.add_sub_of_le H,
  exact multistep_none_add hn,
end

(Reading these proofs non-interactively isn’t very illuminating—you can try clicking through them in the Lean web editor, though it might not make much sense if you haven’t used a proof assistant before.)

Defining halting

With multistep defined, we can easily define halting. Starting from cfg₀ (an empty tape and the initial state), a machine M halts if there is some n such that it halts after n steps:

def halts (M : turing.TM0.machine Γ Λ) : Prop :=
∃ n, multistep M n cfg₀ = none

Now we can try using this definition of halting, for a few specific simple Turing machines.

A machine that halts immediately

First we’ll define the simplest possible machine, which just halts (i.e. returns none) no matter what its current state and tape symbol are:

def M₁ : turing.TM0.machine Γ Λ
| _ _ := none

To prove this halts, we basically just run it for one step and see that it has halted.

Specifically, we use Lean’s ⟨⟩ implicit constructor syntax to construct a proof of ∃ n, multistep M₁ n cfg₀ = none (aka halts M₁), by specifying n=1 and using rfl to prove the trivial multistep M₁ 1 cfg₀ = none:

theorem M₁_halts : halts M₁ :=
⟨1, rfl⟩

A machine that goes A → B → halt

In state A, this machine goes to state B, and writes the current symbol back to the tape (i.e. basically ignores the tape). And for any other state (including B) it halts:

def M₂ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| _ _ := none

So again we can easily prove that it halts, by simply running it for two steps:

theorem M₂_halts : halts M₂ :=
⟨2, rfl⟩

A machine that loops A → B → A → B → ⋯

Proving that a machine halts isn’t very interesting since you just run it until it halts. Proving that a machine doesn’t halt is trickier and potentially more useful (e.g. for helping to determine the values of the Busy Beaver function).

This machine loops forever between A and B, while leaving the tape unchanged:

def M₃ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| Λ.B symbol := some ⟨Λ.A, turing.TM0.stmt.write symbol⟩
| _ _ := none

(We have to specify the final _ _ := none because Λ.C is a possible state as far as the type system is concerned.)

Proving that this machine doesn’t halt is more work than the previous trivial halting proofs. First we prove that for any number of steps, the machine always ends up in either state A or state B.

We prove this by induction on n. The base case is easy because the initial state is always A (aka the left half of the or clause). The inductive case shows that if we are at A or B after n steps, then after n+1 steps we will be at B (right) or A (left), respectively:

lemma M₃_AB_only {n} : ∃ tape,
  multistep M₃ n cfg₀ = some ⟨Λ.A, tape⟩
  ∨ multistep M₃ n cfg₀ = some ⟨Λ.B, tape⟩ :=
begin
  induction n with n hn,
  { existsi _,
    left,
    refl, },
  { cases hn with tape_n hn,
    cases hn; existsi _,
    {
      right,
      rw [multistep, function.iterate_succ_apply', ← multistep,
          hn, step', option.bind, turing.TM0.step],
      simp,
      existsi _,
      existsi _,
      split; refl, },
    {
      left,
      rw [multistep, function.iterate_succ_apply', ← multistep,
          hn, step', option.bind, turing.TM0.step],
      simp,
      existsi _,
      existsi _,
      split; refl, },
  },
end

(Again, reading these proofs non-interactively isn’t ideal, try the Lean web editor.)

Now that we know that the machine is always in state A or state B, it’s easy to prove that it doesn’t halt, using the theorem option.no_confusion to show that the only possible states some A and some B are never equal to the halting state none:

theorem M₃_not_halts : ¬ halts M₃ :=
begin
  rintro ⟨n, hn⟩,
  cases M₃_AB_only with tape h_tape,
  cases h_tape; {
    rw h_tape at hn,
    exact option.no_confusion hn,
  },
end

So there we have it, a Turing machine which loops forever …doesn’t halt!

This is pretty obvious, though maybe someday proofs like these could be automatically derived for more complicated machines.2 But mostly this was just a fun way for me to learn some Lean!

  1. Lean makes it easy to type Greek letters and math symbols in your code!

    E.g. \Lambda → Λ, \ex → ∃, … ↩

  2. Of course, there can be no general algorithm for generating such proofs, since it would solve the impossible halting problem. ↩