feat: define the Transducer class as recognizing a function from input strings to weights

[LiamSchilling]

This definition easily specializes to:

• weighted acceptors, by attaching an annihilator none to the weights
• functional string transducers, by having output strings as the weights
• partial functional string transducers, by having output strings with an annihilator none as the weights

The design is similar to the related Acceptor.lean

[ctchou]

What is the purpose of the T and t : T arguments here and below? They never seem to be used.

[LiamSchilling]

T is a type of transducers implementing the type class Transducer. The function recognized by some transducer t : T can then be accessed via transduce t.

e.g. If we have def WeightedDFA : Type := ..., then the function recognized by a wdfa : WeightedDFA will be implemented as transduceFrom wdfa in instance : Transducer WeightedDFA Symbol Weight where ....

In this sense, T and t : T are analogous to A and a : A in Acceptor.lean.

[ctchou]

Thanks for the explanation. Perhaps something like you wrote above should be part of the doc-string.

[ctchou]

Please give a name to this section.

[LiamSchilling]

Thanks for the feedback 👍 This is now named Monoid as the section that takes weights to be from a Monoid.

[ctchou]

Some general comments:

• Please run lake exe mk_all --module, so that imports for any files you add will also be added to Cslib.lean.
• I'm not sure weighted automata are a widely known subject. (I for one don't know anything about it.). So please provide some references, which you can add to the file references.bib in the root directory and refer to them in a comment here.

[LiamSchilling]

A good reference for weighed automata is Droste et al. 2009. As in the chapter Mohri 2009, weighted automata have shortest-distance interpretations when weights are from an idempotent semiring. In this commit, just a semigroup is sufficient for stating the definition.

[ctchou]

This file looks fine by itself. So I'm approving it. But I wonder if we should wait for more material about weighted automata to be PR-ed to see how everything fits together. I leave that decision to @fmontesi .

[ctchou]

Thanks for the explanation. Perhaps something like you wrote above should be part of the doc-string.

[LiamSchilling]

Thanks for all the feedback @ctchou. Here's a second iteration that works with an implementation of typical deterministic FSTs (DetTransducer) and bimachines (Bimachine) in a downstream branch. It's a lot of code altogether, so I'm thinking it's best to split into 3 PRs:

• this one, defining Transducer
• one defining DetTransducer with a Transducer implementation
• one defining Bimachine with a Transducer implementation