Yes, as Kummar said, you can use SIGMA to express summation in your
function C[i,j] = sum z=1..n A[i,z]*B[z,j], but in some case, you can also
use sum.
Using sum (in realTheory) or SIGMA (in pred_setTheory) to express such a
function, it depends on the type of the "index" z (in fact, it's the
parameter of functions A[i, z] and B[z, j]) in your expression.
If the result of the summation (C[i,j]) is a real number and "z" is a
nature number, you can use sum or SIGMA to express it. For example, you can
use sum as following:
C i j = sum (0, n) (\z. (A i z) * (B z j)).
Kumar has already given the example using SIGMA.
If the type of z is not a nature number, and this summation is based on a
set, then it's better for you to use SIGMA. For example, z IN (s:'a ->
bool), in this case, you can use: SIGMA (\(z:'a). (A i z) * (B z j)) s.
Otherwise, you need another function to map s to the set (count n), then
use sum to do it. It will be a little complex ...
In a summary, when you are doing summation based on a set, in which
elements are not nature number, it's better to use SIGMA; when the
summation is based on an index, which is nature number, it's better to use
sum.
However, if the type of C[i, j] is not real number (in this case functions
A and B have the same type of C), either you convert the type of A and B to
be real or your develop some theorems similar as those based on sum or
SIGMA using the corresponding type (such as integer, extended real number),
for example, SUM_2 and SUM_IMAGE_ZERO, and so on.*
*Good Luck,
Liya*
*
2012/6/17 Ramana Kumar <[email protected]>
> The constant ``SIGMA`` in pred_setTheory can be used to express a sum.
>
> It has type ``:('a -> num) -> ('a set) -> num``.
>
> So, for example, to do the sum of f(z) for z in 1..n, you could use:
>
> ``SIGMA (\z. f (z+1)) (count n)``
>
> On Sat, Jun 16, 2012 at 4:27 PM, Thomas Melham <
> [email protected]> wrote:
>
>> Dear Anggha,
>>
>> I'm afraid it's been a very long time since I was a HOL user, so I
>> can't answer your question. But I hereby forward your query to the HOL
>> mailing list, hoping some active user can help.
>>
>> Best regards,
>> Tom
>>
>> From: Anggha Nugraha <[email protected]>
>> Reply-To: Anggha Nugraha <[email protected]>
>> Date: Tuesday, 12 June 2012 06:14
>> To: Tom Melham <[email protected]>
>> Subject: Asking about HOL TP (sum syntax)
>>
>> Good evening Professor Melham.
>>
>> Firstly, let me introduce my self. My name is Anggha and now I'm a
>> master student in Faculty of Computer Science in University of Indonesia.
>> Now, I'm making my master thesis about proving the partial correctness of
>> matrix multiplication program. I plan to making the manual proof using
>> Hoare logic and then making the automation in HOL Theorem Proving.
>>
>> I have read your paper entitled,"A MECHANIZED THEORY OF THE -CALCULUS IN
>> HOL" and I know that you're an expert in HOL TP.
>>
>> I have a problem in writing in HOL. I wanna write: C[i,j] = sum z=1..n
>> A[i,z]*B[z,j]
>> I use # to indicate array, so C[i,j] is written as (C#i)#j. Am I right
>> doc?
>>
>> About the summation, I don't have any idea how to write this in HOL.
>> How I define the syntax of sum? What library that I have to use prof?
>> May you help me prof? And if you don't mind, can you give me an example?
>>
>> Thank you very much Prof. Melham and I really sorry if I disturb you
>> prof.
>>
>> --
>> Best regards,
>> Anggha Satya Nugraha
>> Graduate Student in Faculty of Computer Science
>> University of Indonesia (Universitas Indonesia)
>>
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Live Security Virtual Conference
>> Exclusive live event will cover all the ways today's security and
>> threat landscape has changed and how IT managers can respond. Discussions
>> will include endpoint security, mobile security and the latest in malware
>> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
