[TYPES] Definable programs in type theories

[Yong Luo]

Dear all,

Last time I asked a question about the fib function, "can we define the fib
function in a normal type system (eg. Martin-Lof's type theory, Luo's UTT),
and such that fib (n+2) and fib n + fib (n+1) are computationally (or
definitionally) equal to each other?"

I have got some responses and the answer seems to be "No", although it
cannot be proved. I am wondering whether anyone has any idea about the
proof.

When we talk about definability of functions (or programs), we must be clear
what we mean by two functions (or two programs) are the same. For example,
one may ask "can you define the QuickSort in the system?". We cannot simply
answer "Yes" based on the fact that we can define another sorting program.

Regards,

Yong