[Agda] termination proofs

[Jacques Carette]

On 12-09-24 03:30 PM, Altenkirch Thorsten wrote:
> Re: Does there exist an algorithmic map in  Nat -> Nat  for which there
> is not any Agda program with a termination proof accepted by Agda ?
> [...]
> Another question: Is there such a program which we can actually write down?
>

Wouldn't a program based on Goodstein sequences [1] be quite easy to 
write, but with quite a difficult termination proof, at least as far as 
Agda is concerned?

If that's not fast enough, then one can go up the hierarchy [2] (without 
the need to go all Goedelian) of fast growing functions to Friedman's 
TREE function [3] for something quite frightening (although still 
'predicative' in a certain sense).

Jacques

[1] http://en.wikipedia.org/wiki/Goodstein%27s_theorem
[2] http://en.wikipedia.org/wiki/Fast-growing_hierarchy
[3] 
http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem#Friedman.27s_finite_form