[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).
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
More information about the Agda
mailing list