functional programs, was: Re: [Termtools] Next competition

[Johannes Waldmann]

Claude Marche wrote:

>>From your answers, may I assume that at least two tools could
> participate to a Haskell programs category ? That would be great ! 

Well well well - we now seem to have agreed on syntax
but I still remain quite unconvinced about the FP category as a whole,
so I'm not sure how much time I will put into it.

I see two options:

(a) only handle those FPs that are in fact first-order TRSs
(b) handle "real" FPs (higher order, case expressions in RHSs)

So (a) is in fact only a programming exercise (independent
of the underlying termination prover), while (b) would require
significant research (and both are time-consuming).

The proper way to prove properties of programs (what a lot of "pro"s)
is of course to design the correctness/termination argument first, and
derive the implementation from that (see bottom of page 2 (= "1305-1")
in  http://www.cs.utexas.edu/users/EWD/ewd13xx/EWD1305.PDF )

And we already have fine  tools for that!
(e. g. as emphasized by the title of the Coq book:
http://www.labri.fr/perso/casteran/CoqArt/index.html)

So what I'm saying is that an FP category probably would not buy us much
(outside our own community). Of course it's a nice intellectual
challenge (... but so is solving Sudoku puzzles :-).

All this general discussion aside, the success of the FP category
(as well as all the others) would depend on the problems that are in it.
I must admit I don't have any, at the moment.
Of course we could somehow translate TRSs into form (a) (see above)
but that seems silly. Moving to (b), should we just include
each and every function from the official Haskell98 Prelude?
http://www.haskell.org/onlinereport/standard-prelude.html
To what extent does this seem realistic or desirable?
At least this would set a clear, external goal.

best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------