A rewriting point of view on strategies

TL;DR

This paper reviews various formal definitions of strategies in rewriting systems, connecting concepts from rewriting logic, calculus, deduction, and game theory to provide a comprehensive understanding.

Contribution

It synthesizes different formalizations of strategies in rewriting, highlighting their higher-order, deductive, and sequential aspects in a unified framework.

Findings

Strategies can be formalized as proof terms in rewriting logic and calculus.

Strategies can be viewed as subsets of derivations for deduction and computation.

Strategies can be represented as partial functions in sequential path-building games.

Abstract

This paper is an expository contribution reporting on published work. It focusses on an approach followed in the rewriting community to formalize the concept of strategy. Based on rewriting concepts, several definitions of strategy are reviewed and connected: in order to catch the higher-order nature of strategies, a strategy is defined as a proof term expressed in the rewriting logic or in the rewriting calculus; to address in a coherent way deduction and computation, a strategy is seen as a subset of derivations; and to recover the definition of strategy in sequential path-building games or in functional programs, a strategy is considered as a partial function that associates to a reduction-in-progress, the possible next steps in the reduction sequence.