Recursive Inclusions

This file proves that recursive languages are Turing-recognisable and hence recursively enumerable.

Main results

• is_Recursive_implies_is_TM — every recursive language is TM-recognisable.
• is_Recursive_implies_is_RE — every recursive language is recursively enumerable.
• Recursive_subset_RE — the class of recursive languages is contained in RE.

def liftCfg {Γ Λ : Type} [Inhabited Γ] (c : Turing.TM0.Cfg Γ Λ) : Turing.TM0.Cfg Γ (Λ ⊕ Unit)

Lift a TM0 configuration from state type Λ to Λ ⊕ Unit by wrapping the state in Sum.inl.

Equations

• liftCfg c = { q := Sum.inl c.q, Tape := c.Tape }

def decider_to_recognizer {Γ Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) : Turing.TM0.Machine Γ (Λ ⊕ Unit)

Construct a recogniser TM from a decider TM with acceptance predicate. The recogniser halts iff the decider would halt in an accepting state; when the decider rejects, the recogniser enters an infinite loop.

Equations

• One or more equations did not get rendered due to their size.
• decider_to_recognizer M accept (Sum.inr PUnit.unit) γ = some (Sum.inr (), Turing.TM0.Stmt.move Turing.Dir.right)

theorem recognizer_step_of_decider_step {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (c c' : Turing.TM0.Cfg Γ Λ) (hs : c' ∈ Turing.TM0.step M c) : Turing.TM0.step (decider_to_recognizer M accept) (liftCfg c) = some (liftCfg c')

theorem recognizer_reaches_of_decider_reaches {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (c c' : Turing.TM0.Cfg Γ Λ) (hr : Turing.Reaches (Turing.TM0.step M) c c') : Turing.Reaches (Turing.TM0.step (decider_to_recognizer M accept)) (liftCfg c) (liftCfg c')

theorem recognizer_halts_of_accept {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (c : Turing.TM0.Cfg Γ Λ) (hstep : Turing.TM0.step M c = none) (hacc : accept c.q = true) : Turing.TM0.step (decider_to_recognizer M accept) (liftCfg c) = none

theorem recognizer_inr_reaches_inr {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (tape : Turing.Tape Γ) (c' : Turing.TM0.Cfg Γ (Λ ⊕ Unit)) (hr : Turing.Reaches (Turing.TM0.step (decider_to_recognizer M accept)) { q := Sum.inr (), Tape := tape } c') : c'.q = Sum.inr ()

theorem recognizer_inr_never_halts {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (tape : Turing.Tape Γ) : ¬(Turing.eval (Turing.TM0.step (decider_to_recognizer M accept)) { q := Sum.inr (), Tape := tape }).Dom

theorem recognizer_diverges_of_reject {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (c : Turing.TM0.Cfg Γ Λ) (l : List Γ) (hreach : Turing.Reaches (Turing.TM0.step M) (Turing.TM0.init l) c) (hstep : Turing.TM0.step M c = none) (hrej : accept c.q = false) : ¬(Turing.eval (Turing.TM0.step (decider_to_recognizer M accept)) (Turing.TM0.init l)).Dom

theorem recognizer_eval_dom_of_accept {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (l : List Γ) (hdom : (Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).Dom) (hacc : accept ((Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).get hdom).q = true) : (Turing.eval (Turing.TM0.step (decider_to_recognizer M accept)) (Turing.TM0.init l)).Dom

theorem recognizer_eval_not_dom_of_reject {Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (l : List Γ) (hdom : (Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).Dom) (hrej : accept ((Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).get hdom).q = false) : ¬(Turing.eval (Turing.TM0.step (decider_to_recognizer M accept)) (Turing.TM0.init l)).Dom

theorem recognizer_tm0_eval_iff {T Γ Λ : Type} [Inhabited Γ] [Inhabited Λ] (L : Language T) (input : List T → List Γ) (M : Turing.TM0.Machine Γ Λ) (accept : Λ → Bool) (halts : ∀ (w : List T), (Turing.eval (Turing.TM0.step M) (Turing.TM0.init (input w))).Dom) (hmem : ∀ (w : List T) (h : (Turing.eval (Turing.TM0.step M) (Turing.TM0.init (input w))).Dom), w ∈ L ↔ accept ((Turing.eval (Turing.TM0.step M) (Turing.TM0.init (input w))).get h).q = true) (w : List T) : w ∈ L ↔ (Turing.TM0.eval (decider_to_recognizer M accept) (input w)).Dom

theorem is_Recursive_implies_is_TM {T : Type} [Fintype T] {L : Language T} (hL : is_Recursive L) : is_TM L

theorem is_Recursive_implies_is_RE {T : Type} [DecidableEq T] [Fintype T] {L : Language T} (hL : is_Recursive L) : is_RE L

Every recursive language is recursively enumerable.

theorem Recursive_subset_RE {T : Type} [DecidableEq T] [Fintype T] : Recursive ⊆ RE

The class of recursive languages is a subset of the class of RE languages.