Dear Stefan, thanks for your comment.
E.g. the Coq papers define its elimination constructs either as
a catamorphism, or as a combination of casefix, 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/ ---
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
