[TYPES] Definable programs in type theories

Yong Luo Y.Luo at kent.ac.uk
Thu Mar 30 07:06:24 EST 2006

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

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.



More information about the Types-list mailing list