Iterative fixed point computation for type-based strictness analysis

Abstract

Amtoft has formulated an “on-line” constraint normalization method for solving a strictness inference problem inspired by Wright. From the syntactic form of the normalized constraints he establishes that every program expression has a unique, most precise (“minimal”) strictness judgement, given fixed values for the strictness annotation in negative position.

We show that his on-line normalization is not required for proving his main syntactic result. Instead of normalizing the constraints during a bottom-up pass through the program we simply collect them first and solve them by standard iterative fixed point methods in a second phase. The main result follows from the fact that observable negative strictness variables only occur on the right-hand sides of the constraints. Furthermore, a standard iterative fixed point algorithm solves the constraints in linear time in the number of strictness variables in the constraint system whereas Amtoft's method requires exponential time.

Our presentation is somewhat different than Amtoft's. We use a linear-logic inspired presentation of the programming language and the strictness inference system for it. This results in smaller constraint systems generated. A tight strictness inference normalization result shows that many inequational constraints can be replaced by equational ones. Thus the constraint system can be simplified and significantly reduced in size by efficient variable unification, which can be performed on-line during its construction. Finally, we give an asymptotic worst-case analysis of the size of constraint systems relative to a program with or without explicitly typed variable declarations.

The main contributions in this paper are our analysis and method for solving type-based program analyses efficiently, not the design of new type-based program analyses. Generally, our method provides insight into the strengths of noncompositional program analysis algorithms; i.e., algorithms where the solution for a program is not computed as a function of the corresponding solutions of its immediate components, such as in Algorithm W or in frontier-based abstract interpretation.¹ In particular, our method demonstrates the effective use of efficient iterative fixed point computation known from classical data flow analysis in type-based program analysis.

DIKU Semantics Report D-192