Partial evaluation and context-sensitive rewriting
URI permanente para esta colección:
Artículos en la categoría Partial evaluation and context-sensitive rewriting publicados en las Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017).
Notificar un error en esta colección
Examinar
Envíos recientes
Resumen Partial Evaluation of Order-sorted Equational Programs modulo AxiomsAlpuente, María; Cuenca-Ortega, Angel; Escobar, Santiago; Meseguer, José. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts and overloading; and equational rewriting modulo axioms such as commutativity, associativity–commutativity, and associativity–commutativity–identity. In this paper, we illustrate the key concepts by showing how they apply to partial evaluation of expressive rule-based programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on equational least general generalization for ensuring global termination. We demonstrate the use of the resulting partial evaluator for program optimization on several examples where it shows significant speed-ups.Resumen Some applications of context-sensitive rewritingLucas, Salvador. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.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.