> Is there documentation on exactly what the elimination constants are? > Epigram was happy with an Ackermann function, which surprised me > slightly. >
It is also surprising to me. Ackermann function is a nested function and is not a primitive recursion. The eliminators in conventional type theories are not powerful enough to define such functions directly. We must be clever enough to find other functions which are primitive and are "extensionally" equal to Ackermann function. Of course, other function may not have the beauty of the original, and most of programmers would feel very uncomfortable. I don't like the "Ackermann" function defined in Coq. I don't even like the way we define Fibs in Coq because the programmers are forced to find another equivalent function. Another similar example is the following. f(0)=0 f(1)=1 f(n+2)=2*f(n+1)-f(n)+1 There are many ways to define this function, but we cannot define it as it is. (The cleverest programmers can define f as: f(n)=n*(n+1)/2) I have developed and implemented a type theory which does not care whether a function is totally defined. In other words, partially defined functions are acceptable. In my implementation, the Ackermann function and the above function can be defined just as they are. Yong ============================== Dr. Yong Luo Computing Laboratory University of Kent
