Stream: Beginner Questions

Topic: Un-indexed sum of finite set of numbers

Chengsong Tan (May 23 2023 at 11:46):

Hi community,

I am looking for ways to represent functions (maps) on a finite domain and be able to count certain entries in that map easily.
Say I want to express a system which has two blocks which can be in different states. Such a system can be expressed by a function which we call block_map.

datatype BlockID = Block1 | Block2
datatype MESI_State = Modified| Exclusive| Shared| Invalid

type_synonym block_map = "BlockID ⇒ MESI_State"

It is clear that block_map is defined on a finite domain.
Now if we define a function that count the number of blocks that are in a Shared state, it would look like the following:

fun count_sharers :: "block_map ⇒ nat"
  where "count_sharers f = finite_sum ((λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) ` (f ` (UNIV::BlockID set)))"

It is not sure how the function finite_sum which sums all numbers in a finite set should be defined.
A search in the FiniteSet theory entry did not give anything useful.
An alternative is to define the datatype of a BlockID which takes a natural number parameter, and then doing an indexed sum over the blocks. The natural number parameter needs to be restricted to a finite subset of nat to make the sum finite:

datatype BlockIDSet2 = nat{.. < 2}
datatype BlockID2 = Block2 BlockIDSet2


type_synonym block_map2 = "BlockID2 ⇒ MESI_State"

fun count_sharers2 :: "block_map2 ⇒ nat"
  where "count_sharers2 f = (∑i::nat=0..<2.  (λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) (f (Block2 i))   )"

Again I am not sure how to make this finite restriction on datatypes work for Isabelle.

A MWE code snippet:

theory mweFiniteSum imports
  Main
begin


datatype BlockID = Block1 | Block2

datatype MESI_State = Modified| Exclusive| Shared| Invalid

type_synonym block_map = "BlockID ⇒ MESI_State"

fun count_sharers :: "block_map ⇒ nat"
  where "count_sharers f = finite_sum ((λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) ` (f ` (UNIV::BlockID set)))"



datatype BlockIDSet2 = nat{.. < 2}
datatype BlockID2 = Block2 BlockIDSet2


type_synonym block_map2 = "BlockID2 ⇒ MESI_State"

fun count_sharers2 :: "block_map2 ⇒ nat"
  where "count_sharers2 f = (∑i::nat=0..<2.  (λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) (f (Block2 i))   )"


end

Thanks a lot in advance for your help!

Kevin Kappelmann (May 24 2023 at 14:31):

Maybe Finite_Set.fold?

Mathias Fleury (May 24 2023 at 14:36):

Or summing over the set directly:

fun count_sharers :: "block_map ⇒ nat"
  where "count_sharers f = (∑i ∈ (UNIV::BlockID set). if f i = Shared then 1 else 0)"

Mathias Fleury (May 24 2023 at 14:38):

Remark that infinite sets are not really a problem, the sum just becomes empty

thm Groups_Big.comm_monoid_add_class.sum.infinite
 infinite ?A ⟹ sum ?g ?A = 0

Chengsong Tan (May 26 2023 at 10:24):

Mathias Fleury said:

Or summing over the set directly:

fun count_sharers :: "block_map ⇒ nat"
  where "count_sharers f = (∑i ∈ (UNIV::BlockID set). if f i = Shared then 1 else 0)"

Thank you! That works. I forgot to emphasise that I wanted to generate executable code. But this works perfectly regardless.

Chengsong Tan (May 26 2023 at 10:24):

Kevin Kappelmann said:

Maybe Finite_Set.fold?

Thank you for the pointer!

Last updated: Apr 27 2024 at 16:16 UTC