Elimination of Conditional Rules in Term Rewrite Systems
From FSL
(Redirected from Computationally Equivalent Elimination of Conditions)
This page covers several papers authored by FSL group members regarding elimination of conditional rules. We believe that any conditional term rewrite system (CTRS) intended for ground term reductions can be automatically rewritten to contain no conditional rules. The papers presented below give a history of our attempts in this direction, separated in conference papers and technical reports; the technical reports contain all the proofs that have been omitted from the conference papers.
Contents |
[edit] Conference Papers
[edit] RTA'06
- Computationally Equivalent Elimination of Conditions
- Traian Florin Serbanuta and Grigore Rosu
- RTA'06, LNCS 4098, pp 19-34. 2006
- Abstract. An automatic and easy to implement transformation of conditional term rewrite systems into computationally equivalent unconditional term rewrite systems is presented. No special support is needed from the underlying unconditional rewrite engine. Since unconditional rewriting is more amenable to parallelization, our transformation is expected to lead to efficient concurrent implementations of rewriting.
- PDF, Experiments, RTA'06 Slides, LNCS, RTA'06, DBLP, BIB
[edit] WADT'04
- From Conditional to Unconditional Rewriting
- Grigore Rosu
- WADT'04, LNCS 3423, pp 218-233. 2004
- Abstract. An automated technique to translate conditional rewrite rules into unconditional ones is presented, which is suitable to implement, or compile, conditional rewriting on top of much simpler and easier to optimize unconditional rewrite systems. An experiment performed on world's fastest conditional rewriting engines shows that speedups for conditional rewriting of an order of magnitude can already be obtained by applying the presented technique as a front-end transformation.
[edit] Technical Reports
- Computationally Equivalent Elimination of Conditions
- Traian Florin Serbanuta and Grigore Rosu
- Technical Report UIUCDCS-R-2006-2693, February 2006
- Abstract. An automatic and easy to implement transformation of conditional term rewrite systems into computationally equivalent unconditional term rewrite systems is presented. No special support is needed from the underlying unconditional rewrite engine. Since unconditional rewriting is more amenable to parallelization, our transformation is expected to lead to efficient concurrent implementations of rewriting.
- PDF, Experiments, TR@UIUC, BIB
- Towards Effectively Eliminating Conditional Rewrite Rules
- Traian Florin Serbanuta and Grigore Rosu
- Technical Report UIUCDCS-R-2004-2494, December 2004
- Abstract. Conditional rewrite rules are notorious for being difficult to implement in rewrite engines. This is because, like in the case of function calls in programming language implementations, rewrite engines need to "freeze" the current rewriting environment and to create a new one in which the condition is reduced. Stacking these rewriting environments efficiently can easily become a nontrivial task, which can have a direct impact on the efficiency of rewriting.
Continuation-passing-style (CPS) transformations are used as a front-end in many programming languages to transform the programs to compile into a convenient and highly optimizable form, in which functions never need to return their values: they just pass their computed values to the current data-context, which "knows" how to continue the computation. We argue that a similar transformation technique can be applied to conditional rewrite systems, to transform them into computationally equivalent unconditional rewrite systems.
In this paper we present the first steps towards such a transformation. No special support is needed from the underlying unconditional rewrite engine, so the presented technique can be used as a front-end to any of the current rewrite engines. Since unconditional rewriting is more amenable to parallelization, our transformation is expected to lead to efficient concurrent implementations of rewriting.
- Abstract. Conditional rewrite rules are notorious for being difficult to implement in rewrite engines. This is because, like in the case of function calls in programming language implementations, rewrite engines need to "freeze" the current rewriting environment and to create a new one in which the condition is reduced. Stacking these rewriting environments efficiently can easily become a nontrivial task, which can have a direct impact on the efficiency of rewriting.
- From Conditional to Unconditional Rewriting
- Grigore Rosu
- Technical Report UIUCDCS-R-2004-2471, August 2004
- Abstract. An automated technique to translate conditional rewrite rules into unconditional ones is presented, which is suitable to implement, or compile, conditional rewriting on top of much simpler and easier to optimize unconditional rewrite systems. An experiment performed on world's fastest conditional rewriting engines shows that speedups for conditional rewriting of an order of magnitude can already be obtained by applying the presented technique as a front-end transformation.


