next up previous
Next: Arbitraryness Up: Approx Trs Menu Previous: Membership to CBN

Preservation of the set of normalizable terms

As shown in [5], the sets of terms of $ \mathcal{T}(\mathcal{F})$ that are normalizable may be augmented if the signature $ \mathcal{F}$ is extended with just one fresh constant symbol (for instance ). Using the command WN(S,G,F) = WN(S,F) one can check whether signature extension preserves the set of normalizable terms. If this is not the case, then a term witnessing that WN$ (\mathcal{R}_\alpha,\mathcal{G},\mathcal{F}) \not\subseteq$   WN$ (\mathcal{R}_\alpha,\mathcal{F})$ is shown.

The same can be done with $ \mathcal{R}\cup \{ \bullet \to \bullet \}$ as for the growing approximation we may have WN$ (\mathcal{R}_\alpha,\mathcal{G},\mathcal{F}) =$   WN$ (\mathcal{R}_\alpha,\mathcal{F})$ but    WN$ _\bullet(\mathcal{R}_\alpha,\mathcal{G},\mathcal{F}) \not\subseteq$   WN$ _\bullet(\mathcal{R}_\alpha,\mathcal{F})$.
Use the command WNo(S,G,F) = WNo(S,F) for that purpose.