Re: [tlaplus] Initial state doesn't satisfy type invariant

On Tuesday, December 8, 2020 at 1:14:48 PM UTC+5:30 Stephan Merz wrote:

Perhaps it would make sense to add an operator such as

PartialFunctions(A,B) == UNION {[X ->B] : X \in SUBSET A}

to the CommunityModules, representing functions from some subset of A to B?

Stephan

P.S.: Apologies for the typo (missing function brackets) in my reply to the original question. -s

On 8 Dec 2020, at 08:29, Srikumar Subramanian <srikumar.s...@xxxxxxxxxxxx> wrote:

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...@ryanleonard.us 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 \in SUBSET Labels})
or perhaps -
edges_stack \in Seq(UNION {[X -> Nodes] : X \in {1..n : n \in Labels}})
?

This mail contains confidential information intended only for the individual(s) named. If you’re not the named addressee, don’t disseminate, distribute or copy this e-mail. Please notify the sender immediately and delete it from your system.If you wish not to receive such e-mails you may reply with text “Unsubscribe”.

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