Add Reduce operator to Functions

[lemmy]

Reduce(op(_,_), fun, from, to, base) == 
  (**************************************************************************)
  (* Reduce the elements in the range from..to of the function's co-domain. *)
  (**************************************************************************)
  LET reduced[i \in from..to] ==
          IF i = from THEN op(base, fun[i])
          ELSE op(reduced[i - 1], fun[i])
  IN reduced[to]

/cc @muenchnerkindl @konnov @quicquid

[quicquid]

We had a discussion that the current Reduce operator from FiniteSetsEx is a bit restrictive: it works only on functions with integer domain but it also works on sets. On the other hand, it is sometimes needed not to reduce on the full domain, as @lemmy's example from the ewd998 formalization shows. I have added the operators to a branch in my fork of the community modules. What do you think?

[lemmy]

As mentioned in today's call, I suggest moving the functions-related operators out of FiniteSetsExt to Functions.tla or moving all fold operators to a new module. I - as a user - wouldn't have looked for functions-related fold operators in FiniteSetsExt. If it is decided to split the operators across FiniteSetsExt and Functions.tla, comments could point users to the other variants.

Speaking of comments, the format that is the best support by tools, i.e., IDE is:

OpDecl(params) ==
   (************)
   (* comments *)
   (* comments *)
   (* comments *)
   (************)
   TheOperatorDefinition

I'd also suggest adding an example invocation in the comment as in:

CommunityModules/modules/FiniteSetsExt.tla

Lines 71 to 75 in 4337afb

	(* Compute all sets that contain one element from each of the input sets: *)
	(* *)
	(* Example: *)
	(* Choices({{1,2}, {2,3}, {5}}) = *)
	(* {{2, 5}, {1, 2, 5}, {1, 3, 5}, {2, 3, 5}} *)

Lastly, there is a precedence of operator aliasing:

CommunityModules/modules/SequencesExt.tla

Lines 34 to 46 in 4337afb

	SeqOf(set, n) ==
	(***************************************************************************)
	(* All sequences up to length n with all elements in set. Includes empty *)
	(* sequence. *)
	(***************************************************************************)
	UNION {[1..m -> set] : m \in 0..n}
	BoundedSeq(S, n) ==
	(***************************************************************************)
	(* An alias for SeqOf to make the connection to Sequences!Seq, which is *)
	(* the unbounded version of BoundedSeq. *)
	(***************************************************************************)
	SeqOf(S, n)

---

PS: TLC takes 2-3 minutes on a laptop to check EWD998 for N=3 and the given state constraint: https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998.cfg

[lemmy]

Restrict operator mentioned by @muenchnerkindl :

CommunityModules/modules/Functions.tla

Lines 10 to 13 in 4337afb

	(***************************************************************************)
	(* Restriction of a function to a set (should be a subset of the domain). *)
	(***************************************************************************)
	Restrict(f,S) == [ x \in S |-> f[x] ]

[muenchnerkindl]

In fact, FoldMap and friends do not use any operator defined in either Functions or FiniteSets, so I believe it would be best to place them in a separate module. Also, please remove the comment in the definition of FoldSet that refers to the operator ReduceSet that will disappear. For the rest, I agree with @lemmy's comments. And I don't know if "FoldMap" is a good name?

[lemmy]

WRT the functions/sequence-based folds, what about non-associative operators (fold left vs. right)? Do we want to open that can of worms?

[muenchnerkindl]

I'd be in favor for having those for sequences (or perhaps for functions whose domain is an interval of integers). I don't think it's worth having them for arbitrary functions: you need a total order on the domain for those notions to make sense, so doing it in full generality would require auxiliary definitions for little gain in expressiveness.

[konnov]

In fact, FoldMap and friends do not use any operator defined in either Functions or FiniteSets, so I believe it would be best to place them in a separate module.

I also think that we could place all fold-like operators in a separate module, like Fold.tla or even Recursion.tla. Perhaps, we will discover other forms of recursive operators that are useful in the context of TLA+.

[lemmy]

Given that we have Functions, Sequences, FiniteSets, ..., I'd suggest making it Folds.tla (with an "s" at the end). However, we already have Graphs, Sequences, Functions to which the folds are applied. Instead of a gigantic Folds.tla, why not move the fold operators to the data-structure modules to which they apply?

[konnov]

And I don't know if "FoldMap" is a good name?

True. Would MapThenFoldSet work better? It essentially does a map and then fold.

[quicquid]

I have created one Folds module for the complicated MapThenFoldSet definition that probably shouldn't be used directly (see comment there) and put the changes into a pull request draft that it's easier to compare. I don't think it's ready yet - the least I'm missing is test cases.

I'm wondering two things:

1. Would we also like folds on Graphs? Should we alias FoldSequence in FoldFunction?
2. As @muenchnerkindl said foldLeft / foldRight, we would need an ordering on the set - I could add an ordering to MapThenFoldSet such that we could implement it easily for sequences. Would we want that?

[quicquid]

I have added the FoldLeft / FoldRight definitions to SequencesExt (and removed ReduceSeq)
Edit: I just realized I ordered the values not the indices, please still disregard FoldLeft / FoldRight

[lemmy]

#38 and 0b5fcd4 address this issue.