module public import Langlib.Classes.ContextSensitive.Closure.IntersectionRegular public import Langlib.Classes.ContextSensitive.Closure.EpsFreeHomomorphism public import Langlib.Classes.ContextSensitive.Inclusion.Recursive public import Langlib.Classes.Recursive.Closure.IntersectionRegular public import Langlib.Classes.Recursive.Closure.InverseHomomorphism public import Langlib.Classes.Recursive.Basics.Post public import Langlib.Classes.Recursive.Inclusion.StrictRecursivelyEnumerable public import Langlib.Classes.RecursivelyEnumerable.Examples.Halting public import Langlib.Classes.Regular.Closure.Concatenation public import Langlib.Classes.Regular.Closure.Homomorphism public import Langlib.Classes.Regular.Closure.Star public import Langlib.Classes.Regular.Examples.SingletonWord public import Langlib.Grammars.NonContracting.ErasingImage public import Langlib.Utilities.ClosurePredicates import Mathlib.Tactic @[expose] public section /-! # Context-Sensitive Languages Are Not Closed Under Regular Right Quotient This is the standard Hopcroft--Ullman padding reduction. The noncontracting simulation of an unrestricted grammar appends padding to the generated word. Intersecting with the regular language `some* none*` keeps representatives whose padding is a suffix; quotienting by `none*` then exposes the source language. Instantiating the source with the unary halting language contradicts the fact that every context-sensitive language is recursive. -/ open Grammar.ErasingImage namespace CSQuotientRegular private def symbolStar {A : Type} (a : A) : Language A := KStar.kstar ({[a]} : Language A) private lemma flatten_singleton_of_mem {A : Type} (a : A) : ∀ blocks : List (List A), (∀ y ∈ blocks, y ∈ ({[a]} : Language A)) → blocks.flatten = List.replicate blocks.length a | [], _ => by simp | b :: bs, hmem => by have hb : b = [a] := Set.mem_singleton_iff.mp (hmem b (by simp)) have hbs : ∀ y ∈ bs, y ∈ ({[a]} : Language A) := by intro y hy exact hmem y (by simp [hy]) rw [List.flatten_cons, hb, flatten_singleton_of_mem a bs hbs] simp [List.replicate_succ] private lemma symbolStar_mem_iff_replicate {A : Type} (a : A) {w : List A} : w ∈ symbolStar a ↔ ∃ k : ℕ, w = List.replicate k a := by constructor · intro hw rw [symbolStar, Language.mem_kstar] at hw rcases hw with ⟨blocks, rfl, hblocks⟩ exact ⟨blocks.length, flatten_singleton_of_mem a blocks hblocks⟩ · rintro ⟨k, rfl⟩ rw [symbolStar, Language.mem_kstar] refine ⟨List.replicate k [a], ?_, ?_⟩ · have hmem : ∀ y ∈ List.replicate k [a], y ∈ ({[a]} : Language A) := by intro y hy exact Set.mem_singleton_iff.mpr (List.eq_of_mem_replicate hy) calc List.replicate k a = List.replicate (List.replicate k [a]).length a := by rw [List.length_replicate] _ = (List.replicate k [a]).flatten := (flatten_singleton_of_mem a (List.replicate k [a]) hmem).symm · intro y hy exact Set.mem_singleton_iff.mpr (List.eq_of_mem_replicate hy) private lemma symbolStar_regular {A : Type} (a : A) : (symbolStar a).IsRegular := (singletonWordLanguage_isRegular [a]).kstar' private def someStar : Language (Option Unit) := symbolStar (some ()) private def noneStar : Language (Option Unit) := symbolStar none private def trailingShape : Language (Option Unit) := someStar * noneStar private lemma someStar_regular : someStar.IsRegular := symbolStar_regular (some ()) private lemma noneStar_regular : noneStar.IsRegular := symbolStar_regular none private lemma trailingShape_regular : trailingShape.IsRegular := someStar_regular.mul' noneStar_regular private lemma map_some_mem_someStar (w : List Unit) : w.map some ∈ someStar := by apply (symbolStar_mem_iff_replicate (some ())).mpr refine ⟨w.length, ?_⟩ induction w with | nil => rfl | cons _ w ih => simp [List.replicate_succ, ih] private lemma someStar_eq_map_some {x : List (Option Unit)} (hx : x ∈ someStar) : ∃ w : List Unit, x = w.map some := by rcases (symbolStar_mem_iff_replicate (some ())).mp hx with ⟨k, rfl⟩ exact ⟨List.replicate k (), by simp⟩ private lemma trailingShape_mem (w : List Unit) (k : ℕ) : w.map some ++ List.replicate k none ∈ trailingShape := by rw [trailingShape, Language.mem_mul] exact ⟨w.map some, map_some_mem_someStar w, List.replicate k none, (symbolStar_mem_iff_replicate none).mpr ⟨k, rfl⟩, rfl⟩ private lemma flatMap_map_some (w : List Unit) : (w.map some).flatMap erasePadding = w := by induction w with | nil => rfl | cons u w ih => cases u; simp [erasePadding, ih] private lemma flatMap_replicate_none (k : ℕ) : (List.replicate k (none : Option Unit)).flatMap erasePadding = [] := by induction k with | zero => rfl | succ k ih => simp [List.replicate_succ, erasePadding, ih] private noncomputable def paddedLanguage (g : grammar Unit) : Language (Option Unit) := grammar_language (erasingImageGrammar g) private noncomputable def paddedNumerator (g : grammar Unit) : Language (Option Unit) := paddedLanguage g ⊓ trailingShape private theorem paddedNumerator_is_CS (g : grammar Unit) : is_CS (paddedNumerator g) := by apply CS_inter_regular (paddedLanguage g) trailingShape · exact is_CS_of_is_noncontracting ⟨erasingImageGrammar g, erasingImageGrammar_noncontracting g, rfl⟩ · exact trailingShape_regular private theorem exposed_padded_eq_map (g : grammar Unit) : Language.rightQuotient (paddedNumerator g) noneStar ⊓ someStar = Language.map some (grammar_language g) := by ext x constructor · rintro ⟨⟨v, hv, hxv⟩, hxsome⟩ rcases someStar_eq_map_some hxsome with ⟨w, rfl⟩ rcases (symbolStar_mem_iff_replicate none).mp hv with ⟨k, rfl⟩ have hproject := erasingImageGrammar_generates_project g hxv.1 have hw : w ∈ grammar_language g := by simpa [List.flatMap_append, flatMap_map_some, flatMap_replicate_none] using hproject exact ⟨w, hw, rfl⟩ · rintro ⟨w, hw, rfl⟩ rcases erasingImageGrammar_generates_padded g hw with ⟨k, hk⟩ refine ⟨?_, map_some_mem_someStar w⟩ refine ⟨List.replicate k none, (symbolStar_mem_iff_replicate none).mpr ⟨k, rfl⟩, ?_⟩ exact ⟨hk, trailingShape_mem w k⟩ private lemma map_some_computable : Computable (fun w : List Unit => w.map some) := by exact (Primrec.list_map (f := fun w : List Unit => w) (g := fun (_ : List Unit) (u : Unit) => some u) Primrec.id (Primrec₂.mk (Primrec.option_some.comp Primrec.snd))).to_comp private theorem recursive_of_recursive_map_some (h : is_Recursive (Language.map some haltingUnaryLanguage)) : is_Recursive haltingUnaryLanguage := by obtain ⟨f, hf, hs⟩ := ComputablePred.computable_iff.mp (Recursive_membership_computable h) refine is_Recursive_of_computable_decide haltingUnaryLanguage (fun w => f (w.map some)) (hf.comp map_some_computable) ?_ intro w have hmap : w ∈ haltingUnaryLanguage ↔ w.map some ∈ Language.map some haltingUnaryLanguage := by constructor · intro hw exact ⟨w, hw, rfl⟩ · rintro ⟨v, hv, heq⟩ have hvw : v = w := by exact List.map_injective_iff.mpr (Option.some_injective Unit) heq simpa [hvw] using hv have hdec : w.map some ∈ Language.map some haltingUnaryLanguage ↔ f (w.map some) = true := by exact iff_of_eq (congrFun hs (w.map some)) exact hmap.trans hdec end CSQuotientRegular open CSQuotientRegular /-- Context-sensitive languages are not closed under right quotient with regular languages. -/ public theorem CS_notClosedUnderRightQuotientWithRegular : ¬ ClosedUnderRightQuotientWithRegular (α := Option Unit) is_CS := by intro hclosed obtain ⟨g, hg⟩ := haltingUnaryLanguage_RE have hquot : is_CS (Language.rightQuotient (paddedNumerator g) noneStar) := hclosed (paddedNumerator g) (paddedNumerator_is_CS g) noneStar noneStar_regular have hexposed : is_CS (Language.rightQuotient (paddedNumerator g) noneStar ⊓ someStar) := CS_inter_regular _ someStar hquot someStar_regular have hmapped : is_CS (Language.map some haltingUnaryLanguage) := by rw [← hg, ← exposed_padded_eq_map] exact hexposed exact haltingUnaryLanguage_not_Recursive (recursive_of_recursive_map_some (is_Recursive_of_is_CS hmapped)) private theorem CS_of_map {α β : Type} (f : α → β) (L : Language α) (hL : is_CS L) : is_CS (Language.map f L) := by have h := is_CS_homomorphicImage_epsfree L (fun a => [f a]) (fun _ => by simp) hL rwa [Language.homomorphicImage, Language.subst_singletons_eq_map] at h private theorem Language.map_rightQuotient_injective {α β : Type} {f : α → β} (hf : Function.Injective f) (L R : Language α) : Language.map f (Language.rightQuotient L R) = Language.rightQuotient (Language.map f L) (Language.map f R) := by ext w constructor · rintro ⟨u, ⟨v, hvR, huvL⟩, rfl⟩ exact ⟨v.map f, ⟨v, hvR, rfl⟩, ⟨u ++ v, huvL, by simp⟩⟩ · rintro ⟨v, ⟨v₀, hv₀R, hv⟩, ⟨z, hzL, hz⟩⟩ subst v have hz' : z.map f = w ++ v₀.map f := by simpa using hz obtain ⟨w₀, v₁, hz_eq, hw₀, hv₁⟩ := List.map_eq_append_iff.mp hz' have hv₁_eq : v₁ = v₀ := List.map_injective_iff.mpr hf hv₁ subst v₁ rw [← hw₀] exact ⟨w₀, ⟨v₀, hv₀R, by simpa [hz_eq] using hzL⟩, rfl⟩ private theorem recursive_of_recursive_map_injective {α β : Type} [Fintype α] [Fintype β] {f : α → β} (hf : Function.Injective f) (L : Language α) (h : is_Recursive (Language.map f L)) : is_Recursive L := by have hpre := is_Recursive_inverseHomomorphism (Language.map f L) (fun a => [f a]) h have hflat : ∀ w : List α, w.flatMap (fun a => [f a]) = w.map f := by intro w induction w with | nil => rfl | cons a w ih => simp [ih] have heq : ({w : List α | w.flatMap (fun a => [f a]) ∈ Language.map f L} : Language α) = L := by ext w change w.flatMap (fun a => [f a]) ∈ Language.map f L ↔ w ∈ L rw [hflat] constructor · rintro ⟨v, hv, hmap⟩ have : v = w := List.map_injective_iff.mpr hf hmap simpa [this] using hv · intro hw exact ⟨w, hw, rfl⟩ rwa [heq] at hpre /-- Context-sensitive languages are not closed under regular right quotient over any finite alphabet into which the binary witness alphabet embeds. -/ public theorem CS_notClosedUnderRightQuotientWithRegular_of_embedding {α : Type} [Fintype α] (e : Option Unit ↪ α) : ¬ ClosedUnderRightQuotientWithRegular (α := α) is_CS := by letI : DecidableEq α := Classical.decEq α letI : Primcodable α := Primcodable.ofEquiv (Fin (Fintype.card α)) (Fintype.truncEquivFin α).out intro hclosed obtain ⟨g, hg⟩ := haltingUnaryLanguage_RE have hnum : is_CS (Language.map e (paddedNumerator g)) := CS_of_map e (paddedNumerator g) (paddedNumerator_is_CS g) have hden : (Language.map e noneStar).IsRegular := noneStar_regular.map e have hquot : is_CS (Language.rightQuotient (Language.map e (paddedNumerator g)) (Language.map e noneStar)) := hclosed _ hnum _ hden rw [← Language.map_rightQuotient_injective e.injective] at hquot have hbase : is_Recursive (Language.rightQuotient (paddedNumerator g) noneStar) := recursive_of_recursive_map_injective e.injective _ (is_Recursive_of_is_CS hquot) have hexposed : is_Recursive (Language.rightQuotient (paddedNumerator g) noneStar ⊓ someStar) := Recursive_closedUnderIntersectionWithRegular _ hbase _ someStar_regular have hmapped : is_Recursive (Language.map some haltingUnaryLanguage) := by rw [← hg, ← exposed_padded_eq_map] exact hexposed exact haltingUnaryLanguage_not_Recursive (recursive_of_recursive_map_some hmapped) /-- Context-sensitive languages are not closed under regular right quotient over any finite alphabet with at least two symbols. -/ public theorem CS_notClosedUnderRightQuotientWithRegular_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ ClosedUnderRightQuotientWithRegular (α := α) is_CS := by let πW : Option Unit ≃ Fin (Fintype.card (Option Unit)) := Fintype.equivFin (Option Unit) let πA : α ≃ Fin (Fintype.card α) := Fintype.equivFin α have hWA : Fintype.card (Option Unit) ≤ Fintype.card α := by simpa using hα exact CS_notClosedUnderRightQuotientWithRegular_of_embedding (πW.toEmbedding.trans ((Fin.castLEEmb hWA).trans πA.symm.toEmbedding)) end