Iterative Fixed Point Computation for Type-Based Strictness Analysis

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 ex...

• Type: Conference
• Year: 1994
• Where: SAS
• Authors: Fritz Henglein
• Keywords: Constraint Normalization Method, Formal Methods, Iterative Fixed Point, SAS 1994, Strictness Inference