The latter will be used for generating identity translations.
In the end, we should replace the lists by maps or something similar, for efficiency.
Admittedly, the transducer examples so far has not been large enough to make any difference felt …
Note that the module Mtt contains a few more printing-functions, which refer to the specific representations that will be defined only there to deal with T.
One could choose that right-hand sides are from TΣ(Q(X) ∪ X), but in this way we assure that states never just vanish.
The functions tend to work best, if the shorter rules come first.
When writing TΣ(Q(X)), we for the time being mean more precisely TΣ(Q(X)) ∪ TΣ(Q(Q((X))))….
The identity of the variables in tTΣ(Q(X)) doesn’t play a role. It is (implicitely) assumed, that they are all different. As the function will be used on the right-hand sides of the rules of linear transducers, the assumption is justified.
At the current stage —unlike to some previous revisions— the step does not touch the the rewrite rules. Needs to be done.
This avoids also, that straightforwardly reversing the reduction relation leads to non-termination behavior, especially in the function pre_on_rhs.
Later, the two relations will be the past and future bisimulations ∼p and ∼f on an approximation of the star transducer.
No attempt to minimize the rewrite system is done at this stage.
In [DLS02], we have a more straightforward exit condition: the loop stops, if the transducer indeed calculate a fixpoint, but this would be much less efficient. We need to think about the soundness of this exit condition here, though.
It will be use to speed-up the bisimulation calculation (avoiding recomputation). The invariant will be that the tuple constitutes a partition of the visited states(?).