[Haskell] Re: refactoring, catamorphism, termination of programs

[Johannes Waldmann]

Dear Stefan, thanks for your comment.

> E.g. the Coq papers define its elimination constructs either as
> a catamorphism, or as a combination of case&fix, where the recursive calls
> are appropriately restricted to pass subterms as arguments.

if we replace the "subterm" ordering by some other well-founded
ordering on terms, and let a tool look for this ordering, then we get
the "classical" approach (that is used for term rewriting systems).

my point is that most (Haskell) programs don't require this
because they are (or should be) just primitive recursive functions
(catamorphisms) over data structures, and in fact they should be
presented as such (explicit recursion should be replaced
by the catamorphism), and I want a tool to do that replacement.

Sure, this will not solve all Haskell termination problems.
I just want to see how many are left
(e.g. from the functions in the Prelude, or in my programs).

If you want to contribute further to the discussion,
then please do so via http://groups.google.com/group/fp-termination
(I don't want to clutter the haskell  mailing  list,
but I want to have the discussion in some public place.)

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