Overloading in the context of higher-order logic has been used for some time now. Isabelle is the only proof-assistant that actually implements overloading within the logic instead of merely instrumenting the pretty-printing machinery on top of the logic.
So far there existed no satisfying theory that could explain why it is safe to add a mechanism of certain kinds of possibly overloading constant definitions to ordinary higher-order logic. This is not only of theoretical interest but also of practical importance; until now it was easy to introduce inconsistencies in Isabelle by abusing overloaded definitions.
This paper addresses both the theoretical and the practical aspects of adding overloading to higher-order logic. We first define what we mean by Higher-Order Logic with Conservative Overloading (HOLCO). HOLCO captures how overloading is actually applied by the users of Isabelle; for example it allows to freely mix type definitions with overloaded constant definitions. We then show the consistency of HOLCO by reducing it to ordinary higher-order logic with only type definitions and no constant definitions.
Having so established our playground we show that this playground is too big for any proof-assistant implementing HOLCO; checking if definitions obey the rules of HOLCO is not even semi-decidable. We prove this by connecting this problem with the problem of deciding the termination of certain kinds of term rewriting systems (TRSs) which we call overloading TRSs and showing that Post's Correspondence Problem for Prefix Morphisms can be reduced to it.
The undecidability proof reveals strong ties between our problem and the dependency pair method by Arts and Giesl for proving termination of TRSs. The dependency graph of overloaded TRSs can be computed exactly (for general TRSs it is not computable and must be approximated). We exploit this by providing an algorithm that checks the conservativity of definitions based on the dependency pair method and a restricted 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. Of course the algorithm cannot successfully check all valid conservative definitions; but it is sufficiently powerful 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.
Full Text: Conservative Overloading in Higher-Order Logic [pdf]
Abridged & Revised Text: Checking Conservativity of Overloaded Definitions in Higher-Order Logic [pdf]
(accepted for RTA 2006)
Software
README: How to Check Overloaded Definitions in Isabelle [pdf]
Example Isabelle Theories
The theory files below are for Isabelle 2005. The latest versions of Isabelle (>= May 15th 2006) employ a simple substructural test (slightly easier to implement than our test, but likely to get in the way of the serious overloader) that accepts none of the examples below. To try out the examples with these versions of Isabelle, replace
defs(overloaded)with
defs (unchecked overloaded)
| 1) | inconsistent.thy: | a non-conservative theory which leads to inconsistencies in Isabelle |
| 2) | easy_succ.thy: | a conservative theory whose conservativity can be proven by Checkdefs |
| 3) | hard_succ.thy: | a conservative theory whose conservativity cannot be proven by Checkdefs despite its similarity with example 2); the conservativity can be shown by exporting the resulting overloading TRSs and checking them for example with the Tyrolean Termination Tool (you can give the ZIP file directly to TTT) |
Last update: Wednesday, March 28th, 2007, 4:00 AM.