next up previous
Next: Automata Up: Using Autowrite Previous: Needed reduction

TRS Automata

The TRS Automata menu, gathers commands to compute automata related to the left-handsides of the current TRS or to its approximation. The Redex automaton , Reducible automaton , Nf automaton compute the automata recognizing the sets of redexes, reducible terms, normal forms.

We have the possibilities of computing Toyama's or Jacquemard's $ \mathcal{C}_{{\mathcal{R}_\alpha},\mathcal{L}}$ automaton recognizing $ (\to_{\mathcal{R}_\alpha}^*)[\mathcal{L}]$ with either

We can also compute the automaton $ \mathcal{D}({\mathcal{R}_\alpha},\mathcal{F})$ which recognizes the set of reducible terms without $ {\mathcal{R}_\alpha}$-needed redex: command Automaton D .