HEAD-STRICTNESS IS NOT A MONOTONIC ABSTRACT 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 parts A(P) and A(non-P), such that any value has property P if and only if abs maps it to an element of A(P). 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 at every element in that prefix. We prove that head-strictness is not definable by abstract interpretation.