A Logic for Rewriting Strategies

AbstractRewriting strategies can become quite complex and are not easy to comprehend or reason about when they are expressed in operational terms. This paper develops a weakest precondition logic for reasoning about strategies programmed in the strategy language Stratego. This logic embeds the modal mu-calculus, allowing it to express properties of terms of arbitrary depth. Its use is illustrated by characterizing properties of several reduction strategies for the lambda calculus with explicit substitutions