TM recognizability for languages over Empty

When T = Empty, every language over T is trivially TM-recognizable, since List Empty = {[]} and any language is either ∅ or {[]}.

Key results

• alwaysHaltTM_halts: the trivial halting TM halts on every input.
• neverHaltTM_diverges: the trivial moving TM never halts.
• is_TM_of_empty: every language over Empty is TM-recognizable.

theorem List.eq_nil_of_empty (l : List Empty) : l = []

Every list of Empty elements is the empty list.

noncomputable def alwaysHaltTM (Γ : Type) [Inhabited Γ] : Turing.TM0.Machine Γ Unit

A TM that always halts (transition function returns none).

Equations

• alwaysHaltTM Γ x✝¹ x✝ = none

theorem alwaysHaltTM_halts (Γ : Type) [Inhabited Γ] (l : List Γ) : (Turing.TM0.eval (alwaysHaltTM Γ) l).Dom

noncomputable def neverHaltTM (Γ : Type) [Inhabited Γ] : Turing.TM0.Machine Γ Unit

A TM that loops forever (always moves right).

Equations

• neverHaltTM Γ x✝¹ x✝ = some ((), Turing.TM0.Stmt.move Turing.Dir.right)

theorem neverHaltTM_diverges (Γ : Type) [Inhabited Γ] (l : List Γ) : ¬(Turing.TM0.eval (neverHaltTM Γ) l).Dom

theorem is_TM_of_empty (L : Language Empty) : is_TM L

Any language over the empty type is TM-recognizable.