|  | |||||||||
Analysing Functions by Projection-Based Backward Abstraction
Kei Davis
Department of Computing Science, University of Glasgow
Glasgow G12 8QQ, UK
Abstract
Various techniques for strictness analysis by non-standard interpretation have been proposed in which the basic non-standard values are projections. We show that continuous functions can be completely characterised by appropriate forward and backward abstractions.
1 Introduction
Strictness analysis by non-standard (or abstract) interpretation allows significant optimisation
by compilers for lazy functional languages ([1], [2], [3]). Research continues in both the development
of strictness analysis techniques and their practical exploitation. In projection-based
backward analysis, abstract values in the form of projections are propogated from the leaves of
an expression to the root, and such analyses are able to determine not just ordinary strictness
but more elusive properties such as head strictness, even when working in finite domains of
abstract values ([4]). We are concerned with the theoretical power of such analyses, without
much consideration of such practical considerations restriction to finite abstract domains; in
particular we show that continuous functions can be completely determined by both forward
and backward abstract values from appropriate domains.
This works brings together and expands on ideas from several sources, most notably [4], [5],
and [6].
2 Projections
A projection is a continuous idempotent function that approximates the identity. The set of all projections on a given domain, ordered by the usual function ordering, forms an !-algebraic complete lattice, with the identity ID as the greatest element, and the constant bottom function BOT as the least. Since the glb of a set of projections in the domain of continuous functions is not necessarily a projection, the glb in the lattice of projections is defined to be the greatest projection approximating every element of the set. This projection necessarily approximates the glb in the continuous function space. A projection is finitary if its image is a domain. The set of finitary projections on any domain U also forms an !-algebraic complete lattice, and will be denoted by j U j. All projections herein are finitary, though no essential use is made of this fact. The symbols , , , and ffi will always denote projections.
3 Projections and Strictness
Projections may be used to specify upper and lower bounds on the definedness of values|a semantic interpretation, and upper and lower bounds on the degree of evaluation of expressions| an operational interpretation. Though it is possible to formalise the operational interpretation [3], here it is used only as an informal source of intuition. We give three examples. Let f denote f 2 U ! V such that f = f ffi BOT . This equation makes clear that f requires no information