On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
Per the wiki on termination analysis some languages with dependent types (Agda, Coq) have built-in termination checkers. I assume that DMD employs something short of such a checker, some combination of cycle detection backed up by resource bounds?
"Decidable" is a term that means that there are some cases which cannot be decided even if you had near infinite computational resources at your disposal. So it is a very theoretical term, and not very practical. I don't know what kind of solvers those languages use, so I am not exactly sure what they mean by "termination checker". In general, it is hard to tell if a computation is long-running or unsolvable.
