Lambda-choice: a calculus for consistent alternatives Seminars/Workshops

Abstract

When making program transformations, an optimizing compiler must frequently choose between different alternatives without yet having sufficient knowledge of their ultimate effects on its optimization objectives. Thus, all these compilers employ ad-hoc techniques for estimating these effects. I propose a calculus that can express pending choices between semantically equivalent alternatives directly. Thus, an optimizer that uses this calculus as its intermediate language can track the effects of several alternatives simultaneously. I investigate the impact of adding "choice between consistent alternatives" on the formal properties of the calculus itself and propose some ways of circumventing the problems that arise.