Yong Luo wrote:
Hi, Conor,
Since you use elimination rule on both arguments, I was expecting four cases
like Thorsten did in the previous email. If you can define the Ackermann
function, then you must be able to define the Majority function. Is there
anything more than the standard elimination? Can we define the Ackermann
function like the following form?
ack x y = Elim_Nat ......
Couldn't you do this yourselves after reading my previous email?
T.
For example, plus can be defined as:
plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
Regards,
Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent
----- Original Message -----
From: "Conor McBride" <[EMAIL PROTECTED]>
To: <epigram@durham.ac.uk>
Sent: Friday, November 18, 2005 4:36 PM
Subject: Re: [Epigram] epigram tells me fibs
Yong Luo wrote:
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.
Since you ask, see attached file.
Conor
----------------------------------------------------------------------------
----
--------------------------------------------------------------------------
----
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
--------------------------------------------------------------------------
----
( ( p : P m ! !
! n : Nat ; P : Nat -> * ; mz : P zero ; !------------------! !
! ! ms p : P (suc m) ) !
let !----------------------------------------------------------------!
! elim n P mz ms : P n )
elim n P mz ms <= rec n
{ elim n P mz ms <= case n
{ elim zero P mz ms => mz
elim (suc n) P mz ms => ms (elim n P mz ms)
}
}
--------------------------------------------------------------------------
----
( x, y : Nat !
let !---------------!
! ack x y : Nat )
ack x y <= elim x
{ ack zero y => suc y
ack (suc m) y <= elim y
{ ack (suc m) zero => ack m (suc zero)
ack (suc m) (suc m') => ack m (ack (suc m) m')
}
}
--------------------------------------------------------------------------
----
inspect lam n : Nat => ack zero n => (lam n => suc n) : all n : Nat => Nat
--------------------------------------------------------------------------
----
inspect lam m : Nat => ack (suc m) zero
=> (lam m => ack m (suc zero)) : all m : Nat => Nat
--------------------------------------------------------------------------
----
inspect lam m, n : Nat => ack (suc m) (suc n)
=>
(lam m ; n => ack m (ack (suc m) n))
: all m : Nat ; n : Nat => Nat
--------------------------------------------------------------------------
----
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.
