Recursive Closure Under Kleene Star

This file proves that recursive languages are closed under Kleene star.

The decider builds a dynamic-programming table for the input word w. The table entry at index j records whether the prefix w.take j belongs to L∗; to fill entry j + 1, it searches all earlier cut positions i and checks whether the left prefix is already accepted and the nonempty block w.drop i |>.take (j + 1 - i) belongs to L.

theorem is_Recursive_star {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L : Language T} (hL : is_Recursive L) : is_Recursive (KStar.kstar L)

Recursive languages over finite, primcodable alphabets are closed under Kleene star.

theorem Recursive_closedUnderKleeneStar {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderKleeneStar is_Recursive

The class of recursive languages is closed under Kleene star.