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

[Juergen Giesl]

Dear Johannes,


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

I think there is some misunderstanding here.
Obviously, almost all functions used in practice are
primitive recursive. But the natural formulation for
their algorithm is often not in primitive recursive form.

Therefore, I agree with Claude who wrote:

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

An example is the classical minus & div example from our dependency pair
papers. Obviously, division is a primitive recursive function, but the
formulation of the algorithm is not in primitive recursive form.

> As I said earlier, my style of programming is that normally,
> a function should be primitive (*) recursive

Do you really write almost all your algorithms
in primitive recursive form? For example, how would you
define division on a user-defined data type of natural numbers?

Best Regards
Juergen


_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools