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

*From*: Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx>*Date*: Tue, 8 Dec 2020 01:22:36 -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> <cd36eaeb-0e53-40cf-a5c5-0fd5895d3793n@googlegroups.com> <BBF48CDE-9CEF-4A42-AB93-908EEEF0EC00@gmail.com>

I have a feeling (albeit uninformed) that such pure partial functions are likely to be too relaxed for many purposes. Even in this example, we're looking for 1..n where n \in A and not any subset of A. Maybe making it slightly more general would be useful since subset enumeration blows up quickly -

PartialFunctions(Domains, Codomain) == UNION {[X -> Codomain] : X \in Domains}

which would be used as PartialFunctions(SUBSET A, B) for the full set of partial functions .. or in this case PartialFunctions({1..n : n \in Labels}, Nodes) where the domains are way more limited. .. but then now PartialFunctions does more than just make sets of partial functions :)

.. and the _expression_ itself reads fairly clear to me now!

-Srikumar

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 asPartialFunctions(A,B) == UNION {[X ->B] : X \in SUBSET A}to the CommunityModules, representing functions from some subset of A to B?StephanP.S.: Apologies for the typo (missing function brackets) in my reply to the original question. -sOn 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.{DOMAINX : 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){DOMAINX : 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 \inSUBSETLabels})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.

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/6b4e0c58-1362-47e4-ac3b-a031afb66d8cn%40googlegroups.com.

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

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

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

- Prev by Date:
**Re: [tlaplus] Initial state doesn't satisfy type invariant** - Next by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - 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):