[Agda] termination proofs

[Martin Escardo]

On 24/09/12 20:30, Altenkirch Thorsten wrote:
> Let g : Nat -> Nat -> Nat be the function which to compute g m n
> interprets m as the binary encoding of an Agda program and which returns
> (f n)+1 if the program type checks and defines a function f : Nat -> Nat
> and 0 otherwiseŠ Then define the function f : Nat -> Nat with f x = g x xŠ
>
> Another question: Is there such a program which we can actually write down?

Well, of course: (0) A Martin-Lof type theory term normalizer, (1) An 
Agda type checker, (2) a Haskell interpreter, (3) a bar-recursor 
relizing the double-negation shift.

Martin