structure StringTransducer (α : Type u_1) (β : Type u_2) (σ : Type u_3) [Fintype α] [Fintype β] [Fintype σ] : Type (max (max u_1 u_2) u_3)

• start : σ
• accept : Finset σ
• step : σ → α → σ × List β
• final (q : σ) : q ∈ self.accept → List β

def StringTransducer.RewriteWordWithoutFinal {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Fintype α] [Fintype β] [Fintype σ] (𝓣 : StringTransducer α β σ) : σ → List α → σ × List β

Equations

• 𝓣.RewriteWordWithoutFinal x✝ [] = (x✝, [])
• 𝓣.RewriteWordWithoutFinal x✝ (a :: as) = match 𝓣.step x✝ a with | (q_next, head) => match 𝓣.RewriteWordWithoutFinal q_next as with | (q_last, tail) => (q_last, head ++ tail)

def StringTransducer.Generates {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Fintype α] [Fintype β] [Fintype σ] (𝓣 : StringTransducer α β σ) (source : List α) (target : List β) : Prop

Equations

• 𝓣.Generates source target = match 𝓣.RewriteWordWithoutFinal 𝓣.start source with | (q, w) => ∃ (h : q ∈ 𝓣.accept), target = w ++ 𝓣.final q h

def StringTransducer.map {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Fintype α] [Fintype β] [Fintype σ] (𝓣 : StringTransducer α β σ) (L : Language α) : Language β

Equations

• 𝓣.map L = {w : List β | ∃ u ∈ L, 𝓣.Generates u w}