Computability of Membership

This file proves that membership in a recursive language is computable.

Main results

• Recursive_membership_computable — membership in a recursive language is a ComputablePred (genuine computability in the theory-of-computation sense).

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

Membership in a recursive language is computable. This is the genuine theory-of-computation statement: from an always-halting decider we obtain a ComputablePred, via Post's theorem applied to L and its (recursive, hence recognizable) complement.

This mirrors computablePred_mem_of_is_CS for context-sensitive languages.