[Club2] Mi. 11.01.06: 15.00 Uhr

[Norbert Schirmer]

Diese Woche:

Mi. 11.01.06: 15.00 Uhr,  in Alan Turing (00.09.055).
Steven Obua:

Conservative Overloading in Higher-Order Logic ---
Theory and practice of checking overloaded definitions in Isabelle

Abstract:

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 overloaded 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.


    Norbert