
Backwards Strictness Analysis:
Proved and Improved
Kei Davis
Philip Wadler
Dept. of Computing Science
University of Glasgow
Glasgow G12 8QQ
United Kingdom
Abstract
Given a syntax tree representing an expression, and some information regarding that
expression, a backwards analysis will involve propagating the information (with appropriate
transformation) towards the leaves of the tree, to yield information about the
subexpressions. Here, the information at the root will describe the required definedness
of the value of the expression, with the results of the analysis describing the definedness
of the values lower in the tree sufficient or necessary to meet the condition at the root.
In Projections for Strictness Analysis [1], such an analysis is described in which the
information at each node is encoded by a special kind of function called a projection,
with the results of the analysis revealing strictness information about the expression.
This paper describes a more general and powerful technique, and provides proofs that
both techniques meet a corresponding generalisation of the safety condition described
in [1].
1 Introduction
The theory developed in [1] is prerequisite to the development in this paper. To make our presentation reasonably selfcontained, this introduction includes a brief summary of much of the content of [1].
A projection is an idempotent function on domains that removes information from its
argument, but does not change its type. Formally, a projection is a continuous function
which for every u in its domain,
u v u
( u) = u
Projections form a complete lattice under the ordering v, with the identity function ID as the greatest element and BOT , defined by BOT u = ? for all u, as the least. (The greatest lower bound u of two projections and is defined to be the the greatest projection less than both and ; the greatest such function will not necessarily be a projection.) In this paper, and (sometimes subscripted) will always denote projections. Consider the following projections on pairs, defined for all values u and v.
F (u; v) = (u; ?)
S (u; v) = (?; v)
Then
(F t S) (u; v) = (u; v)
(F u S) (u; v) = (?; ?)