Head-Strictness is Not a Monotonic Abstract Property

Abstract

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 A(sub p) and A(sub non p), such that any value has property P if and only if abs maps it to an element of A(sub p). Head-strictness is a property of functions over lists which asserts, roughly speaking, that whenever the function looks at the tail of a list, it looks at the head of the tail. We prove that head-strictness is not definable by abstract interpretation. We then present a non-monotonic abstract interpretation for head-strictness and prove its safety.