Turing machines recognize exactly the recursively enumerable languages (TM = RE)

Statement

A language is recursively enumerable (type-0, generated by an unrestricted grammar) if and only if it is recognized by a Turing machine. The class of TM-recognizable languages equals the class of recursively enumerable languages.

In Lean

The two inclusions TM_subset_RE and RE_subset_TM assemble these. The grammar-to-machine translation is powered by the GrammarToTM and TMToGrammar constructions and the composable search-procedure DSL.

The RE ⊆ TM engine: compiling searches to machines

The forward direction is powered by a reusable bridge that compiles any computable search procedure into a Turing machine — see Compiling search procedures to Turing machines. Grammar membership is itself a search (enumerate derivation sequences, test each with the computable grammarTest), so feeding that search to the bridge yields a machine recognizing the grammar’s language. The same bridge is what the RE closure proofs reuse — they just build a different computable test.

Proof idea

RE ⊆ TM (re_implies_tm): given a grammar for L, grammar_equivalent_finiteNT first restricts it to finitely many nonterminals; membership is then the search “∃ a derivation sequence seq with grammarTest g' seq w” (sound and complete by grammarTest_sound / grammarTest_complete). search_is_partrec turns this Computable₂ test into a partial-recursive ToPartrec.Code, which code_implies_isTM_direct compiles to a TM0 machine (the search-to-machine bridge).

TM ⊆ RE (tm_recognizable_implies_re): the machine has tape alphabet T ⊕ Γ (input symbols plus an existential finite work alphabet). The construction tmToGrammar builds an unrestricted grammar whose sentential forms encode the machine’s configurations, with rules mirroring the transition function, sound and complete via tmToGrammar_halts_of_generates / tmToGrammar_generates_of_halts. pullbackGrammar then restricts this grammar along the fixed inclusion Sum.inl : T → T ⊕ Γ, so the result generates exactly the input words the machine accepts.

Keywords / also known as

Turing machines equal recursively enumerable languages, TM = RE, type-0 languages, unrestricted grammars equal Turing machines, RE recognizable iff TM recognizable, Chomsky type-0 automaton characterization, semi-decidable languages.

Formalized in Lean 4 with Mathlib, in Langlib.