Consider a simple language:$$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ordered set of terms.These terms can be evaluated using a small step operational semantics:$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ plus ~ t_1 t_3 \rightarrow plus ~ t_2 ~  t_3}$$$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ plus ~ n ~ t_1 \rightarrow plus ~ n ~ t_2}$$$$\frac{}{G ~ \vdash ~ plus ~ n_1 ~ n_2 \rightarrow n_1 + n_2} \\ \text{using the addition on natural numbers}$$$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ gen ~ t_1 \rightarrow gen ~ t_2}$$$$\frac{}{\{t_n\} ~ \vdash ~ gen ~ n \rightarrow except ~ n ~ t_n}$$$$\frac{G \setminus \{t_n\} ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ except ~ n ~ t_1 \rightarrow except ~ n ~ t_2}$$$$\frac{}{G ~ \vdash ~ except ~ n ~ m \rightarrow m}$$The idea is that the stored terms in $G$ might be mutually recursive, but are not allowed to loop. Hence, everytime, one term is selected from $G$, it is wrapped in an $except$ term that prevents such a loop.It seems intuitive, that this system (i.e. a function that applies a rule as long as possible) always terminates. But is that so? How does one prove this? I tried to map the evaluation to a CPO, but failed so far. The problem is proving the supremum of a directed chain: The term might grow and shrink. It may only grow however, when an except node is introduced, which reduces the allowed set $G$. So expansion is clearly limited. Any reduction clearly shrinks the term which is also limited. So I'd need a CPO defined as the product of these two orders that is not defined as usual.Does anyone have an idea how to solve this?
Termination of deterministic term rewriting
recursion;term rewriting;operational semantics;termination