A Logic for Rewriting Strategies

Richard B. Kieburtz
Beaverton, Oregon, USA

Abstract

Rewriting 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 {\em weakest precondition} logic for
reasoning about strategies programmed in the strategy language {\sl
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.