Regular Languages Included in Recursive Languages

This file proves that every regular language over a finite, encodable alphabet is recursive, by composing the existing computable regular-membership predicate with the generic construction of a recursive language from a total computable Boolean decider.

Main results

• is_Recursive_of_isRegular — every Mathlib-regular language is recursive.
• is_Recursive_of_is_RG — every right-regular grammar language is recursive.
• RG_subclass_Recursive — class-level inclusion RG ⊆ Recursive.

theorem is_Recursive_of_isRegular {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] {L : Language T} (hL : L.IsRegular) : is_Recursive L

Every Mathlib-regular language over a finite alphabet is recursive.

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

Every right-regular grammar language over a finite alphabet is recursive.

theorem RG_subclass_Recursive {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : RG ⊆ Recursive

The regular languages are included in the recursive languages.