Efficient Strong Sequentiality Using Replacement Restrictions

Author

Salvador Lucas

Abstract

Huet and Lévy defined the (orthogonal) strongly sequential term rewriting systems, for which index reduction, i.e., reduction of redexes placed at special positions called (strong) indices, is optimal and normalizing. Despite the fact that Huet and Lévy give a general 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 don 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 reduction strategy.

Keywords

functional programming, neededness, replacement restrictions, term rewriting.