[Agda] termination proofs

Jacques Carette carette at mcmaster.ca
Mon Sep 24 21:42:43 CEST 2012

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).


[1] http://en.wikipedia.org/wiki/Goodstein%27s_theorem
[2] http://en.wikipedia.org/wiki/Fast-growing_hierarchy

More information about the Agda mailing list