Re:Weakening Cycles So That Turing Can Halt
by jondgoodwin on Friday May 15, 2020 @02:16AM
(#23189443)
Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.
[ Parent
| on HN ]
> Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.
How is it weak? Surely it's equivalent to any other approach: given a function and any form of termination guarantee for that function, you can encode that guarantee as a phantom type and then you have an expression of that function in a total functional language.
I mean, how long does it take to convince yourself a function will halt vs how long does it take to use implement it with well-founded recursion, with comparable readability? Not that it's not possible, it's just more of a pain.