Computational properties of term rewriting with
strategy annotations
Author
Salvador Lucas
Abstract
Strategy annotations have been
used in several programming languages to improve termination and efficiency of
computations. Eager (rewriting-based) languages (e.g., Lisp, OBJ*, CafeOBJ,
or Maude) interpret them
as replacement restrictions in order to become `more lazy',
thus (hopefully) avoiding nontermination.
In this paper, we investigate some computational properties (termination
and completeness) of
programs whose execution is controlled by strategy annotations.
Keywords
Declarative programming, replacement
restrictions, term rewriting, termination.