Hi everyone,
I have to define the determinant
definition in HOL4 and I define it as following:
val det =
Define ` det (A:('n ,'n) matrix)
= sigma ( (sign (dimindex(:'n)) p) * ( prod_iter ( (1:num), dimindex(:'n) )
(\(k:num). (A %% k %% (p (k) ) ) ):real ) ) { (p:num -> num) | permutes
dimindex(:'n) p}`;
But there are some errors on typecheck.
<<HOL message: inventing new type
variable names: 'a>>
Type inference failure: unable to infer a
type for the application of
(sigma :('a -> real) -> ('a ->
bool) -> real) :('a -> real) -> ('a -> bool) -> real
on line 50, characters 46-50
to
sign (dimindex ((:'n)
:'n itself)) (p :num -> num) *
(prod_iter :num # num
-> (num -> real) -> real)
((1 :num),dimindex ((:'n) :'n itself))
(\(k :num). (A :('n, 'n) matrix) %% k %% p k)
on line 50, characters 54-160
which has type
:real
unification failure message: unify failed
Exception raised at Preterm.typecheck:
on line 50, characters 54-160:
failed
! Uncaught exception:
! HOL_ERR
Because the blue part has real type not “’a
-> real” type?
How can I correct the definition of
determinant?
Could anybody give me some hints?
I really appreciate your help!
The loaded libraries are listed here:
app
load["HolKernel","bossLib","fcpTheory","listTheory","wordsLib","realTheory","realLib",
"simpLib","boolTheory","boolLib","mesonLib","Parse","fcpLib","pred_setTheory"];
open HolKernel bossLib fcpTheory listTheory wordsLib
realTheory realLib simpLib boolTheory
boolLib mesonLib Parse fcpLib pred_setTheory;
val _ = type_abbrev ("matrix", ``:(real ** 'a) ** 'b``);
val permutes =
Define ` permutes (n:num) (p:num -> num) =(!i. (i =
0) ==> (p i = i)) /\ (!i. (i < SUC n) ==> (p i < SUC n)) /\ (!y.
?!i. p i = y)`;
val productc = Define ` (productc n 0 f = 1) /\
(productc n (SUC m) f = productc n m f * f(n+m))`;
val product = Define ` product(m,n) f = productc m n
f`;
val prod_iter = store_thm("prod_iter", ``!f
m n. (product(n,0) f = 1) /\
(product(n, SUC m) f = product(n,m) f * f (n+m))``,
REWRITE_TAC [productc,product]);
val nixu = Define` nixu (n:num) (p: num -> num) =
{i:num ,j| ((i < j) /\(j < n)) /\ (p i > p j)}`;
val _ = overload_on ("nixu", ``nixu : num
-> (num -> num) -> num # num ->bool``);
val evenperm = Define`evenperm n p = EVEN (CARD(nixu n
p))`;
val _ = overload_on ("evenperm", ``evenperm
: num -> (num -> num) -> bool``);
val sign = Define`sign n p = if evenperm n p then 1
else ~1`;
val _ = overload_on ("sign", ``sign : num
-> (num -> num) -> real``);
val sum_image_real = Define`sigma (f :'a -> real)
(s :'a -> bool) = ITSET (\(e :'a) (acc :real). f e + acc) s (0 :real)`;
Amy
全国最低价，天天在家冲照片，24小时发货上门！
best Rasmus ------------------------------------------------------------------------------ Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novell-sfdev2dev
RSS Feed