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]

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 .

[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

[ctchou]

I would prefer that you do not introduce "unit" in FLTS/Basic.lean and DA/Basic.lean, for I'm not sure that's a universally recognized concept. Please define the "unit DA" at the place where it is needed (namely, in ToBimachine.lean).

[ctchou]

There should be a /-! ... -/ comment about what this file is for.

[ctchou]

If the purpose of this file is to prove additional results about semigroup that are not in mathlib, this file should be named Semigroup.lean.

[ctchou]

Sorry, I did not mean to approve. I was requesting changes in the last batch of comments.