refactoring, catamorphism, termination of programs
Dear all, 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. I figure it could be distilled from some existing refactoring suite, or be manufactured from existing building blocks. E.g. Language.Haskell.* from the ghc libs, and perhaps "Typing Haskell in Haskell"? http://citeseer.ist.psu.edu/424440.html Any hints appreciated. Of course, if you already have some termination prover for Haskell programs, using any method whatsoever, then you're invited to take part in the "FP" category of the upcoming Termination Competition, see http://www.lri.fr/~marche/termination-competition/2007/ (Also, I'd welcome your comments on the proposed form and semantics of the FP category.) For discussion, please do not use this list but http://groups.google.de/group/fp-termination Best regards, Johannes Waldmann.
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
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/ -------
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 Haskell Cafe exactly the place for that discussion? (As opposed to the Haskell mailing list.) Good luck with the discussion. Someone mentioned DrHylo; that's built on the work of Hu, Onoue and others from Tokyo on a system called Hylo: http://www.ipl.t.u-tokyo.ac.jp/~onoue/hylo/ See also Alberto Pardo's HFusion: http://www.fing.edu.uy/inco/proyectos/fusion/ Jeremy Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 283531 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html
Hi Maybe this link is of interest to you: http://wiki.di.uminho.pt/twiki/bin/view/Research/PURe/WebHome. A tool called DrHylo, developed in the context of this project is available, altough I don't know how suitable it could be for you: http://wiki.di.uminho.pt/twiki/bin/view/Personal/Alcino/DrHylo. Regards José Pedro On 5/1/07, Johannes Waldmann <waldmann@imn.htwk-leipzig.de> wrote:
Dear all,
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.
I figure it could be distilled from some existing refactoring suite, or be manufactured from existing building blocks.
E.g. Language.Haskell.* from the ghc libs, and perhaps "Typing Haskell in Haskell"? http://citeseer.ist.psu.edu/424440.html
Any hints appreciated.
Of course, if you already have some termination prover for Haskell programs, using any method whatsoever, then you're invited to take part in the "FP" category of the upcoming Termination Competition, see http://www.lri.fr/~marche/termination-competition/2007/
(Also, I'd welcome your comments on the proposed form and semantics of the FP category.) For discussion, please do not use this list but http://groups.google.de/group/fp-termination
Best regards, Johannes Waldmann.
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Hi Jahannes,
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.
I figure it could be distilled from some existing refactoring suite, or be manufactured from existing building blocks.
Well, HaRe -- the Haskell refactorer -- offers a full API for building transformations and refactorings for the full Haskell 98 standard. http://www.cs.kent.ac.uk/projects/refactor-fp/hare.html A new release will hopefully be released very soon (even in the next few days) which will be compatible with ghc-6.6.1. The releases on our refactoring page currently only work with GHC-6.4.*.
E.g. Language.Haskell.* from the ghc libs, and perhaps "Typing Haskell in Haskell"? http://citeseer.ist.psu.edu/424440.html
HaRe also uses the GHC API and type checker, with parts of the HaRe API extended to retrieve type information from GHC on abritrary expressions and functions. Kind regards, Chris.
participants (5)
-
C.M.Brown -
Jeremy Gibbons -
Johannes Waldmann -
José Pedro Correia -
Stefan Monnier