* "Jonathan S. Shapiro" <[EMAIL PROTECTED]> [2005-01-31T14:40-0500]:
> On Mon, 2005-01-31 at 17:39 +0100, Dominique Quatravaux wrote:
> > # let rec l = (1::l);;
> 
> URK.
> 
> Well, the reason to avoid this sort of thing is that termination matters
> to some people...

It's possible to prove termination of functions dealing with
recursive data structures, see

J. Giesl and A. Middeldorp:
Transformation Techniques for Context-Sensitive Rewrite Systems
http://www-i2.informatik.rwth-aachen.de/giesl/papers/JFP-distribute.ps

The paper gives the example
                          zeros = 0 :: zeros
and definitions of head and tail.


Cheers,
Michael
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to