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

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Wed, 21 Oct 2020 10:35:32 -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> <75847d4b-4d20-4b19-86ca-f7653292137cn@googlegroups.com> <C19D59F6-A17E-4DF9-AFC6-146D390148FD@gmail.com>

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!):

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.

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é

On Wednesday, October 21, 2020 at 12:33:53 PM UTC-3 Stephan Merz wrote:

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 }On 21 Oct 2020, at 02:42, JosEdu Solsona <josedu...@xxxxxxxxx> wrote: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é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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/75847d4b-4d20-4b19-86ca-f7653292137cn%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/1f3ad3fc-99f7-436d-9e11-9496ba42e6fcn%40googlegroups.com.

**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

**Re: [tlaplus] n-ary Cartesian product***From:*JosEdu Solsona

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

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