functional programs, was: Re: [Termtools] Next competition

[Johannes Waldmann]

>    . I'd like to propose new categories for functional programs and
>      imperative programs. I have no proposal for a official input
>      syntax, but if you are interested plase tell me.

Obviously I am interested, since I do a lot of functional programming.
On the other hand I'm skeptical, see below.

Termination for Functional programming opens up quite some problems
(of which syntax should be the easiest one):
what is "termination"? what evaluation strategy?
Full termination or top termination (because of lazy eval.)?
Are the programs typed? If so, what type system?
(Does it have an influence on termination?)
Do we do higher-order rewriting?
(I certainly use lambdas in my Haskell programs.)

Anyway to avoid syntax discussions, can we try for a subset
of some existing functional programming language (e. g. ML or Haskell).


Now, why am I skeptical: I do a lot of Haskell programming
but I find that termination is seldom an issue: either my programs are
(1) "trivially" terminating because I use structural induction
(primitive recursion on algebraic data types)
or (2) I don't know about termination myself (because the program
does something that is inherently hard or even Turing complete).

Of course sometimes I cannot avoid (2) but most of the time,
I enforce (1) by using generic higher order functions (map/fold).
That's why I like to translate the classical "Goto considered harmful"
into "recursion considered harmful". Sure I need recursion to define
map and fold, but only in the same way that I need a "goto" to define a
loop (that is, if  the loop is "built in", I can avoid the "goto",
and the program looks much better).

So I have the feeling that proving termination for (functional) programs
automatically is like guessing a loop invariant: it's too late.
With proper design, the invariant (resp. termination proof)
would have been written by the programmer (and *before* programming).

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

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools