Hi folks
Half asleep; pressed send instead of attach
Conor
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.
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( x, y : Nat !
let !-----------------!
! plus0 x y : Nat )
plus0 x y <= rec x
{ plus0 x y <= case x
{ plus0 zero y => y
plus0 (suc x) y => suc (plus0 x y)
}
}
------------------------------------------------------------------------------
( n : Nat !
! !
! P : Nat -> * ; mz : P zero ; ms : all k => P k -> P (suc k) !
let !---------------------------------------------------------------!
! elimNat n P mz ms : P n )
elimNat n P mz ms <= rec n
{ elimNat n P mz ms <= case n
{ elimNat zero P mz ms => mz
elimNat (suc n) P mz ms => ms n (elimNat n P mz ms)
}
}
------------------------------------------------------------------------------
inspect lam n : Nat => case n
=>
(lam n => case n) :
all n : Nat ; P : all n' : Nat => * ; m'zero : P zero
m'suc : all n' : Nat => P (suc n')
=> P n
------------------------------------------------------------------------------
( x, y : Nat !
let !-----------------!
! plus1 x y : Nat )
plus1 x y <= elimNat x
{ plus1 zero y => y
plus1 (suc k) y => suc (plus1 k y)
}
------------------------------------------------------------------------------
inspect (plus1 (suc (suc zero)) (suc (suc zero)))
=> suc (suc (suc (suc zero))) : Nat
------------------------------------------------------------------------------
( x, y : Nat !
let !-----------------!
! plus2 x y : Nat )
plus2 x y
=>
elimNat x (lam n => Nat -> Nat) (lam y => y)
% (lam x ; xp ; y => suc (xp y))
% y
------------------------------------------------------------------------------
inspect (plus2 (suc (suc zero)) (suc (suc zero)))
=> suc (suc (suc (suc zero))) : Nat
------------------------------------------------------------------------------
( x, y : Nat ! ( x, y, n : Nat !
data !--------------! where !--------------------------!
! Plus x y : * ) ! retPlus x y n : Plus x y )
------------------------------------------------------------------------------
( x, y : Nat ; p : Plus x y !
let !----------------------------!
! callPlus x y p : Nat )
callPlus x y p <= case p
{ callPlus p y (retPlus p y n) => n
}
------------------------------------------------------------------------------
let (----------------------------------------!
! plusWorks : all x, y : Nat => Plus x y )
plusWorks
=>
lam x =>
elimNat x (lam x => all y => Plus x y) (lam y => retPlus zero y y)
% (lam k ; kh ; y => retPlus (suc k) y (suc (callPlus k y (kh y))))
------------------------------------------------------------------------------
( x, y : Nat !
let !-----------------!
! plus3 x y : Nat )
plus3 x y => callPlus x y (plusWorks x y)
------------------------------------------------------------------------------
inspect (plus3 (suc (suc zero)) (suc (suc zero)))
=> suc (suc (suc (suc zero))) : Nat
------------------------------------------------------------------------------
( n : Nat !
let !--------------!
! fib0 n : Nat )
fib0 n <= rec n
{ fib0 n <= case n
{ fib0 zero => zero
fib0 (suc n) <= case n
{ fib0 (suc zero) => suc zero
fib0 (suc (suc n)) => plus0 (fib0 n) (fib0 (suc n))
}
}
}
------------------------------------------------------------------------------
( S, T : * ! ( s : S ; t : T !
data !--------------! where !---------------------!
! Pair S T : * ) ! pair s t : Pair S T )
------------------------------------------------------------------------------
( n : Nat ; P : Nat -> * !
let !-------------------------!
! Memo n P : * )
Memo n P <= elimNat n
{ Memo zero P => One
Memo (suc k) P => Pair (Memo k P) (P k)
}
------------------------------------------------------------------------------
inspect lam n ; P : Nat -> * => Memo (suc (suc n)) P
=>
(lam n ; P => !
! Pair (Pair (Memo n (lam x => P x)) (P n)) (P (suc n)))
: all n : Nat ; P : all x : Nat => * => *
------------------------------------------------------------------------------
( n : Nat ; P : Nat -> * ; m : all k => Memo k P -> P k !
let !---------------------------------------------------------!
! Gen n P m : Memo n P )
Gen n P m <= elimNat n
{ Gen zero P m => ()
Gen (suc k) P m => [pair (Gen k P m) (m k (Gen k P m))]
}
------------------------------------------------------------------------------
( n : Nat ; P : Nat -> * ; m : all k => Memo k P -> P k !
let !---------------------------------------------------------!
! Rec n P m : P n )
Rec n P m => m n (Gen n P m)
------------------------------------------------------------------------------
( n : Nat ! ( n, x : Nat !
data !-----------! where !-----------------------!
! Fib n : * ) ! returnFib n x : Fib n )
------------------------------------------------------------------------------
( n : Nat ; p : Fib n !
let !----------------------!
! callFib n p : Nat )
callFib n p <= case p
{ callFib n (returnFib n p) => p
}
------------------------------------------------------------------------------
( n : Nat !
let !--------------!
! fib1 n : Nat )
fib1 n <= Rec n
{ fib1 k <= case k
{ fib1 zero []
fib1 (suc k) <= case k
{ fib1 (suc zero) []
fib1 (suc (suc k)) []
}
}
}
------------------------------------------------------------------------------
[This is the helper function which computes fib, given the trail of values.]
------------------------------------------------------------------------------
( n : Nat ; m : Memo n Fib !
let !---------------------------!
! fibBody n m : Fib n )
fibBody n m <= case n
{ fibBody zero m => returnFib zero zero
fibBody (suc n) m <= case n
{ fibBody (suc zero) m => [returnFib (suc zero) (suc zero)]
fibBody (suc (suc n)) m <= case m
{ fibBody (suc (suc n)) (pair s t) <= case s
{ fibBody (suc (suc n)) (pair (pair s t) t')
[returnFib (suc (suc n)) !
=> !% (plus0 (callFib n t) (callFib (suc n) t'))]
}
}
}
}
------------------------------------------------------------------------------
[ ( n : Nat ! !
!let !--------------------! !
! ! fibWorks n : Fib n ) !
! !
! fibWorks n => Rec n Fib fibBody]
------------------------------------------------------------------------------
[ ( n : Nat ! !
!let !--------------! !
! ! fib2 n : Nat ) !
! !
! fib2 n => callFib n (fibWorks n)]
------------------------------------------------------------------------------
[inspect fib2 (suc (suc (suc (suc (suc zero))))) => ? : Nat]
------------------------------------------------------------------------------
[inspect fib2 (suc (suc (suc (suc (suc (suc zero)))))) => ? : Nat]
------------------------------------------------------------------------------
[inspect fib2 (suc (suc (suc (suc (suc (suc (suc zero))))))) => ? : Nat]
------------------------------------------------------------------------------
