Post's theorem for recursive languages

Post's theorem: a predicate whose positive and negative instances are both recursively enumerable is computable; in language terms, a language that is RE and co-RE is recursive. We package it both at the computability level (ComputablePred) and at the recursive-language level (is_Recursive).

The bridge to is_Recursive goes through the tape-output decider construction (is_Recursive_of_computable_decide): a ComputablePred membership yields a total computable decider, which yields an always-halting TM0 decider.

Main results

• REPred_mem_of_is_RE — membership in an RE language is an REPred.
• computablePred_of_isRE_of_isRE_compl — RE ∩ co-RE ⟹ computable membership.
• is_Recursive_of_isRE_of_isRE_compl — RE ∩ co-RE ⟹ recursive.
• Recursive_membership_computable — the fixed-language corollary that every recursive language has a computable membership predicate.

theorem REPred_mem_of_is_RE {T : Type} [DecidableEq T] [Primcodable T] {L : Language T} (hL : is_RE L) : REPred fun (w : List T) => w ∈ L

For any recursively enumerable language over a Primcodable alphabet, membership is a recursively enumerable predicate. This is the search over derivation sequences made uniform via grammarTest.

theorem computablePred_of_isRE_of_isRE_compl {T : Type} [DecidableEq T] [Primcodable T] {L : Language T} (h1 : is_RE L) (h2 : is_RE Lᶜ) : ComputablePred fun (w : List T) => w ∈ L

Post's theorem (RE ∩ co-RE = recursive), computability form. A language that is recursively enumerable and whose complement is recursively enumerable has computable membership.

theorem is_Recursive_of_isRE_of_isRE_compl {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L : Language T} (h1 : is_RE L) (h2 : is_RE Lᶜ) : is_Recursive L

Post's theorem, recursive form. A language that is recursively enumerable and whose complement is recursively enumerable is recursive (decided by an always-halting TM0).

theorem Recursive_membership_computable {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L : Language T} (hL : is_Recursive L) : ComputablePred fun (w : List T) => w ∈ L

Every recursive language has a computable membership predicate.

This is a fixed-language consequence of Post's theorem and is useful when building closure constructions from already-given recursive languages. It is not the uniform encoded-device membership property; that property is proved from raw decider codes in Recursive.Decidability.Membership.