Another option is to use finite Cartesian products, which are defined in
src/n-bit/. This is very similar to Konrad's approach, except for the handling
of the number of rows and columns, which is done through the type system. For
example, you would have
load "wordsLib"; (* loads finite Cartesian products and gets evaluation
working *)
val vprod_def =
Define
`vprod (v1:num['a]) (v2:num['a]) =
Sigma 0 (dimindex(:'a)-1) ((FCP i. (v1 ' i) * (v2 ' i)):num['a])`;
val matrix_prod_def =
Define
`matrix_prod (M1:num['a]['b]) (M2:num['c]['a]) =
(FCP r c. vprod (M1 ' r) (FCP r. M2 ' r ' c)) : num['c]['b]`;
val fromLists_def =
Define
`fromLists lists = FCP r c. EL c (EL r lists)`;
val matA_def =
Define
`matA = fromLists [[1;2;3;4]; [2;3;5;7]; [9;8;7;2]] : num[4][3]`;
val matB_def =
Define
`matB = fromLists [[1;2]; [5;7]; [8;7]; [11;3]] : num[2][4]`;
EVAL ``(matrix_prod matA matB) ' 1 ' 1``; (* Should be 81 *)
FCP is a binder, used to define finite Cartesian products -- the size is given
by the function dimindex. Type annotations are needed when using fromLists
because the definition doesn't (can't) examine the lists to get the correct
dimensions.
For a HOL beginner, I would expect proofs to be a little more tricky with this
approach. However, there is the advantage that side conditions are no longer
required e.g. you would just prove
matrix_prod A (matrix_prod B C) = matrix_prod (matrix_prod A B) C
Cheers,
Anthony.
On 12 Apr 2010, at 04:32, Konrad Slind wrote:
> Hi Amy,
>
> Matrices are an interesting modelling example, since there are
> several
> viable approaches. For extreme simplicity, I would use functions of
> type
>
> num -> num -> 'a
>
> to represent them. That makes many of the basic operations quite easy.
> You will also need to include the rows and columns. This leads to the
> idea of having a record hold the rows, columns, and indexing function:
>
> Hol_datatype
> `matrix = <| rows:num; cols:num; index:num->num->'a |>`;
>
> To then define an operation like matrix multiplication, you need a
> summation
> function:
>
> val Sigma_def =
> tDefine
> "Sigma"
> `Sigma lo hi f =
> if lo > hi then 0 else f(lo) + Sigma (lo+1) hi f`
> (WF_REL_TAC `measure (\(lo,hi,f). (hi+1) - lo)`);
>
> WIth that you can define the finite product of two vectors:
>
> val vprod_def =
> Define
> `vprod v1 v2 k = Sigma 0 (k-1) (\i. v1(i) * v2(i))`;
>
> And then the matrix product is
>
> val matrix_prod_def =
> Define
> `matrix_prod (M1:num matrix) (M2:num matrix) =
> <|rows := M1.rows ;
> cols := M2.cols ;
> index := \r c. vprod (M1.index r) (\r. M2.index r c)
> M1.cols |>`;
>
> It also helps for testing to have something that makes a matrix from a
> list of lists:
>
> Define
> `fromLists lists =
> <| rows := LENGTH lists;
> cols := LENGTH (HD lists);
> index := \r c. EL c (EL r lists) |>`;
>
> A test:
>
> val matA_def =
> Define
> `matA = fromLists [[1;2;3;4]; [2;3;5;7]; [9;8;7;2]]`;
>
> val matB_def =
> Define
> `matB = fromLists [[1;2]; [5;7]; [8;7]; [11;3]]`;
>
> EVAL ``(matrix_prod matA matB).index 1 1``; (* Should be 81 *)
>
> Then you of course have to prove some theorems about the product.
> An obvious one would be associativity. Note that you have to constrain
> the matrices appropriately.
>
> (A.cols = B.rows) /\ (B.cols = C.rows)
> ==>
> ( matrix_prod A (matrix_prod B C) = matrix_prod (matrix_prod A B) C
>
> I haven't tried this proof, so there may be lurking problems with the
> above
> formulation. But the general idea should be clear. I would be keen to
> hear
> of other formalizations of matrices, since, as I mentioned, there are
> multiple
> ways to skin this cat.
>
> For example, another approach would be to use a list of equal-length
> lists
> to represent the matrix, but my experience with that approach was
> kind of
> negative: I got bogged down in relatively horrible inductions to prove
> even simple theorems.
>
> Cheers,
> Konrad.
>
>
>
> On Apr 11, 2010, at 9:42 AM, anythingroom wrote:
>
>> Hi everyone，
>>
>>
>>
>> Who know the different between with type and datatype in HOL4? I
>> wanted to define a new type for matrix in HOL4, but I might be
>> confusing type with datatype. I didn’t know how to start to define
>> the type of matrix.
>>
>>
>>
>> Who can help me ? Thank you very much. I’m looking for your reply.
>>
>>
>>
>> Best wishes,
>>
>> Amy
>>
>>
>>
>> ----------------------------------------------------------------------
>> --------
>> Download Intel® Parallel Studio Eval
>> Try the new software tools for yourself. Speed compiling, find bugs
>> proactively, and fine-tune applications for parallel performance.
>> See why Intel Parallel Studio got high marks during beta.
>> http://p.sf.net/sfu/intel-sw-
>> dev_______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> ------------------------------------------------------------------------------
> Download Intel® Parallel Studio Eval
> Try the new software tools for yourself. Speed compiling, find bugs
> proactively, and fine-tune applications for parallel performance.
> See why Intel Parallel Studio got high marks during beta.
> http://p.sf.net/sfu/intel-sw-dev
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
