Re: [tlaplus] n-ary Cartesian product

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

On 20 Oct 2020, at 14:09, Mariusz Ryndzionek <mryndzionek@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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/777d286f-858b-42c2-ac89-1d2eac77f01en%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8e33ff4b-097b-43a8-b58a-e35010782ae2n%40googlegroups.com.