Thanks for the link (looking at it now), and for the terminology (sound, complete). The trivial algorithm to determine termination is to just run the code. Thi

Thanks for the link (looking at it now), and for the terminology (sound, complete). The trivial algorithm to determine termination is to just run the code. This algorithm is sound but not complete, and is not interesting from the point of view of a termination competition. Very curious about complete but unsound approaches. First instinct is to just determine some rules that allow you to prune paths in the control flow of a program (e.g. prune away bounded loops). This doesn't help with recursion, though. If we were dealing with recursive functions with constrained argument types, I can see rules like "for two calls, integer argument is moving closer to base case" being effective. Generalizing this still feels like it would be magical to me (which means I don't understand it at all).