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

[Johannes Waldmann]

Peter Schneider-Kamp wrote:

> A term t containing no abstract variables is "terminating"
> if and only if
> (a) its evaluation (according to Haskell strategy) is finite
> and
> (b) all (type-correct) applications of t to a "terminating"
>     term are "terminating"
> 
> An abstract term t is "terminating" if and only if
> all (type-correct) instantiations of t which instantiate
> all abstract variables with "terminating" terms
> are "terminating".

just to clarify: what does (a) mean?

Since Haskell is lazy,  I'd think it should be
evaluation to head normal form,
i. e., a constructor (with unevaluated arguments)
or a lambda expression (with unevaluated body).

But then "ones = 1 : ones" should be terminating,
while your example indicates otherwise.

Or do you plan to have a separate concept  for "laziness"
(top termination perhaps)?

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