Checking Conservativity of Overloaded Definitions in Higher-Order Logic

Steven Obua

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationTerm Rewriting and Applications
Subtitle of host publication17th International Conference, RTA 2006 Seattle, WA, USA, August 12-14, 2006 Proceedings
EditorsFrank Pfenning
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-540-36835-9
ISBN (Print)978-3-540-36834-2
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Checking Conservativity of Overloaded Definitions in Higher-Order Logic'. Together they form a unique fingerprint.

Cite this