[Agda] Theoretical limits of termination checking (reference request)

[Thomas Jaeger]

On 07/29/2014 02:26 PM, Kirill Elagin wrote:
> Formally: is there a subset of programs, such that there is an algorithm
> correctly checking termination of programs from this subset _and_ for
> any program there is an equivalent in this subset (by “equivalent” I
> mean “extensionally equal”)?

I'm assuming you require that membership in this subset be decidable. In
that case, the answer is no, by diagonalization.  You can enumerate all
programs (in the subset) that terminate according to your termination
checker; let f_i be the function that the ith program in that list
computes.  Then there is a terminating program that computes the
function g(i) := f_i(i) + 1 that your termination checker won't catch.

Thomas