[Termination tools] Re: termination competition: certification of proofs

[Frederic Blanqui]

On Mon, 9 May 2005, H. Zantema wrote:

thank you for your answer hans.

> Many generated proofs are based on the application of some set of basic
> theorems (related to recursive path order, polynomial interpretation,
> dependency pairs, approximations of the dependency graph, analysis of SCC's
> in this graph, argumetn filtering, semantic labelling, match bounds, ....)
> Essentially a generated proof is a sequence of applications of these basic
> theorems, such that finally termination can be concluded. One way to
> certify such a generated proof is:
> * Verify the proofs of the basic theorems, e.g. in the CoLoR project; this
>  should be done only once for every basic theorem.

the certification of termination proofs is clearly possible now. at the 
moment, polynomial interpretations and dependancy pairs have been formalized 
and proved in color. hence, any proof using polynomial interpretations on 
dependancy pairs can be formally checked in color. rpo (and perhaps horpo) 
will be soon added in color. in addition to proving other termination 
criteria, we need to develop more tactics to automate the verifications and 
some interfaces between termination tools and color, hence my request for 
defining an output format for formally expressing termination proofs.

to this end, we need to clearly identify the termination criteria used (this 
requires a precise and complete description), and give a precise and complete 
description of the witnesses/ingredients that are necessary for certification. 
for instance, in the simple case of a proof using polynomial interpretations 
only, we need to give the polynomial associated to each symbol. in case of 
rpo, we need to give the precedence on symbols. etc.

> One problem in this area is that the output format based on such a set of
> basic theorems is not stable at all, since the set of basic theorems is
> growing and growing. This in contrast with the input format which is very
> stable up to the introduction of new categories. Even if there is good
> progress in formal verification of the basic theorems it seems quite
> unavoidable that (new) basic theorems are used in generated proofs for
> which formal verification has not been done (yet). Since I want to
> stimulate development of new basic theorems, I think the current
> competition on (non-formally verified) termination proofs should be kept.

i agree with you. providing a formal witness should be optional. however, even 
though the set of theorems will be growing, it is not a big thing to update 
the output format to include it, even though no certification tool will be 
able to handle it for some time.

> But the development of a new category of formally verified termination
> proofs in the competition is very welcome. The first step in this direction
> should be a proposal for the output format, based on some (restricted?)
> set of basic theorems. I think this proposal should come from the CoLoR
> project. As soon as this set of basic theorems is sufficiently substantial
> this category will be viable.

i will be happy to propose a first version of such an output format to the 
termination competitors. i was not thinking in asking a new category, but why 
not? the main challenge for me is more about certifying as much as possible as 
termination proofs, and perhaps finding some bugs...