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@science.ru.nl
http://mailman.science.ru.nl/mailman/listinfo/clean-list
_______________________________________________
clean-list mailing list
clean-list@science.ru.nl
http://mailman.science.ru.nl/mailman/listinfo/clean-list
