[Agda] termination proofs

[Peter Hancock]

On 24/09/2012 19:01, Serge D. Mechveliani wrote:

> Does there exist an algorithmic map in  Nat -> Nat  for which there
> is not any Agda program with a termination proof accepted by Agda ?

I hope so.  For example, if you Godel-number everything, the function/map
that maps the Godel-number of a typed expression to that of its canonical
form is (unless I am being silly) such a function.

On countability grounds too, there are uncountably many functions in Nat -> Nat,
but since Agda is a formal system (isn't it?) there are only countably many
expressions in it of (formal) type Nat -> Nat. (They are not just countable
but even computably enumerable.)

There are also (I hope) well-orderings on Nat that are not provably so.
Using this, one can cook up some functions in Nat -> Nat that are
too fast-growing to be representable in Agda.

This all for "Godelian" reasons, and is just a fact of life.  The same
goes for any half-way sensible extension of Agda.

Regards,

Peter