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
Lecturer in Automated Verification
University of Southampton - School of Electronics and Computer Science
http://www.jobs.soton.ac.uk/soton/jobboard/JobDetails.aspx?__ID=*638C9CD43034EAA6
£34,607 - £43,840 per annum
Applications are invited for a Lecturer to join the School of Electronics and
C
*
1st Call for Papers
5th INTERNATIONAL CONFERENCE ON LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS
(LATA 2011)
Tarragona, Spain, May 30 – June 3, 2011
http://grammars.grlmc.com/LATA2011/
*
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}`;
T
