Simplification and termination of strategies in rule-based languages

Authors:
Open Access
Publisher website
Google Scholar
Abstract
In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient criterion for ELAN-like strategies to terminate, only lying on rewrite rules involved in the strategy. We then give a simplification process of strategies, itself described by rewriting, to empower the previous criterion. This simplification can also make proofs of other program properties easier.