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

• $\mathcal{L}=$   NF: command Automaton C NF ,
• $\mathcal{L}= L(\mathcal{A}_A)$: command Automaton C A ,
• $\mathcal{L}= L(\mathcal{A}_{S})$: command Automaton C S , $S$ being the instances of the current termset.

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 .