[clean-list] GRS vs LTRS

[Arjen]

The compiler probably already converts recursive lets/wheres to 
non-recursive lets/wheres internally if this is possible.

But I don't think that this will solve you problem. Recursive function 
definitions are just as powerful as recursive lets. Also, data 
structures and functions are interchangeable. Therefore, as long as you 
permit any kind of recursion, you will always have this issue.

Any Turing-complete (or equivalent to lambda calculus) language will 
have nontermination issues. If you do want guaranteed termination, you 
will have to use a less powerful (or strongly normalizing) system, which 
cannot express all computable functions. That is why recursion (and 
recursive lets or similar and semantically equivalent language 
constructs) are important.

I hope this gives you a general idea about why removing recursive 
lets/wheres won't be enough to prevent nontermination.

Can you explain more about the specific issue you are trying to resolve?

kind regards,
	Arjen

Vag wrote:
> Why CLEAN is "based" on GRS instead of LTRS? Recursive let seems to be
> not so useful, but cyclic links in data makes automatic reasoning very
> hard and gives another evil source of nontermination.
> 
> Maybe it is worth to add a compiler option to deny recursive lets (and
> wheres) per module and convert them internally to let-befores?
> _______________________________________________
> clean-list mailing list
> clean-list at science.ru.nl
> http://mailman.science.ru.nl/mailman/listinfo/clean-list