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
On 2 May 2007, at 12:18, Johannes Waldmann wrote:
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.)
Isn't
I'm looking for a tool that implements the source code transformation
replace recursion by catamorphism (fold etc.).
My application is that if the transformation succeeds,
it implies that the program terminates. (roughly)
I don't want to make a big research project out of this,
rather I
