Nondeterministic finite ε-transducers

Transducers based on NA with an invisible symbol in their input and output alphabets.

structure Cslib.Automata.NA.εTransducer (State : Type u_1) (InSymbol : Type u_2) (OutSymbol : Type u_3) extends Cslib.Automata.NA State (InSymbol × OutSymbol) : Type (max (max u_1 u_2) u_3)

A nondeterministic ε-transducer of finite strings where the input and output alphabets include an invisible symbol, modelled as HasTau.τ (typically called ε).

• Tr : State → InSymbol × OutSymbol → State → Prop
• start : Set State
• accept : Set State

  The set of accepting states.

def List.dropTaus {α : Type u_1} [Cslib.HasTau α] [Cslib.DecidableEqTau α] (l : List α) : List α

Removes all τs from a list.

Equations

• l.dropTaus = List.filter (fun (x : α) => decide (x ≠ Cslib.HasTau.τ)) l

def Cslib.Automata.NA.εTransducer.MTransl {InSymbol : Type u_1} {OutSymbol : Type u_2} [HasTau InSymbol] [HasTau OutSymbol] {State : Type u_3} [DecidableEqTau InSymbol] [DecidableEqTau OutSymbol] (a : εTransducer State InSymbol OutSymbol) (s : State) (xs : List InSymbol) (ys : List OutSymbol) (s' : State) : Prop

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.

Equations

• a.MTransl s xs ys s' = ∃ (μs : List (InSymbol × OutSymbol)), a.MTr s μs s' ∧ (List.map Prod.fst μs).dropTaus = xs ∧ (List.map Prod.snd μs).dropTaus = ys

@[implicit_reducible]

instance Cslib.Automata.NA.εTransducer.instTransducerOfDecidableEqTau {InSymbol OutSymbol : Type u_1} [HasTau InSymbol] [HasTau OutSymbol] {State : Type u_2} [DecidableEqTau InSymbol] [DecidableEqTau OutSymbol] : Transducer (εTransducer State InSymbol OutSymbol) InSymbol OutSymbol

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Automata.NA.εTransducer.MTransl.comp {InSymbol : Type u_2} {OutSymbol : Type u_3} [HasTau InSymbol] [HasTau OutSymbol] {State : Type u_1} [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₃

Composition of multistep translations.