Special Case of Second-Order Strictness Analysis

摘要

A function declaration is called strict in one of its formal parameters if, in all calls to the function, either the actual corresponding parameter is evaluated, or the call does not terminate. Approximating strictness analysis with abstract interpretation reduces to the evaluation of recursive monotone Boolean functions. This evaluation problem is complete in deterministic exponential time when the functions are declared with only base type formal parameters, and is deterministic super-exponential time hard when functions are formal parameters. However, by coarsening the strictness analysis approximation to be conjunctive, the first-order case can be completed in linear time. This paper will show that the second-order case is NP-hard. Keywords: Programming languages, Semantics. (kr)