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

[Claude Marche]

>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:

    Johannes> 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 ! 

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

    Johannes> I see two options:

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

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

The main goal of the termination competition is to motivate future
research. Handling higher-order, and case expressions, are an
interesting challenges. In many cases, I noticed that termination of
higher-order programs can be made by simply abstracting the
higher-order arguments, and using first-order techniques (for example map on
lists), this should be investigated more.


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

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

I think you are wrong here.  In Coq, you can easily define functions,
terminating by construction, by primitive recursion. But if you want
to use a more general recursion scheme, you have to built a
termination proof by hand. Having a tool for automatically proving
termination of non primitive-recursive definitions of functions would
be, on the contrary, very handy.

See the work of Frederic Blanqui (Definitions by rewriting in the
Calculus of Constructions), for example. And the CoLoR project.

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

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

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

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools