Turing-Recognizable Languages Are Exactly RE Languages

This module packages the two existing directions:

• re_implies_tm: unrestricted grammars are TM-recognizable.
• TM_subset_RE: TM-recognizable languages are generated by unrestricted grammars.

Key results

• TM_eq_RE: equality of TM-recognizable and recursively enumerable languages.
• is_TM_iff_is_RE: pointwise membership equivalence.

theorem TM_eq_RE {T : Type} [DecidableEq T] [Fintype T] : TM = RE

The class of TM-recognizable languages is exactly the class of recursively enumerable languages.

theorem is_TM_iff_is_RE {T : Type} [DecidableEq T] [Fintype T] (L : Language T) : is_TM L ↔ is_RE L

Pointwise version of TM_eq_RE.