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: Dec 21 2024 at 16:20 UTC