Recursive Non-Closure Under Right Quotient By A Regular Language

Recursive languages are not closed under right quotient by a regular language.

The counterexample encodes the unary halting problem. Over Bool, let the regular suffix language be false*. The recursive numerator consists of words false^n ++ [true] ++ false^k such that the program encoded by n halts within bounded time k. Quotienting by false* removes the bounded-time certificate and leaves exactly the unbounded unary halting language on prefixes false^n ++ [true].

theorem Recursive_notClosedUnderRightQuotientWithRegular : ¬ClosedUnderRightQuotientWithRegular is_Recursive

Recursive languages are not closed under right quotient by regular languages.

theorem Recursive_notClosedUnderRightQuotientWithRegular_of_embedding {α : Type} [Fintype α] (e : Bool ↪ α) : ¬ClosedUnderRightQuotientWithRegular is_Recursive

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

theorem Recursive_notClosedUnderRightQuotientWithRegular_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderRightQuotientWithRegular is_Recursive

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