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.
