Checking Conservativity of Overloaded Definitions in Higher-Order Logic

Overloading in the context of higher-order logic has been used for some time now. We define what we mean by Higher-Order Logic with Conservative Overloading (HOLCO). HOLCO captures how overloading is actually applied by the users of Isabelle.

We show that checking whether definitions obey the rules of HOLCO is not even semi-decidable.

The undecidability proof reveals strong ties between our problem and the dependency pair method by Arts and Giesl for proving termination of TRSs via the notion overloading TRS. The dependency graph of overloading TRSs can be computed exactly. We exploit this by providing an algorithm that checks the conservativity of definitions based on the dependency pair method and a simple form of linear polynomial interpretation; the algorithm also uses the strategy of Hirokawa and Middeldorp of recursively calculating the strongly connected components of the dependency graph. The algorithm is powerful enough to deal with all overloaded definitions that the author has encountered so far in practice.

An implementation of this algorithm is available as part of a package that adds conservative overloading to Isabelle. This package also allows to delegate the conservativity check to external tools like the Tyrolean Termination Tool or the Automated Program Verification Environment.