hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
183 stars 39 forks source link

Structured data chapter improvements #63

Open acud opened 11 months ago

acud commented 11 months ago

Now what about an operator that sorts as a sequence? Specifically, one such that IsSorted(SortSeq(seq)) is always true. That’s easy:

Sort(seq) ==
<<>>

We had to tweak the definition a bit and make sure that the output sequence has all the same elements, too.

The phrasing of this sentence is not clear, and together with the example operator, it appears that the operator is one that simply returns an empty sequence for any given input. In that case, it does not seem to "sort" anything. It is also not clear what changes to the definition were made and since the output sequence is an empty sequence, the last sentence is even more confusing. I do understand that an empty sequence may satisfy any picked indices since the set is empty, therefore landing on the edge case that any two picked indices in an empty set will satisfy the condition; if that was the intention behind it, clarifying this somehow might be helpful. Nit: before the actual code snippet there's mentioning of SortSeq but the example has Sort. Aligning them might be useful too.


Then [DOMAIN seq -> Range(seq)] is the set of all sequences which have the same elements as seq. Our operator will then look something like this...

I've tried to wrap my head around it multiple times halfway successfully. Range(seq) here is the set of all unique elements in the given input seq. DOMAIN seq here should be {<<1,2,3>>} (since seq is a sequence and it's domain is the actual indices). Therefore how can "[DOMAIN seq -> Range(seq)]" do the actual value indirection + different permutations of the values? Maybe a word on "how to read" could help here


For the Summary section in this chapter, there's no reference to Function sets. It would be useful to have a succinct description which would help remember how they work and their intended use-case along with the syntax.