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 self-contained, 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) = (?; ?)