Re: [Hol-info] How can I correct the type?

[Anthony F. <ac...@ca...>]

Hi,

My guess for the correct definition is:

val det = Define`
    det (A:('n ,'n) matrix) =
      sigma (\p. (sign (dimindex(:'n)) p) *
                 (product (1n, dimindex(:'n))
                   (\(k:num). (A ' k ' (p (k)))):real))
            { (p:num -> num) | permutes (dimindex(:'n)) p}`;

This fixes a few things:

1. "prod_iter" wasn't defined, so replaced it with "product".
2. "sigma" requires a map as the first argument, so added "\p. ".
3. "dimindex(:'n)" needed to be surrounded by brackets.
4. "%%" syntax is not supported in the latest release, it has been  
replaced with '.  You can an overload if you like the old syntax.

Anthony

On 12 Oct 2010, at 13:28, anythingroom wrote:

> 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小时发货上门！  
> ------------------------------------------------------------------------------
> 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...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info