Búsqueda avanzada

Some applications of context-sensitive rewriting (Tutorial)


The appropriate selection of the arguments of functions that can be evaluated in function calls improves the evaluation of such calls in a number of different ways: efficiency, speed, termination behavior, etc. This is essential in the conditional if-then-else operator. Other operators like sequencing (;) or choice (+) that are used in concurrent and/or imperative languages require a similar treatment. The (lazy) list constructor ‘cons’ of functional languages is another well-known example. At the syntactic level we can specify this by just associating a set mu(f) of indices of evaluable arguments to each function symbol ‘f’ by means of a mapping mu which we call a replacement map. For instance, we let mu(if-then-else)={1} to specify that only the boolean argument ‘b’ of a conditional expression (if b then e else e’) is necessarily evaluated. We can write mu(;)={1} to avoid computations on S2 in a sequence S1;S2, and mu(+)={} to say that processes should not be executed as part of a choice expression. In the realm of term rewriting, context-sensitive rewriting is the restriction of rewriting that arises when these syntactic replacement restrictions are taken into account. It has been used to improve the termination behavior of reduction-based computation systems and programs. It has been shown useful as an operational notion to model or simulate the executions of various formalisms and calculi. Some computational properties of context-sensitive rewriting (remarkably termination) have been used to characterize or verify computational properties of important rewriting strategies like innermost, outermost, demand-driven, and lazy rewriting. Context-sensitive rewriting has also been shown useful to develop verification techniques and tools for variants of rewriting like order-sorted or conditional rewriting. Consequently, it is also useful for analyzing computational properties of programs written in sophisticated rewriting-based programming languages such as OBJ*, CafeOBJ, Maude, Elan, etc., where related language constructions are used. This paper provides an overview of the theory of context-sensitive rewriting and some of its applications.

Palabras Clave:

context-sensitive rewriting - infinitary normalization - normalization - replacement restrictions - rewriting semantics - termination





Este artículo tiene una licencia de uso CreativeCommons Reconocimiento (by)

Descarga el artículo haciendo click aquí.