Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] a line of type definition


view this post on Zulip Email Gateway (Aug 19 2022 at 14:28):

From: yongjian Li <lyj238@ios.ac.cn>
Dear experts:
I read line 2404 in Determinats.thy, which is listed as follows:

definition trace :: "'a::semiring_1^'n^'n ⇒ 'a"
where "trace A = setsum (λi. ((A$i)$i)) (UNIV::'n set)"

I can guess A is of type 'a matrix, returns a result with type 'a. (informally)

This is the first time I meet the type cat operator ^, can some experts
interpret it?

Or simply point me which tutorial material I should read .

regards!


Yongjian Li
Associate Research Professor, Ph.D
State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
Beijing, China

Tel: (+86)10 6266 1645
Email:lyj238@ios.ac.cn
Homepage: http://lcs.ios.ac.cn/~lyj238

view this post on Zulip Email Gateway (Aug 19 2022 at 14:28):

From: Lawrence Paulson <lp15@cam.ac.uk>
This is a way of representing an N-dimensional vector space as a type, even though higher-order logic does not have dependent types. The idea is to represent the number N by a type having that many elements.

John Harrison invented this idea, and his exposition is still the best:

http://link.springer.com/article/10.1007%2Fs10817-012-9250-9

Larry Paulson


Last updated: Mar 28 2024 at 12:29 UTC