- 1
- The latter will be used for generating identity translations.
- 2
- In the end, we should replace the lists by maps or something similar, for efficiency.
- 3
- Admittedly, the transducer examples so far has not been large enough to make any difference felt …
- 4
- 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
^{∗}. - 5
- One could choose that right-hand sides are from T
_{Σ}(Q(X) ∪ X), but in this way we assure that states never just vanish. - 6
- The functions tend to work best, if the shorter rules come first.
- 7
- When writing T
_{Σ}(Q^{∗}(X)), we for the time being mean more precisely T_{Σ}(Q(X)) ∪ T_{Σ}(Q(Q((X))))…. - 8
- The identity of the variables in t∈ T
_{Σ}(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. - 9
- At the current stage —unlike to some previous revisions— the step does not touch the the rewrite rules. Needs to be done.
- 10
- This avoids also, that straightforwardly reversing the reduction relation leads to non-termination behavior, especially in the function pre_on_rhs.
- 11
- Later, the two relations will be the past and future bisimulations ∼
_{p}and ∼_{f}on an approximation of the star transducer. - 12
- No attempt to minimize the rewrite system is done at this stage.
- 13
- 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.
- 14
- 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(?).