LanglibRecursive Closure Under Concatenation #
This file proves that recursive languages are closed under concatenation.
The decider searches the finitely many splits of the input word. At split n, it checks
membership of w.take n in the left language and w.drop n in the right language.
theorem
is_Recursive_concatenation
{T : Type}
[DecidableEq T]
[Fintype T]
[Primcodable T]
{L₁ L₂ : Language T}
(h₁ : is_Recursive L₁)
(h₂ : is_Recursive L₂)
:
is_Recursive (L₁ * L₂)
Recursive languages over finite, primcodable alphabets are closed under concatenation.
The class of recursive languages is closed under concatenation.