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------------------------------------------------------------------------------
Beautiful is writing same markup. Internet Explorer 9 supports
standards for HTML5, CSS3, SVG 1.1, ECMAScript5, and DOM L2 & L3.
Spend less time writing and rewriting code and more time creating great
experiences on the web. Be a part of the beta today.
http://p.sf.net/sfu/beautyoftheweb
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
