[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Tue, 20 Oct 2020 17:42:15 -0700 (PDT)*References*: <777d286f-858b-42c2-ac89-1d2eac77f01en@googlegroups.com> <B6601963-34E5-412A-BAB2-3CBEEEC0B736@gmail.com> <8e33ff4b-097b-43a8-b58a-e35010782ae2n@googlegroups.com> <D6B92ECC-5325-4ADA-99BA-59CC601B9260@gmail.com> <3d3b91e7-4ad0-4bd3-93b2-20e9f800a6e4n@googlegroups.com>

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é

On Tuesday, October 20, 2020 at 3:26:21 PM UTC-3 mrynd...@xxxxxxxxx wrote:

Thanks Stephan and Markus!wtorek, 20 października 2020 o 18:57:00 UTC+2 Stephan Merz napisał(a):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,StephanOn 20 Oct 2020, at 14:09, Mariusz Ryndzionek <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.StephanOn 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 .. SnThe 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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8e33ff4b-097b-43a8-b58a-e35010782ae2n%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/75847d4b-4d20-4b19-86ca-f7653292137cn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] n-ary Cartesian product***From:*Stephan Merz

**References**:**[tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

**Re: [tlaplus] n-ary Cartesian product***From:*Stephan Merz

**Re: [tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

**Re: [tlaplus] n-ary Cartesian product***From:*Stephan Merz

**Re: [tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

- Prev by Date:
**Re: [tlaplus] n-ary Cartesian product** - Next by Date:
**[tlaplus] Integers Standard Module Location** - Previous by thread:
**Re: [tlaplus] n-ary Cartesian product** - Next by thread:
**Re: [tlaplus] n-ary Cartesian product** - Index(es):