Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable

Would { [x -> d] : x \in {1..n} } also be a set of functions whose domain is a set from 1..n and whose range is a subset of d? I was not concerned about double comprehension, I was just trying to understand the difference between Dominik's version and { [x -> d] : x \in {1..n} } and it seemed that the only difference is Dominik's version takes into account <<>> while { [x -> d] : x \in {1..n} } does not. I could be wrong again since I'm still really new to TLA.

Yuri

On Tuesday, April 30, 2013 4:55:56 AM UTC-7, Stephan Merz wrote:

Hi Yuri,

I am not sure I understand your suggestion. { [x -> d] : x \in {1..y : y \in 0..n} } is the set of functions whose domain is a set of the form 1..y, for some y \in 0 .. n, and whose range is a subset of d. Any function of that shape is a sequence over d whose length is at most n, and the union of all these function sets gives you the set of sequences over d whose length is at most n. In contrast, { [x -> d] : x \in 1..n } is a set of functions whose domain is some x \in 1 ..n (so x is a natural number, assuming n \in Nat). Although it is a well-formed TLA _expression_, it is not clear what such a value is.

If you are concerned about the double set comprehension in Dominik's suggestion, you can easily get rid of it. In fact, I just typed the following into TLAPS, the TLA+ Proof System, and it is proved immediately.

LEMMA
ASSUME NEW n \in Nat, NEW Data
PROVE UNION{[x -> Data]: x \in {1..y : y \in 0..n}} = UNION {[(1..y) -> Data] : y \in 0..n}
OBVIOUS

Best regards,

Stephan

On Apr 30, 2013, at 3:31 AM, Y2i <yur...@xxxxxxxxx> wrote:

Dear Dominik,

I realized that a record or a tuple is a shortcut for a function but did not think that a function with domain 1..n can be treated as a sequence. This is a very cleaver technique, thank you for sharing it!

And what about using { [x -> d] : x \in {1..y : y \in 0..n} } instead of { [x -> d] : x \in 1..n }? Was it in order to take into account sequences of length 0?

Thank you again,
Yuri

On Monday, April 29, 2013 1:54:50 AM UTC-7, Dominik Hansen wrote:
Dear Yuri,

in TLA+ a sequence of length n is a function with the Domain 1..n .Hence [1..n -> Data] defines the set of all sequences of length n.
The UNION-operator is used to collect all sequences of different length (from 0 to n) in a set.

Dominik

--
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...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.