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