Weighted DFAs and Deterministic FSTs

Stream: CSLib

[Liam Schilling]

Hello!

I am working on a contribution (one of my first) in Computability defining Weighted DFAs here:

https://github.com/LiamSchilling/mathlib4/blob/rational-and-subsequential-transductions/Mathlib/Computability/WDFA.lean

I want to build up to defining subsequential and rational string transductions, then proving the Choffrut characterization.

I know it's advisable for PRs to be minimal, and in general I'm wondering what's the best way to go about it. It's not long yet, but it may be after adding the simp lemmas and lemmas relating WDFAs to acceptor DFAs.

Thank you :)

[Snir Broshi]

Hello :wave:
You might want to consider #CSLib instead

[Chris Henson]

cc @Rudy Peterson who I believe had mentioned some related work and @Ching-Tsun Chou who has been working on automata in CSLib

[Liam Schilling]

Thank you for the direction! This is my first time hearing of CSLib.

[Ching-Tsun Chou]

You can start by browsing the code here:
https://github.com/leanprover/cslib/tree/main/Cslib/Computability/Automata
I'm porting the results from an earlier project into CSLib:
https://github.com/ctchou/AutomataTheory
whose README indicates which results are already in CSLib.

[Ching-Tsun Chou]

There was a talk about CSLib in the just-concluded "Lean Together":
#Lean Together 2026 > Fabrizio Montesi - CSLib: The Lean Computer Science Library
I'm told the video recording will appear on YouTube next week.

[Ching-Tsun Chou]

@Liam Schilling It would be nice if you can outline what definitions and theorems from the theory of weighted automata you plan to formalize. That will help people like myself who are not already familiar with the theory to get a sense of (so to speak) the lay of the land.

[Liam Schilling]

Hello! My first formalization target is the class of subsequential transductions, which are realized by deterministic FSTs. Then, I will prove the Choffrut Theorem, which is the transducer version of Myhill-Nerode.

My motivation for capturing weighted automata with Transducer is that they immediately specialize to the desired FST definition without being any more complicated. Similarly, every transducer model within the rational class (deterministic FST; nondeterministic FST; bimachine) has an immediate generalization from string outputs (the free monoid) to outputs from any monoid. In this sense, defining Transducer in terms of semigroups and monoids instead of assuming we are working with the free monoid is a two birds/one stone situaion: we get both weighted automata and string-to-string transducers.

I also wonder if this discussion should be moved to #CSLib.

[Liam Schilling]

As for the PR, I agree with your comment that it might be better to wait until some transducer models are defined, so that we will see if the current definition is the most convenient.

[Notification Bot]

This topic was moved here from #mathlib4 > Weighted DFAs and Deterministic FSTs by Kim Morrison.

[Liam Schilling]

I have drafted the PR until I define the weighted automaton and bimachine models, and implement Transducer for them. This should help ensure that we have the best definition of Transducer. There were other design choices I could have made that I will outline here for if anybody has thoughts:

• No accumulators: have weights from a Monoid and give Transducer only one field transduce : T -> List Symbol -> Weight. This is simpler, and the Monoid restriction should be fine because there are no practical situations I can think of where weights are not from a Monoid. However, this limits performance optimizations in cases like transduce t xs * y where transduce t xs is a very long list. Ideally, y would be passed as an accumulator so that transduce t xs is only constructed once (recall List.append unfolds the left-hand list).
• Current definition: have weights from a Semigroup and give Transducer the function transduceFrom that takes a left and right accumulator. This is still fairly simple and it allows some of the optimizations. However, once implemented, the direction of associativity of multiplication cannot be changed, even for types where the other direction is preferred. Also, for Semigroups that are not Monoids, transduceFrom is limited in expressivity because it must have both a left and right accumulator where an empty weight (1) cannot be provided.
• Separate functions for left and right accumulators: have weights from a Semigroup and give Transducer two functions transduceFromLeft and transduceFromRight which take a left and right accumulator respectively. This is the least simple definition. However, it allows both directions of associativity of multiplication to be implemented at once. Also, it avoids the expressivity limitation of the previous transduceFrom.

I am leaning toward the third definition because it is the most general and the most flexible to implementation.

[Ching-Tsun Chou]

I don't know enough about the subject matter to make any concrete suggestions. But it seems to me that the best way to exercise your definitions is to try to prove some not-entirely-trivial theorems. Then you'll find out quickly how well your definitions work.

[Chris Henson]

Yes, for adding new definitions like this there is a bit of a bootstrapping problem of actually using your definitions to gain confidence that they are both correct and ergonomic. What I think would be most helpful, for both yourself and the reviewers, is to follow the above advice and see how these definitions play out in practice. Most of the developments in CSLib started this way, spending a lot of time in a fork or other personal repo until reaching a non-trivial theorem.

[Chris Henson]

Also if you're aware of any related formalizations in other proof assistants, this is extremely helpful for reviewing purposes. When thinking about the first lambda calculi definitions we added, I spent a lot of time contrasting formalizations in Rocq and Agda.