[Termination tools] termination competition: certification of proofs

[H. Zantema]

On Tue, 3 May 2005, Frederic Blanqui wrote:

> hi! for the termination competition, you have defined an input format, but you 
> don't have an output format explaining the criteria used, hence no way to 
> certify those results. CoLoR, http://color.loria.fr/, is a project that aims 
> at certifying termination proofs. if the main participants of the termination 
> competition could agree on a comon output format for termination proofs, i 
> could try to use color to certify those proofs. so, as authors of the input 
> format, i come to you to know whether it would be possible to launch a 
> discussion on this subject, and try to design a first version of such an 
> output format.

This point has been discussed by several people. Often formal certification
of the generated proofs is seen as an ultimate goal, but is considered 
to be too ambitious for the moment.

For the first point (formal certification as an ultimate goal) I fully agree:
often the generated proofs are that complex that it is unfeasible to check
them by human. Moreover, it already turns out that some generated proofs
are wrong; this was observed for several tools. In most cases the code of
the tool has been repaired such that the same wrong proof is not generated
any more. But there is no evidence at all that all generated proofs are 
correct, and formal certification is the obvious way to proceed to increase
reliability of the tools. 

Whether formal certification is too ambitious for the moment or not strongly
depends on the state of the art in this area, in which most of the 
termination tool developers (including me) are no experts.

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.
* Verify formally that in the applications of the basic theorems in the 
  generated proofs all conditions of the basic theorems hold; this should
  be done for every generated proof separately.

I think it is important to distinguish these two points, in order to keep
connection between formally verified proofs and human readable proofs.

In the definition of the output format it is important to know which of the
basic theorems have been certified. I should like to know about the progress
in the area: what are the basic theorems that have been verified formally
already?

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.

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.



		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+