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

[Stefan Monnier]

> 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 think of quickly putting together a prototype
> that proves the concept.

Have you considered another approach?

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.

See for example Eduardo Gimenez's "Codifying guarded definition with
recursive schemes".  This paper also shows how to turn such a case&fix into
a call to a catamorphism.


        Stefan