# Re: [tlaplus] n-ary Cartesian product

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.

wtorek, 20 października 2020 o 14:40:44 UTC+2 alex.we...@xxxxxxxxxxxxxxxx napisał(a):
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].

On Tuesday, October 20, 2020 at 8:09:16 AM UTC-4 mrynd...@xxxxxxxxx wrote:
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?

wtorek, 20 października 2020 o 13:41:38 UTC+2 Stephan Merz napisał(a):
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

On 20 Oct 2020, at 13:27, Mariusz Ryndzionek <mrynd...@xxxxxxxxx> wrote:

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

--
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...@xxxxxxxxxxxxxxxx.