A Type System for Weighted Automata and Rational Expressions?

Abstract. We present a type system for automata and rational expres-sions, expressive enough to encompass weighted automata and transduc-ers in a single coherent formalism. The system allows to express useful properties about the applicability of operations including binary hetero-geneous functions over automata. We apply the type system to the design of the Vaucanson 2 platform, a library dedicated to the computation with finite weighted automata, in which genericity and high efficiency are obtained at the lowest level through the use of template metaprogramming, by letting the C++ tem-plate system play the role of a static type system for automata. Between such a low-level layer and the interactive high-level interface, the type system plays the crucial role of a mediator and allows for a cleanly-structured use of dynamic compilation.