Are needed redexes really needed?
Sergio Antoy, Andy Jost · 2013
We present an approach to rewriting in inductively sequential rewriting systems with a very distinctive feature. In the class of systems that we consider, any reducible term defines a needed step, a step that must be executed by any rewriting computation that produces the term's normal form. We show an implementation of rewriting computations that avoids executing some needed steps. We avoid executing these steps by defining functions that compute a reduct of a step without the explict construction or presence of the redex. Our approach improves the efficiency of many computations---in some cases by one or two orders of magnitude. Our work is motivated by and applicable to the implementation of functional logic programming languages.