Extensional and Intensional Strategies

TL;DR

This paper explores the theoretical foundations of strategies by defining extensional and intensional strategies, characterizing their relationship, and discussing potential logical characterizations and future directions.

Contribution

It introduces a general framework for extensional and intensional strategies, characterizes their relationship, and suggests avenues for logical characterization.

Findings

Characterization of extensional strategies definable intensively

Framework connecting abstract and operational strategies

Discussion of logical perspectives on intensional strategies

Abstract

This paper is a contribution to the theoretical foundations of strategies. We first present a general definition of abstract strategies which is extensional in the sense that a strategy is defined explicitly as a set of derivations of an abstract reduction system. We then move to a more intensional definition supporting the abstract view but more operational in the sense that it describes a means for determining such a set. We characterize the class of extensional strategies that can be defined intensionally. We also give some hints towards a logical characterization of intensional strategies and propose a few challenging perspectives.