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

[Juergen Giesl]

Dear Johannes,


>>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.

We use evaluation to normal form, not to (weak) head normal
form (i.e., we use "hyperstrict evaluation"). Of course, the
evaluation follows the usual Haskell strategy. The same notion
was also used in earlier work on automatic termination analysis
of Haskell.

The motivation is that this is also what (could)
happen in interpreters like hugs. If the user enters a term t
here, then this results in evaluation of the term "show t".
If for the type of t, "show" is defined in a way such that
all arguments of all constructors are inspected, then this
corresponds exactly to hyperstrict evaluation.

So "ones" is not terminating, but "take 5 ones" is terminating.

Best Regards
Juergen



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