The evaluation strategy for head normal form with and without on-demand flags

Abstract

We propose two conditions of the E-strategy with and without on-demand flags on which an evaluated term is always in head normal form. In rewriting with the E-strategy without (or with) on-demand flags, terms are evaluated according to a list of natural numbers (or integers) given to each function symbol. The first (or second) condition is that if there exists a rule such that a function symbol f occurs in its left-hand side and its i-th argument is not a variable, a list of f must contain i (or -i), and if f is also a defined one, a list of f must contain 0 at the end. While there is no restriction w.r.t. the first condition, the second one can only be applied to left-linear constructor TRSs. But, There are cases in which rewriting with the E-strategy with on-demand flags terminates properly while that with the E-strategy without on-demand flags does not. We also propose a method of obtaining normal forms if a way to get head normal forms is given.