Navegación

Búsqueda

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.

Productivity of rewrite systems without transformations

Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data structures are often delivered as the outcome of computations. For instance, the list of all prime numbers can be returned as a neverending stream of numerical expressions or data structures. If such streams are allowed, requiring termination is hopeless. In this setting, the notion of productivity can be used to provide an account of computations with infinite data structures, as it “captures the idea of computability, of progress of infinite-list programs” (B.A. Sijtsma, On the Productivity of Recursive List Definitions, ACM Transactions on Programming Languages and Systems 11(4):633- 649, 1989). However, in the realm of Term Rewriting Systems, which can be seen as (first-order, untyped, unconditional) functional programs, termination of Context-Sensitive Rewriting (CSR) has been showed equivalent to productivity of rewrite systems through appropriate transformations. In this way, tools for proving termination of CSR can be used to prove productivity. In term rewriting, CSR is the restriction of rewriting that arises when reductions are allowed on selected arguments of function symbols only. In this paper we show that well-known results about the computational power or CSR are useful to better understand the existing connections between productivity of rewrite systems and termination of CSR, and also to obtain more powerful techniques to prove productivity of rewrite systems.