A Note on the Choice of Domains

for Projection-Based Program Analysis

Kei Davis

Department of Computing Science

University of Glasgow

Glasgow G12 8QQ, UK

email: [email protected]

Abstract

Various nonstandard interpretations of functional programs have been proposed in which the basic nonstandard values are projections. We show that every stable function is completely determined by an appropriate abstract value in the backward analysis, and that every continuous function is completely determined by an appropriate value in the forward analysis.

1 Introduction

Strictness analysis by abstract (or non-standard) interpretation is an important part of several compilers for lazy functional languages [1, 2], and a wide variety of strictness analysis techniques have been proposed. The term forward is used to describe abstract interpretations in which the goal is to discover information about an entire expression given information at its leaves, while backward describes interpretations in which information flows in the other direction: the goal is to determine information at the leaves of an expression, given information about the entire expression.

The development of backward strictness analysis was motivated in part by the need for a method that could detect certain forms of data structure strictness such as head strictness, since a forward technique was not forthcoming, and suspected to be impossible by any forward analysis BHA framework [3].

A projection may be used to specify upper and lower bounds of the definedness of values (a semantic interpretation), or upper and lower bounds on evaluation (an operational interpretation); see e.g. [4]. In particular, projections can usefully encode head strictness as well as ordinary strictness [5]. Program analysis techniques based on the use of projections include backward strictness analysis techniques [5, 6, 7, 8],, and a forward analysis technique for use in partial evaluation [9].

A domain projection is a continuous, idempotent function that approximates the identity. The set of projections on a given domain forms a complete lattice