Head-Strictness is Not a Monotonic Property

A property P of a language is said to be definable by abstract interpretation if there is a monotonic map abs from the domain of standard semantics to an abstract domain A of finite height, and a partition of the abstract domain into two parts AP and Anon-P , such that any value has property P if and only if abs maps it to an element of AP . Head-strictness is a property of functions over lists which asserts, roughly speaking, that whenever the function looks at some prefix of a list, it looks every element in that prefix. We prove that head-strictness is not definable by abstract interpretation. Keywords: strictness analysis, abstract interpretation 1 INTRODUCTION 2 1 Introduction Given a programming language L with standard semantics [[\Delta]] D : L ! D, an abstract interpretation [2, 6] of L is a semantics [[\Delta]] A : L ! A, together with a function abs : D ! A. A represents some property of programs in L, [[\Delta]] A is the static computation of that property, and abs is ..