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

*From*: Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx>*Date*: Mon, 7 Dec 2020 23:29:10 -0800 (PST)*References*: <cac57bb6-3d36-433e-a1f9-b3747211fe56n@googlegroups.com> <DCC08488-5FEC-4E15-A19C-C1749E2B3F53@gmail.com> <55e16139-6401-44d1-9b21-e4c1e3d694e2n@googlegroups.com> <AAF60449-8329-4E99-B186-9053CF1908B0@TimLeonard.us>

It took me some time to see that [(SUBSET A) -> B] is not the same as UNION {[X -> B] : X \in SUBSET A}, so I thought I'd write them out here for clarity in case someone else stumbles on it. Apologies for the verbosity -- though it seems obvious now, I didn't start out that way and had to work through it.

Consider A = 1..2 and B = {"a", "b"}

Then [(SUBSET A) -> B] is the set of all mappings that assign an element of B to each element of SUBSET(A). For the given A, there are 4 subsets - {}, {1}, {2}, {1,2}. So the cardinality of this set is Cardinality(B) ^ Cardinality(SUBSET A) = 2^4 = 16 .. where each of these subsets of A can be assigned either "a" or "b". Now for the obvious thing - all the functions in this set have the same domain.

{[X -> B] : X \in SUBSET A} is the set of sets of functions whose domain is from SUBSET(A) and whose range is B. So this is -

{ [{} -> B], [{1} -> B], [{2} -> B], [{1,2} -> B] }

The first is {<< >>} (the singleton set with the empty tuple)

The second is {<<"a">>,<<"b">>}

The third is {(2 :> "a"), (2 :> "b")}

The fourth is {<<"a","a">>,<<"a","b">>,<<"b","a">>,<<"b","b">>}

The main thing to notice here is that the domains of the functions are all not the same.

Let S1 = [SUBSET(A) -> B] and S2 = UNION {[X -> B] : X \in SUBSET A},

So the cardinality of S2 is 9 .. whereas for S1 is 16.

{**DOMAIN** X : X \in S1} = {{{}, {1}, {2}, {1, 2}}} (cardinality 1, since all the functions in S1 have the same domain of cardinality 2^Cardinality(A) = 4)

{**DOMAIN** X : X \in S2} = {{}, {1}, {2}, {1, 2}} (cardinality 4, since the functions can have one of 4 possible domains, each of which is a subset of A)

Hope this helps somebody like me.

On Tuesday, December 8, 2020 at 11:02:49 AM UTC+5:30 t...@xxxxxxxxxxxxxx wrote:

Yes. The second is what I’m now using.Thank you for the help.On Dec 8, 2020, at 12:19 AM, Srikumar Subramanian <srikumar.s...@xxxxxxxxxxxx> wrote:I guess you meant this? -edges_stack \in Seq(

UNION{[X -> Nodes] : X \inSUBSETLabels})or perhaps -

edges_stack \in Seq(

?UNION{[X -> Nodes] : X \in {1..n : n \in Labels}})

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/cd36eaeb-0e53-40cf-a5c5-0fd5895d3793n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Stephan Merz

**References**:**[tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Stephan Merz

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Srikumar Subramanian

**Re: [tlaplus] Initial state doesn't satisfy type invariant***From:*Tim Leonard

- Prev by Date:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by Date:
**Re: [tlaplus] A temporal formula to specify that the value of a record does not change** - Previous by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by thread:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Index(es):