Turing Machine Halting in Lean
I recently fooled around with the theoremproving 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 webbased 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+(mn), 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 noninteractively 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 noninteractively 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!

Lean makes it easy to type Greek letters and math symbols in your code!
E.g. \Lambda → Λ, \ex → ∃, … ↩

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