n-ary Cartesian product

[Mariusz Ryndzionek]

Hello,

I need n-ary Cartesian product operator. Something that would do:

Cartesian({S1, S2, .., Sn}) = S1 \X S2 \X .. Sn

The output shouldn't necessarily be sequences. Sets will do.

Is there already something like this in TLA+?

Regards,

Mariusz

[Stephan Merz]

Hello,

your problem is not well specified because {S1, S2} = {S2, S1} but S1 \X S2 is different from S2 \X S1. Also, I don't understand your remark about the output: the cartesian product is a set, but its elements are sequences.

Assuming that your operator takes a *sequence* of sets, i.e. Cartesian(<<S1, S2, ..., Sn>>), you can write the following in TLA+.

Range(S) == { S[i] : i \in 1 .. Len(S) }

Cartesian(S) == 

  LET U == UNION Range(S)

  IN  {s \in Seq(U) : /\ Len(s) = Len(S)

                      /\ \A i \in 1 .. Len(s) : s[i] \in S[i]}

However, TLC will not be available to interpret this because of the quantification over the infinite set Set(U). The following should work in principle (I haven't actually tried):

Cartesian(S) == 

  LET U == UNION Range(S)

      FSeq == [ (1 .. Len(s)) -> U ]

  IN  {s \in FSeq : \A i \in 1 .. Len(s) : s[i] \in S[i]}

However, you probably want to override this operator definition by a Java method.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/777d286f-858b-42c2-ac89-1d2eac77f01en%40googlegroups.com.

[Mariusz Ryndzionek]

Okay, so I wasn't specific enough. I know that \X in TLA+ is not commutative and in fact not even associative.

I wanted something that would give me:

Cartesian({{1, 2}, {3, 4}, {5}}) = {{1, 3, 5}, {1, 4, 5}, {2, 3, 5}, {2, 4, 5}}

Your last definition works in TLC. Thanks Stephan!

Is the `Range` operator defined somewhere in official/builtin modules?

Range(f) == { f[x] : x \in DOMAIN f }

Regarding overriding in Java, is it recommended only for to performance reasons?

[Alex Weisberger]

Do records work for this use case?

If you use a record with a name for the value of each set, you can do:

r == [s1: S1, s2: S2, ... sn: Sn]. 

This does give you the Cartesian product of all of the sets S1-Sn, but instead of plain tuples it assigns a name to each value that would be in the tuple, 

i.e. if S1 = {1,2,3} and S2 = {4,5,6} then [s1 |-> 1, s2 |-> 4] \in [s1: S1, s2: S2].

[Mariusz Ryndzionek]

Yes, I think this would be okay, but wanted to say again that this is not a problem for me.

Maybe I should've used a different name than Cartesian.

Cartesian product (and \X) has this property that the length 

of all the output sequences is the same as the cardinality of the input set (of sets).

In my case I don't care if the lengths are different and some elements are 'annihilated'.

I'll test Stephan's solution and just map Range over all the output elements.

[Markus Kuppe]

On 20.10.20 05:09, Mariusz Ryndzionek wrote:
> Regarding overriding in Java, is it recommended only for to performance
> reasons?

Hi Mariusz,

indeed, Java module overwrites are just a performance optimization for TLC.

Almost all standard modules (Sequences, FiniteSets, ...) and some of the
CommunityModules [1] come with overwrites. The benchmark at [2] gives an
intuition of a realistic performance increase^1. Use engineering
judgment to decide if the performance boost warrants the additional
complexity.

Markus

[1] https://github.com/tlaplus/CommunityModules/tree/master/modules
[2]
https://jmh.morethan.io/?sources=https://raw.githubusercontent.com/tlaplus/tlaplus/master/tlatools/org.lamport.tlatools/test-benchmark/tlc2/tool/ModuleOverwrites-1531220029-80dc6de2b.json

1
"aNoModuleOverwrite" == baseline with no overwrite
"bModuleOverwrite" == direct translation of TLA+ operator into Java code
"cModuleOverwriteLinear" == Human being clever about the translation

[Stephan Merz]

Thanks for the explanations. This operator (I renamed it to Shuffle for lack of a better name) could be defined as follows.

Range(f) == {f[x] : x \in DOMAIN f}

(***************************************************************************) 

(* If Sets is a set of (non-empty) sets then Choice(Sets) is the set of    *)

(* all choice functions over Sets, that is, functions that associate some  *)

(* with every set in Sets.                                                 *) 

(***************************************************************************) 

Choice(Sets) == { f \in [Sets -> UNION Sets] : \A S \in Sets : f[S] \in S }

(***************************************************************************) 

(* Compute all sets that contain one element from each of the input sets:  *)

(* Shuffle({{1,2}, {3,4}, {5}}) = {{1,3,5}, {1,4,5}, {2,3,5}, {2,4,5}}     *)

(***************************************************************************) 

Shuffle(Sets) == { Range(f) : f \in Choice(Sets) }

Regards,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8e33ff4b-097b-43a8-b58a-e35010782ae2n%40googlegroups.com.

[Mariusz Ryndzionek]

Thanks Stephan and Markus! 

[JosEdu Solsona]

Hello,

I'm wondering if it is possible to define a n-ary cartesian operator like the one proposed by Stephan: 

Cartesian(S) == 

  LET U == UNION Range(S)

      FSeq == [ (1 .. Len(S)) -> U ]

  IN  {s \in FSeq : \A i \in 1 .. Len(s) : s[i] \in S[i]}

except it also work with sequences of sets of possible different types.

For example, TLC doesn't have any problem computing something like {1,2} \X {"A","B"}. 

But it will fail to evaluate Cartesian(<<{1,2},{"A","B"}>>) because it can't compare numbers with strings.

Alternatively, can these "limitation" be circumvented if the operator is overridden with an appropriate Java method?

Regards,

José

[Stephan Merz]

Hi José,

in that case I'd suggest using a recursive definition such as the one below. In my original answer to Mariusz I tried to avoid using recursion, but this requires bounding the base set of sequences, which makes TLC balk when the sets are heterogeneous.

I haven't tried writing a Java override of the operator definition.

Regards,

Stephan

(***************************************************************************)

(* Given a sequence s = <<S1, ..., Sn>> of sets, Cartesian(s) computes the *)

(* n-ary Cartesian product of these sets, i.e. the set of all sequences    *)

(* whose i-th element belongs to the set Si. For example,                  *)

(* Cartesian(<<{1,2}, {"a", "b"}, {{}}>>) =                                *)

(*   {<<1, "a", {}>>, <<1, "b", {}>>, <<2, "a", {}>>, <<2, "b", {}>>}      *)

(***************************************************************************)

RECURSIVE Cartesian(_)

Cartesian(s) ==

  IF s = << >> THEN { << >> }

  ELSE LET C == Cartesian(Tail(s))

           AllCons(seq) == { <<x>> \o seq : x \in Head(s) }

       IN  UNION { AllCons(seq) : seq \in C }

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/75847d4b-4d20-4b19-86ca-f7653292137cn%40googlegroups.com.

[JosEdu Solsona]

Hello Stephan,

Thanks for that.  As TLAPS  handles only recursive function definitions, i have rewritten your operator in terms of a recursive function but
doing recursion over the length ("structural" recursion over the sequence itself would need to declare its domain and TLC
would balk me again!):

Cartesian(s) ==

  LET F[k \in 0..Len(s)] ==

    IF k = 0

    THEN { << >> }

    ELSE LET C == F[k-1]

             AllCons(seq) == { seq \o <<x>> : x \in s[k] }

         IN  UNION { AllCons(seq) : seq \in C }

  IN F[Len(s)] 

However, as i'm planning to use this only for type correctness, ie x \in Cartesian(<<s1,..,sn>>), i think i'm going to end overriding it anyway 
as the enumeration would be too costly for TLC. But considering this, i will try first with the non-recursive option, which should be easier too handle in TLAPS.

Regards,

José