Context-Free Languages Included in Recursive Languages

This file proves that every context-free language over a finite, encodable alphabet is recursive. The proof chooses an encoded CFG for the language, specializes the uniform encoded-CFG membership decider to that code, and then applies the generic construction of a recursive language from a total computable Boolean decider.

Main results

• is_Recursive_of_is_CF — every context-free language is recursive.
• CF_subset_Recursive — class-level inclusion CF ⊆ Recursive.

theorem is_Recursive_of_is_CF {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] {L : Language T} (hL : is_CF L) : is_Recursive L

Every context-free language over a finite alphabet is recursive.

theorem CF_subset_Recursive {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : CF ⊆ Recursive

The context-free languages are included in the recursive languages.