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

[Claude Marche]

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

    Johannes> Claude Marche wrote:
    >> Having a tool for automatically proving
    >> termination of non primitive-recursive definitions of functions would
    >> be, on the contrary, very handy.

    Johannes> Do you have examples for (non-PR) functions
    Johannes> that you want proved terminating?

You are making a confusion between "primitive recursive function" and
"primitive recursive scheme of a definition of a function". Jurgen
already answers that.

    Johannes> Let me repeat the suggestion to collect "real" FP termination problems,
    Johannes> so that we know better what we are talking about.
    Johannes> (I suggested the Haskell prelude, and there is one more example below.)

    Johannes> Also, do we want to continue this discussion on this list?
    Johannes> (The good thing about mailing lists is that they have an archive
    Johannes> so one can easily trace the history of discussions.)

Yes, as far as the question is whether we can add a FP category to the
competition.

    Johannes> But perhaps FP termination is not of general interest
    Johannes> (but even then, an archived discussion would be nice.)
    Johannes> I figure that at least Cime, TTT and Matchbox *are* functional programs
    Johannes> (while Aprove seems the only prover *for* functional programs?)

CiME is written on Caml, but uses mutable data structures. It is
definitely not a functional program.



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