Worst-Case Groundness Analysis Using Definite Boolean Functions

TL;DR

This paper explores the theoretical worst-case scenarios for groundness analysis using abstract interpretation over definite and positive Boolean functions, highlighting exponential complexity in certain cases.

Contribution

It provides specific examples demonstrating exponential worst-case behavior for Def and Pos Boolean function domains in groundness analysis.

Findings

Def-based analysis can have exponential chains in argument and clause count.

Pos-based analysis can have exponential chains in program size.

Open problem remains on whether Def's worst case matches Pos's in severity.

Abstract

This note illustrates theoretical worst-case scenarios for groundness analyses obtained through abstract interpretation over the abstract domains of definite (Def) and positive (Pos) Boolean functions. For Def, an example is given for which any Def-based abstract interpretation for groundness analysis follows a chain which is exponential in the number of argument positions as well as in the number of clauses but sub-exponential in the size of the program. For Pos, we strengthen a previous result by illustrating an example for which any Pos-based abstract interpretation for groundness analysis follows a chain which is exponential in the size of the program. It remains an open problem to determine if the worst case for Def is really as bad as that for Pos.