feat(Automata): Transducers (#650)

Adds a class for transducers and a first implementation based on `NA`.

Author: fmontesi

Cslib.lean

@@ -16,13 +16,15 @@ public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.NA.BuchiEquiv
 public import Cslib.Computability.Automata.NA.BuchiInter
 public import Cslib.Computability.Automata.NA.Concat
+public import Cslib.Computability.Automata.NA.EpsilonTransducer
 public import Cslib.Computability.Automata.NA.Hist
 public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.Consensus
 public import Cslib.Computability.Distributed.FLP.ZeroConsensus

Cslib/Computability/Automata/NA/EpsilonTransducer.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.Transducers.Transducer
+public import Cslib.Foundations.Semantics.LTS.HasTau
+
+/-! # Nondeterministic finite ε-transducers
+
+Transducers based on `NA` with an invisible symbol in their input and output alphabets.
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata.NA
+
+/-- A nondeterministic ε-transducer of finite strings where the input and output alphabets include
+an invisible symbol, modelled as `HasTau.τ` (typically called `ε`). -/
+structure εTransducer (State InSymbol OutSymbol : Type*)
+    extends NA State (InSymbol × OutSymbol) where
+  /-- The set of accepting states. -/
+  accept : Set State
+
+/-- Removes all `τ`s from a list. -/
+@[scoped grind =]
+def _root_.List.dropTaus [HasTau α] [DecidableEqTau α] (l : List α) : List α :=
+  l.filter (· ≠ HasTau.τ)
+
+variable [HasTau InSymbol] [HasTau OutSymbol]
+
+namespace εTransducer
+
+/-- An `εTransducer` translates `xs` into `ys` from state `s` to state `s'` if there is a
+multistep transition from `s` to `s'` whose visible projection is `(xs, ys)`.
+`MTransl` is short for Multistep Translation relation.
+-/
+def MTransl [DecidableEqTau InSymbol] [DecidableEqTau OutSymbol]
+    (a : εTransducer State InSymbol OutSymbol) (s : State)
+    (xs : List InSymbol) (ys : List OutSymbol) (s' : State) : Prop :=
+  ∃ μs, a.MTr s μs s' ∧ (μs.map Prod.fst |>.dropTaus) = xs ∧ (μs.map Prod.snd |>.dropTaus) = ys
+
+/-- An `NA.εTransducer` translates a finite string `xs` into a finite string `ys` if it has
+a multistep transition whose visible projection is `(xs, ys)`.
+
+This is the standard string translation performed by nondeterministic transducers, where
+`HasTau.τ` symbols (epsilon transitions) are ignored in the input and output. -/
+instance [DecidableEqTau InSymbol] [DecidableEqTau OutSymbol] :
+    Transducer (εTransducer State InSymbol OutSymbol) InSymbol OutSymbol where
+  Translates a xs ys := ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTransl s xs ys s'
+
+/-- Composition of multistep translations. -/
+theorem MTransl.comp [DecidableEqTau InSymbol] [DecidableEqTau OutSymbol]
+    {a : εTransducer State InSymbol OutSymbol}
+    {s₁ s₂ s₃ : State} {xs xs' : List InSymbol} {ys ys' : List OutSymbol} :
+    a.MTransl s₁ xs ys s₂ → a.MTransl s₂ xs' ys' s₃ →
+    a.MTransl s₁ (xs ++ xs') (ys ++ ys') s₃ := by
+  intro ⟨μs₁, h₁, e₁⟩ ⟨μs₂, h₂, e₂⟩
+  refine ⟨μs₁ ++ μs₂, LTS.MTr.comp a.toLTS h₁ h₂, ?_⟩
+  grind
+
+end εTransducer
+
+end Cslib.Automata.NA

Cslib/Computability/Automata/Transducers/Transducer.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Transducers -/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+/-- A `Transducer` is an automaton that translates strings (lists of symbols, from an input to an
+output alphabet). -/
+class Transducer (A : Type u) (InSymbol OutSymbol : outParam (Type v)) where
+  /-- The string `xs` can be translated into `ys` by `a`. -/
+  Translates (a : A) (xs : List InSymbol) (ys : List OutSymbol) : Prop
+
+@[inherit_doc]
+scoped notation xs "[" a "]" ys => Transducer.Translates a xs ys
+
+end Cslib.Automata

Cslib/Foundations/Semantics/LTS/HasTau.lean

@@ -23,6 +23,9 @@ class HasTau (Label : Type v) where
   /-- The internal transition label, also known as τ. -/
   τ : Label
 
+/-- Checking whether an element is `τ` is decidable. -/
+abbrev DecidableEqTau (α : Type*) [HasTau α] := ∀ a : α, Decidable (a = HasTau.τ)
+
 namespace LTS
 
 /-- Saturated τ-transition relation. -/