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 ......
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
> --------------------------------------------------------------------------
----
>
