Replace definition of `FlattenSet` with `UNION`

[lemmy]

FlattenSet({{1},{2}}) = UNION {{1},{2}}

https://github.com/tlaplus/CommunityModules/blob/e88b5536133eaf0ad68c698d618480c9a84f4192/modules/FiniteSetsExt.tla#L42-L51

@konnov @Kukovec @quicquid

[jonesmartins]

Hi, I have a question.

Would it be useful to have a more “general” definition of flattening, in the sense that such a function would flatten all its elements. In this case, FlattenSet({ {0}, {{1}}, {{{2}}} }) would evaluate to { 0, 1, 2 }. FlattenSeq would be analogous.

Then UNION wouldn't equal FlattenSet here. This new definition would be more “powerful”, although I wonder about a use case.

Anyway, just a thought.

[quicquid]

I'm not sure if this is going to be useful - after all in set theory, everything is a set. To my knowledge, TLA+ does not define the inner structure of numbers like 1 but they are certainly sets (a possible construction defines 0 as {}, 1 as {{}}, 2 as {{}, {{}}}, etc. - an unlimited flattening would be {{}} for all numbers apart from 0).

Just to be sure, I also tried to prove that every object is either the empty set or contains at least one element in TLAPM and it agrees:

LEMMA ASSUME NEW CONSTANT C
             PROVE C = {} \/ \E x \in C : TRUE OBVIOUS (* proved by TLAPM *)

So as soon as we have some opaque set, the flattening operation would not be well founded anymore (we would need to do a case distinction for the empty set and the one containing elements. But in the latter case we could repeat the procedure on each of the elements and never stop recursing).

In the case of model checking with TLC, the task is a bit simpler because the contents of each set must be known in advance and be finite. One could define some sets as non-flattenable and get a definition that's useful in this situation but I'm not sure how well it fits into TLA. (Perhaps someone else wants to comment as well?)

[quicquid]

I became curious and tried to define such an operator relative to a set of primitives

RECURSIVE DeepFlatten(_,_)
DeepFlatten(S, Primitives) ==
 FoldSet(LAMBDA x,y : LET rx == IF x \in Primitives 
                                THEN {x}
                                ELSE DeepFlatten(x, Primitives)
                      IN rx \cup y, {}, S)

TestA == DeepFlatten({{{0}},{{1},{2}}}, {0,1,2})
TestB == DeepFlatten({{{{0}}},{{{1}},{{2}}}}, {0,1,2})
TestC == DeepFlatten({{{0}}}, {0,1,2})

but then I realized that TLC does not allow the comparison of sets with different nesting (e.g. evaluating TestC leads to "Attempted to check equality of integer 0 with non-integer: {{0}}"). Your example mixes the nestings such that TLC can not model check it either (it's a valid expression of TLA but outside the range of expressions that TLC can efficiently check).

I thought I could get my way around by first measuring how many times the flattening operation would need to be iterated first but defining such an operator leads to the same problems. This version

RECURSIVE Depth(_)
Depth(S) == IF S = {} THEN 0 ELSE 1 + Depth(CHOOSE x \in S: \A y \in S \ {x}: Depth(x) >= Depth(y))

suffers from the same problem as above (i.e. works for e.g. {{},{{}}} but not for {{},{{1}}}) and I would need to make the trick I tried above work again.

[jonesmartins]

It'd be easier if we could compare types like in programming languages, but TLA+ isn't one :S

If we could try-except in TLA+ maybe this would work? Funnily enough, you mentioned numbers as sets. If we could check whether an element has a domain, -- including numbers --, we'd be able to flatten deep sequences, at least.

In any case, to flatten a sequence, the key would be to check if an element inside it is a sequence (or check if it's not a sequence, whichever is easiest?).

Here's my prototype on flattening sequences:

DeepFlattenSeq(seq):
    LET 
        IsSequence(seq) == seq \in Seq(Any)  # Error.
        head == Head(seq)
        tail == Tail(seq)
    IN
        IF seq = << >>
        THEN seq
        ELSE IF IsSequence(head)
             THEN DeepFlattenSeq(head) \o DeepFlattenSeq(tail)
             ELSE <<head>> \o DeepFlattenSeq(tail)

[Kukovec]

You'll never be able to define IsSequence(seq) the way you want and here's why:

Russel's paradox demonstrates that there cannot be a "set of all sets" (you need a category). Similarly, you cannot have the "set of all sequences", because the two are mutually definable: the "set of all sequences" would just be UNION {Seq(S): S \in "set of all sets"} and the "set of all sets" would be {Image(seq): seq \in "set of all sequences"}. IsSequence(seq) is essentially seq \in "set of all sequences".

But suppose you could circumvent that problem by unbounded quantification and define IsSequence(seq) == \E S: seq \in Seq(S) (notably, not \E S \in Something: ...), at best, you'd get a predicate that evaluates to TRUE on all sequences, but that doesn't mean it will evaluate to FALSE anywhere else. IsSequence(1) would be \E S: 1 \in Seq(S), but when trying to evaluate 1 \in Seq(S) you run into the same problem of "what is a set?" Martin demonstrates above.

Fundamentally, 1 = <<>> is an undefined expression in TLA, much like the textbook example 3/"abc". One of the basic properties of predicates is that x = y implies P(x) = P(y), which is equivalent to P(x) /= P(y) implying x /= y. If you could define IsSequence, presumably you'd expect IsSequence(1) = FALSE and IsSequence(<<>>) = TRUE. But if you had such a predicate 1 = <<>> would not be undefined, which it is. Contradiction.

So the predicate cannot be defined, and without it, you can't specify a termination condition for recursion.

[jonesmartins]

Thank you, @Kukovec! I couldn't justify why it'd be wrong to compare different “types”. It seems to me that the only way to define IsSequence(S) would be through a try-except structure, right?

So I assume we can only flatten s \in Seq("sequences of depth <depth>")? FlattenSeq in the SequencesExt module "removes" one depth. A DeeplyFlattenSeq would need to apply it <depth> times then.