Faithful (meta-)encodings of programmable strategies into term rewriting systems

Rewriting is a formalism widely used in computer science and mathematicallogic. When using rewriting as a programming or modeling paradigm, the rewriterules describe the transformations one wants to operate and rewritingstrategies are used to con- trol their application. The operational semanticsof these strategies are generally accepted and approaches for analyzing thetermination of specific strategies have been studied. We propose in this papera generic encoding of classic control and traversal strategies used in rewritebased languages such as Maude, Stratego and Tom into a plain term rewritingsystem. The encoding is proven sound and complete and, as a direct consequence,estab- lished termination methods used for term rewriting systems can beapplied to analyze the termination of strategy controlled term rewritingsystems. We show that the encoding of strategies into term rewriting systemscan be easily adapted to handle many-sorted signa- tures and we use ameta-level representation of terms to reduce the size of the encodings. Thecorresponding implementation in Tom generates term rewriting systems compatiblewith the syntax of termination tools such as AProVE and TTT2, tools whichturned out to be very effective in (dis)proving the termination of thegenerated term rewriting systems. The approach can also be seen as a genericstrategy compiler which can be integrated into languages providing patternmatching primitives; experiments in Tom show that applying our encoding leadsto performances comparable to the native Tom strategies