## Stream: Beginner Questions

### Topic: Folding over a Map

#### Robert Soeldner (May 16 2021 at 17:43):

Hi, I want to fold over a Map but haven't found fold* in the Map Theory, or did I miss something? :)

#### Max Kirchmeier (May 18 2021 at 12:22):

A Map is at its core just a function and thus not really a structure you can directly fold over. But you should be able to use Finite_Set.fold to do it, provided you can proof that the domain of the map is actually finite:

``````definition map_fold :: "('b ⇒ 'c ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ ('b ⇒ 'c option) ⇒ 'a"
where "map_fold f z m ≡ Finite_Set.fold (λk acc. f k (the (m k)) acc) z (dom m)"
``````

#### Mathias Fleury (May 18 2021 at 12:45):

Remark that you have to prove that the order of the fold does not matter.

#### Lukas Stevens (May 18 2021 at 12:48):

It doesn't matter if the keys are linearly ordered since the dom function is (piecewise) injective.

#### Manuel Eberl (May 18 2021 at 12:51):

In most cases it is probably easiest to just express whatever you want to do in a less "operational" way without a fold. Once you move to actually implementing these maps with a more concrete datastructure, you can then prove that a fold works out.

#### Lukas Stevens (May 18 2021 at 12:52):

I actually proved all of this already but you will have to wait until the next release.

#### Manuel Eberl (May 18 2021 at 12:56):

I don't understand. How can the order of the fold not matter in general? Surely it depends on what the fold operation actually does.

#### Lukas Stevens (May 18 2021 at 12:57):

Ah, the fold as the defined here doesn't work. But you can use `List.fold` over `List.sorted_list_of_set` of `dom m`.

#### Manuel Eberl (May 18 2021 at 12:57):

In any case, my point was that "fold" is a very operational way to think about things, and `'a ⇒ 'b option` is a very abstract view of maps, so the two don't go together easily.

#### Manuel Eberl (May 18 2021 at 12:58):

In all likelihood, the "fold" aspect should really only come in when you're trying to get this whole thing executable with a more concrete representation of maps.

#### Lukas Stevens (May 18 2021 at 12:58):

Both RBTs and AList can implement this fold

#### Manuel Eberl (May 18 2021 at 12:58):

Lukas Stevens said:

Ah, the fold as the defined here doesn't work. But you can use `List.fold` over `List.sorted_list_of_set` of `dom m`.

That can work, but only if you have an ordering on your elements and that is indeed the order that you want to fold over.

#### Manuel Eberl (May 18 2021 at 12:59):

In the end, it probably depends on the exact application.

#### Lukas Stevens (May 18 2021 at 12:59):

With RBTs in mind, that would be the natural order. In general, it is not so clear.

#### Manuel Eberl (May 18 2021 at 13:00):

In any case, it is generally good advice to try not to mix operational aspects into the abstract reasoning. Whether or not that applies here is difficult to say without knowing the exact use case.

#### Lukas Stevens (May 18 2021 at 13:01):

One should probably only add this operation to `mapping` and not to `map`.

#### Lukas Stevens (May 18 2021 at 13:02):

In fact, that is exactly what I did in my changes.

#### Manuel Eberl (May 18 2021 at 13:12):

Indeed, `Mapping` is intended to be something of a first step of refining "mathematical maps" (i.e. partial functions) to actual implementations

#### Robert Soeldner (May 19 2021 at 18:52):

Thank you for the amount of comments. Still, I'm not able to follow most comments. See below for a minimal example of my current issue. Basically, I have a finite map containing id's and their corresponding object. The folding function should accumulate some state.

``````fun test1 :: "(nat, bool) fmap ⇒ bool" where
"test1 m = (let t = fmdom m in ffold (λv a. the (fmlookup m v) ∧ a) True t)"

value "test1 (fmupd 1 False fmempty)"
``````

I guess, the error reports, `nat` is not finite.

``````Wellsortedness error
(in code equation test1 ?m ≡ Let (fmdom ?m) (ffold (λv. (∧) (the (fmlookup ?m v))) True),
with dependency "Pure.dummy_pattern" -> "test1"):
Type nat not of sort finite
No type arity nat :: finite
``````

#### Mathias Fleury (May 20 2021 at 04:59):

I expect

``````ffold (λv a. v ∧ a) True (fmran mymap)
``````

to be easier to manipulate than your `ffold+fmlookup` definition, but it is not executable either.

#### Mathias Fleury (May 20 2021 at 05:04):

Here is a way to make it work, by providing a characterization directly over the fset, but that might not be applicable to your real example:

``````definition myfold where
‹myfold = ffold (λv a. v ∧ a)›

lemma [code]:
‹myfold b A ⟷ b ∧ False |∉| A›
proof -
interpret comp_fun_commute ‹(λv a. v ∧ a)›
by standard auto
show ?thesis
unfolding myfold_def
by (induction A) auto
qed

value "myfold True ((fmran (fmupd (1::nat) False fmempty))) "
``````

#### Robert Soeldner (May 23 2021 at 18:19):

Following up on this, even the more simplified version fails to be executed. See:

``````definition bla1 :: "nat fset ⇒ bool" where
"bla1 n = (ffold (λeid a. True ∧ a) True n)"

value "bla1 {|1,2,3|}"
``````

with

``````Wellsortedness error
(in code equation bla1 ?n ≡ ffold (λeid. (∧) True) True ?n,
with dependency "Pure.dummy_pattern" -> "bla1"):
Type nat not of sort finite
No type arity nat :: finite
``````

From the error message, I assume it is expected that `nat` is finite?

Last updated: Sep 11 2024 at 16:22 UTC