Hello Thorsten, I need to ponder your email a little bit longer, but here is my initial thoughts.
Let's start from basic concepts. When we write down an equation in programming languages, for example, f(x,0)=x, where x is a variable, we mean that f(x,0) can be reduced to x in one step and they are definitionally equal to each other. And hence, dependent types Vector(f(x,0)) and Vector(x) are the same. Now, let's compare your function with the standard Ackermann function. > > ack 0 0 = 0 ----- (S 0) > ack 0 (S n) = S(S (ack 0 n)) > ack (S m) 0 = 1 > ack (S m) (S n) = ack m (ack (S m) n) > ack 0 n = S n ack (S m) 0 = ack m (S 0) ack (S m) (S n) = ack m (ack (S m) n) In the standard one, (ack 0 n) is definitionally equal to (S n) where n is an arbitrary variable, but in yours, they are only extensionally equal to each other. And hence, dependent types Vector(ack 0 n)and Vector(S n) are not the same in your case. Another typical example is the Majority function. For the last equation, because it is a nested case, I doubt we can define "ack" by the eliminator of Nat, which satisfies that (ack (S m) (S n)) can be reduced to (ack m (ack (S m) n)) in "one" single step. I might be wrong and like to see how "ack" can be defined by the eliminator. As I mentioned before, one of the motivations to develop a type theory with partially defined functions and with pattern matching is that we may be able to define many functions exactly as they are, or as a mathematician intend to be. And we don't need to modify them in any way. In my implementation, the standard Ackermann function can be defined exactly as it is. Regards, Yong ============================== Dr. Yong Luo Computing Laboratory University of Kent ----- Original Message ----- From: "Thorsten Altenkirch" <[EMAIL PROTECTED]> To: <epigram@durham.ac.uk> Sent: Thursday, November 17, 2005 2:01 PM Subject: Re: [Epigram] epigram tells me fibs > Hi Yong, > > >>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. > > That's not correct, in the presence of function types it is completely > straightforward to define the Ackermann function using primitive > recursion. > > My slightly non-standard definition of ack goes as follows > > ack 0 0 = 0 > ack 0 (S n) = S(S (ack 0 n)) > ack (S m) 0 = 1 > ack (S m) (S n) = ack m (ack (S m) n) > > this is just primitive recursion with functions, that is I define > > ack 0 = dbl > > where > > dbl 0 = 0 > dbl (S n) = S( S (dbl n)) > > and > > ack (S m) = ack_f (ack m) > > with > > ack_f : (Nat -> Nat) -> Nat -> Nat > > ack_f ack_m 0 = 1 > ack_f ack_m (S n) = ack_m (ack_f n) > > Hence, I don't need to be clever. > > Btw, the only reason to diverge from the standard def is that I like > ack 0 = 2*n, ack 1 = 2^n and so on, not something slightly odd. > > Primitive recursion + function types give you all functions provable > total in Arithmetic, Goedel proved this (that's where System T comes > from). > > > 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) > > This program is structurally recursive (and so is fib), which can be > reduced to primitive recursion in a standard way, which has been > explored by a number of people, including Conor and Tarmo Uustalu. > Indeed the reduction is built into Epigram's elaboration (or should > be, actually for no good reason the final step of reducing > course-of-value recursion to the elimination constants is currently > left out). > > > 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. > > The examples above do not provide a convincing motivation for such a > development, since we can reduce them to standard elimnators using > well known techniques. > > Cheers, > Thorsten > > -- > Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516 > Lecturer http://www.cs.nott.ac.uk/~txa/ > School of Computer Science & IT University of Nottingham > > This message has been checked for viruses but the contents of an attachment > may still contain software viruses, which could damage your computer system: > you are advised to perform your own checks. Email communications with the > University of Nottingham may be monitored as permitted by UK legislation. > >
