Set, Set Builder Notation, and Set Comprehension

2025-11-19 | 4 min reading

Playing with TLA+, I stumbled across what is called Set Comprehension and my brain didn’t like it too much at first.

These are the notes I took to digest the subject.

Sets, Sequences and Tuples

Before diving in, let’s explore some math concepts of set, sequences and tuples.

A set is a collection of distinct objects where the order does not matter. Sets do not allow duplication and are denoted with curly braces, {a, b, c}.

A tuple is a finite collection of objects in which the ordering of the objects does matter, allows duplication and it is denoted with parentheses such as (a, b, b, c).

Also, if you have P := (a, b, b, c) then

P(0) = a
P(1) = b
P(2) = b
P(3) = c

A sequence is like a tuple but all the elements of the collection must be of the same type and also a sequence can be infinite.

In a language like JavaScript, a math set is represented by the Set object, while a tuple is represented by an Array.

Note, you may even use an array to represent a set, but JavaScript won’t enforce a constraint.

In TLA+ instead, you have Sets with the curly bracket syntax {a, b, c} similar to math and Sequences with the angle bracket syntax <<a, b, c>> that can be used to represent tuples and sequences.

Specifying a Set

How do you write a set?

Two possible ways of writing:

Roster notation, that is, you enumerate the elements in the set
eg: PC := { blue, red, yellow }
Set-builder notation, a logical formula in the shape of
{ espression | condition } or { espression : condition }

Set-Builder Notation Types

For the Set-builder notation, you may have two cases:

built by property filtering, in which the condition is used to filter a set by a property and
built by function, this is what is called Set Comprehension.

1. Build by property filtering

In this case, in the expression we have only a variable definition x or x ∈ Z while in the condition we have a property of the variable that impose a filter to the original set.

// with natural numbers
{ n : n ∈ N, n < 5} = { 0, 1 , 2, 3, 4 }


// with a finite set
S := {-1 , 0 , 1 , 2}

{ x | x ∈ S ⋀ x > 0 } = { 0, 1, 2 }

In JavaScript is quite self-evident why it is called a property filter; in fact, you would have:

// we used array because of filter
const S = [ -1, 0, 1, 2 ];

function buildSet(set) {
    return set.filter(x => x > 0);
}

{ espression | condition }
{   x        |  x ∈ S ⋀ x > 0 } 
    ^             ^       ^  
    |             |       |
    |             |       the property filter
    |             |
    |             arguments of the function `buildSet(set)`
    |
    the value returned by the function
    in this case x 


// While in TLA+ you would have 

S == { -1 , 0 , 1 , 2 }
{ x : x \in S /\ x > 0}

2. Build by function - Set Comprehension

In this case, within the expression or the condition, we may have a transformation function.

// with a finite set
S := { -1, 0, 1, 2 }

{ 2x | x ∈ S ⋀ x > 0 } = { 0, 2, 4 }
   ^
   |

   f(x) = 2x this is the transformation function


// in js we have
const S = [ -1, 0 , 1 , 2 ];

function buildSet(set) {
    return set.filter(x => x > 0)
              .map(x => 2 * x);
}

// And in TLA+
S == { -1 , 0 , 1 , 2 }
{ x * x : x \in S /\ x > 0}