[Fwd: how much detail in proofs (esp. RFC match bounds) - was: Re: [Termtools] Next competition]

[Johannes Waldmann]

Claude Marche wrote:

> of the given problem. In other words, although the problem "is P
> terminating ?" undecidable in general, the problem "is T a valid trace
> for the termination of P ?" should be decidable.

Let's add "efficiently" to "decidable", the strongest definition being
PTIME, and without absurd coefficients or degrees in the polynomials.
Then I think this would not allow to omit the automaton.
The trace automaton might have exponential size (the match bound
is in the exponent) but its verfication is polynomial (w.r.t. its size).

At the moment, the only way to check the claim that
"R  is match-bounded by  c  with some automaton of size  s"
is to (re-)construct the automaton, but that's not trivial.
The approximative construction (as in Torpa, Matchbox, Aprove)
might not terminate. An exact and efficient algorithm
has been found by Jörg (Jambox) but it's currently unpublished.

If you have enough space on the competition server,
then indeed I would suggest to fully output the automaton.
(That's what Torpa and Aprove already do, without asking :-)

Also, I think it is quite legitimate to *not* publish (for a while)
the method of proof construction as long as the proof can be verified
independently from its construction. - Of course in the long run,
you'd get more recognition for publications than for winning
competitions and not saying how :-) (and of course the Jambox
method will be published - we're actively working on that).
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------