Relations and functions: a set of pairs, but you won't write it that way
A relation between two sets is just any set of (input, output) pairs —
nothing more. A function is the special case where no input repeats:
every input is paired with exactly one output. So every function is a
relation, but not every relation is a function ({(1, "a"), (1, "b")} is a
relation — 1 has two outputs — but not a function). TLA+ lets you
construct a function directly, without ever writing the pairs out, using
the same bound-variable shape you just learned for quantifiers:
Squares == [n \in 1..5 |-> n * n]
Read this as: "the function that maps each n in 1..5 to n * n." The set
1..5 is called the function's domain — the inputs it's defined for.
Domain and application: DOMAIN, f[x]
DOMAIN f gives you back the domain of f — the set of valid inputs.
Applying f to an input uses square brackets, f[x], not the f(x) you
might expect from other languages:
DOMAIN Squares = 1..5 \* true
Squares[4] = 16 \* true
The set of all functions: [S -> T]
[S -> T] is the set of every function with domain S and outputs in
T — this is the function analog of the sets you already know how to build.
T here is called the function's codomain: the set its outputs are
drawn from, which isn't quite the same thing as the set of outputs it
actually produces (that narrower set is the function's range or image —
a distinction that won't matter much in this boot camp, but is worth
knowing the words for). Squares \in [1..5 -> Nat] asks "is Squares one
of the functions from 1..5 into the naturals?"
Records
A record is a function whose domain is a fixed set of field names
(strings), written with |-> just like any other function:
Alice == [name |-> "Alice", age |-> 30]
Field access uses dot notation, Alice.age, which is really just shorthand
for Alice["age"] — DOMAIN Alice is the set {"name", "age"}.
The set of all records with a given shape is written [field: Set, ...]:
Alice \in [name: STRING, age: Nat] \* true
(STRING is TLA+'s built-in set of all strings.)
Updating a function: EXCEPT
You'll almost never build a whole new function by hand just to change one
entry. [f EXCEPT ![x] = v] gives you a new function identical to f
everywhere except at x, where it's now v:
[Squares EXCEPT ![1] = 100] \* same as Squares, but maps 1 to 100 instead of 1
This matters more than it looks like it should — it's how you'll write almost every state update once you get to actions in Part 1.
Tuples
A tuple <<a, b, c>> is a function whose domain is 1..3 — so t[1] gets
the first element, exactly like function application, because that's
literally what it is:
Pair == <<7, 8>>
Pair[1] + Pair[2] = 15 \* true
What you'll do in this exercise
Same shape as the last two chapters: fill in ASSUME statements, run TLC,
fix whatever it points at. Still no state machine — but EXCEPT here is a
preview of the single most common thing you'll write once one exists.