A note on completeness of conditional
context-sensitive rewriting
Author
Salvador Lucas
Abstract
Restricting the ability of the rewrite relation to
perform reductions can lead to loose computational
power in rewriting-based programming languages and
systems. Despite this fact, advanced specification
and programming languages like CafeOBJ, Maude, and
OBJ permit the introduction of such computational
restrictions by means of programmable strategies
and suitable syntactic annotations. The main reason
is to achieve a better termination behavior.
Canonical context-sensitive rewriting has been
proposed as a suitable restriction of rewriting
which can improve the termination behavior of TRSs
whereas is still able to achieve useful (normalizing
and infinitary normalizing) computations. In this
paper we discuss a number of drawbacks arising when
using canonical context-sensitive rewriting with
Conditional Term Rewriting Systems (which provide
an abstract computational model for the aforementioned
languages) and propose some appropriate solutions.
Keywords
Programming languages, Conditional term rewriting.