Efficient Strong Sequentially Using Replacement Restrictions

摘要

Huet and Levy defined the (orthogonal) strongly sequential term rewriting systems, for which index reduction, i.e., reduction of re-dexes placed at special positions called (strong) indices, is optimal and normalizing. Despite the fact that Huet and Levy give an algorithm to compute indices for the general case, there are many proposals to define subclasses of strongly sequential rewrite systems for which this can be done more efficiently. In this paper, we show that sometimes it is possible to enlarge such classes by only introducing fixed replacement restrictions, without forcing any sensible modification of the corresponding index re-duction strategy.