Langlib

Langlib.Classes.Recursive.Closure.Quotient

Recursive Non-Closure Under Right Quotient #

Recursive languages are not closed under right quotient. This follows from the stronger counterexample for right quotient by a regular language, since every regular language is recursive.

source
theorem Recursive_notClosedUnderRightQuotient :
¬ClosedUnderRightQuotient is_Recursive

Recursive languages are not closed under right quotient.

source
theorem Recursive_notClosedUnderRightQuotient_of_embedding {α : Type} [Fintype α] (e : Bool ↪ α) :
¬ClosedUnderRightQuotient is_Recursive

Recursive languages are not closed under arbitrary right quotient over any finite alphabet into which the binary witness alphabet embeds.

source
theorem Recursive_notClosedUnderRightQuotient_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) :
¬ClosedUnderRightQuotient is_Recursive

Recursive languages are not closed under arbitrary right quotient over any finite alphabet with at least two symbols.