[Agda] termination proofs
Martin Escardo
m.escardo at cs.bham.ac.uk
Mon Sep 24 22:43:00 CEST 2012
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
More information about the Agda
mailing list