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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.