next up previous
Next: Preservation of the set Up: Approx Trs Menu Previous: Changing the current approximation

Membership to CBN

One can check membership to CBN$ _\alpha$ for the current TRS $ \mathcal{R}$ and the current approximation $ \alpha$ by using the Call-by-need command.

The answer is either ``the TRS is in CBN$ _\alpha$ or ``the TRS is not in CBN$ _\alpha$; in the latter case an ``$ \alpha$-free-term'' i.e. a term with no $ \mathcal{R}_\alpha$-needed redex is shown.

The Call-by-need command checks membership to CBN$ _\alpha$ but with the signature extended with a fresh constant symbol . Indeed a TRS may be in CBN$ _\alpha$ with the signature consiting of all the symbols appearing in its rules but not in CBN$ _\alpha$ with the same signature extended by just one fresh symbol. The preservation of membership thru ``signature extension'' has been investigated in [5].

Note that the membership to CBN$ _\alpha$ problem having a double exponential time complexity, may run for a very long time for big TRS.
Use the Stop button to stop the computation.