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

[Johannes Waldmann]

Claude Marche wrote:

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

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

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

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

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

=========================================================================

So here are some more remarks on FP termination:

As I said earlier, my style of programming is that normally,
a function should be primitive (*) recursive
and everything above that should be reserved
for very special cases, and I expect them to be very complicated.
That's why, from an "engineering" standpoint,
I would not want to hide this by an automatic proof,
rather I want a "handwritten" proof that also explains
where the complexity comes from and why it cannot be avoided.
(Sure "trivial" parts of this proof might be automated.)


(*) of course we have primitive recursion
for higher order functions as well, so we easily get

data Natural = Zero | Successor Natural

primrec :: a -> ( Natural -> a -> a ) -> ( Natural -> a )
primrec base step Zero = base
primrec base step ( Successor x ) = step x ( primrec base step x )

ackermann :: Natural -> Natural -> Natural
ackermann =
    primrec ( Successor )
            ( \ x p -> primrec ( p ( Successor Zero )) ( \ y -> p ) )

{-# TERMINATES: forall x :: Natural, y :: Natural . ackermann x y #-}

So I suggest this as a problem in the FP termination category
where the ideal termination proof is trivial:
check that "primrec" is indeed the correct "fold" for the type Natural,
and then check that outside of the definition of "primrec",
there is no recursive binding (in particular, the actual definition
of "ackermann" does not matter at all - as long as it does not mention
its own name). and of course check that everything is well-typed
because otherwise we could construct a fixpoint combinator
to sidestep the "no recursion" restriction.


Then the next step could be that a termination prover
tries to transform a given FP into such PR form. Such a transformer
would constitute a nice refactoring tool in its own right,
and there is work into that direction, see e. g.
http://www.cs.kent.ac.uk/projects/refactor-fp/
but that's a bit orthogonal to our discussion.

Although I can assure you that reasoning about time and space behaviour
of lazy functional programs is one big unsolved issue (it is a nightmare
to specify, predict or analyze resource consumption of a Haskell
program. In fact, three nightmares.) Termination doesn't give you much
because you rather want e. g. linear time and constant space etc.
IMHO this calls for a sharper type system
where types include resource consumption guarantees.
But again this is outside the scope of the termination competition.

Although tight bounds for derivation lengths *are* interesting
also for standard rewriting. E. g. for SRS/z086, we can prove
an exponential bound but we think the complexity is really polynomial.


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