A minimalistic look at widening operators

TL;DR

This paper redefines the concept of widening in abstract interpretation using a minimalistic approach, representing it as a lazily constructed well-founded tree to improve understanding and correctness proofs.

Contribution

It introduces a new characterization of widening as a lazily constructed well-founded tree, simplifying the formalization in higher-order logic.

Findings

Widening sequences can be characterized as well-founded trees.

Many traditional axioms of widening are unnecessary for correctness.

The approach supports dependent type systems for correct termination.

Abstract

We consider the problem of formalizing the familiar notion of widening in abstract interpretation in higher-order logic. It turns out that many axioms of widening (e.g. widening sequences are ascending) are not useful for proving correctness. After keeping only useful axioms, we give an equivalent characterization of widening as a lazily constructed well-founded tree. In type systems supporting dependent products and sums, this tree can be made to reflect the condition of correct termination of the widening sequence.