Toplevel operator definitions
Quick example
Here is a quick example of a toplevel user operator (which has to be defined in a module) and of its application:
 MODULE QuickTopOperator 
...
Abs(i) == IF i >= 0 THEN i ELSE i
...
B(k) == Abs(k)
===============================================================================
As you most probably guessed, the operator Abs
expects one argument i
.
Given an integer j
, then the result of computing Abs(j)
is the absolute
value of j
. The same applies, when j
is a natural number or a real number.
Syntax of operator definitions
In general, operators of n
arguments are
defined as follows:
\* an operator without arguments (nullary)
Opa0 == body_0
\* an operator of one argument (unary)
Opa1(param1) == body_1
\* an operator of two arguments (binary)
Opa2(param1, param2) == body_2
...
In this form, the operator arguments are not allowed to be operators. If you want to receive an operator as an argument, see the syntax of Higherorder operators.
Here are concrete examples of operator definitions:
 MODULE FandC 
EXTENDS Integers
...
ABSOLUTE_ZERO_IN_CELCIUS ==
273
Fahrenheit2Celcius(t) ==
(t  32) * 10 / 18
Max(s, t) ==
IF s >= t THEN s ELSE t
...
===============================================================================
What is their arity (number of arguments)?
If you are used to imperative languages such as Python or Java, then you are
probably surprised that operator definitions do not have any return
statement. The reason for that is simple: TLA+ is not executed on any hardware.
To understand how operators are evaluated, see the semantics below.
Syntax of operator applications
Having defined an operator, you can apply it inside another operator as follows (in a module):
 MODULE FandC 
EXTENDS Integers
VARIABLE fahrenheit, celcius
\* skipping the definitions of
\* ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius, and Max
...
UpdateCelcius(t) ==
celcius' = Max(ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius(t))
Next ==
/\ fahrenheit' \in 1000..1000
/\ UpdateCelcius(fahrenheit')
...
===============================================================================
In the above example, you see examples of four operator applications:

The nullary operator
ABSOLUTE_ZERO_IN_CELCIUS
is applied without any arguments, just by its name. Note how a nullary operator does not require parentheses()
. Yet another quirk of TLA+. 
The oneargument operator Fahrenheit2Celcius is applied to
t
, which is a parameter of the operatorUpdateCelcius
. 
The twoargument operator
Max
is applied toABSOLUTE_ZERO_IN_CELCIUS
andFahrenheit2Celcius(t)
. 
The oneargument operator
UpdateCelcius
is applied tofahrenheit'
, which is the value of state variablefahrenheit
in the next state of the state machine. TLA+ has no problem applying the operator tofahrenheit'
or tofahrenheit
.
Technically, there are more than four operator applications in our example. However, all other operators are the standard operators. We do not focus on them here.
Note on the operator order. As you can see, we are applying operators after they have been defined in a module. This is a general rule in TLA+: A name can be only referred to, if it has been defined in the code before. TLA+ is not the first language to impose that rule. For instance, Pascal had it too.
Note on shadowing. TLA+ does not allow you to use the same name as an operator parameter, if it has been defined in the context of the operator definition. For instance, the following is not allowed:
 MODULE NoShadowing 
VARIABLE x
\* the following operator definition produces a semantic error:
\* the parameter x is shadowing the state variable x
IsZero(x) == x = 0
===============================================================================
There are a few tricky cases, where shadowing can actually happen, e.g., see
the operator dir
in SlidingPuzzles. However, we recommend to keep things
simple and avoid shadowing at all.
Semantics of operator application
Precise treatment of operator application is given on page 320 of Specifying Systems. In a nutshell, operator application in TLA+ is a Call by macro expansion, though it is a bit smarter: It does not blindly mix names from the operator's body and its application context. For example, the following semantics by substitution is implemented in the Apalache model checker.
Here we give a simple explanation for nonrecursive operators. Consider the
definition of an n
ary operator A
and its application in the definition
of another operator B
:
A(p_1, ..., p_n) == body_of_A
...
B(p_1, ..., p_k) ==
...
A(e_1, ..., e_n)
...
The following three steps allow us to replace application of the operator A
in B
:
 Change the names in the definition of
A
in such a way such they do not clash with the names inB
(as well as with other names that may be used inB
). This is the wellknown technique of Alpha conversion in programming languages. This may also require renaming of the parametersp_1, ..., p_n
. Let the result of alpha conversion be the following operator:
uniq_A(uniq_p_1, ..., uniq_p_n) == body_of_uniq_A

Substitute the expression
A(e_1, ..., e_n)
in the definition ofB
withbody_of_uniq_A
. 
Substitute the names
uniq_p_1, ..., uniq_p_n
with the expressionse_1, ..., e_n
, respectively.
The above transformation is usually called Beta reduction.
Example. Let's go back to the module FandC
, which we considered above. By
applying the substitution approach several times, we transform Next
in
several steps as follows:
First, by substituting the body of UpdateCelsius
:
Next ==
/\ fahrenheit' \in 1000..1000
/\ celcius' = Max(ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius(fahrenheit'))
Second, by substituting the body of Max
:
Next ==
/\ fahrenheit' \in 1000..1000
/\ celcius' =
IF ABSOLUTE_ZERO_IN_CELCIUS >= Fahrenheit2Celcius(fahrenheit')
THEN ABSOLUTE_ZERO_IN_CELCIUS
ELSE Fahrenheit2Celcius(fahrenheit')
Third, by substituting the body of Fahrenheit2Celcius
(twice):
Next ==
/\ fahrenheit' \in 1000..1000
/\ celcius' =
IF ABSOLUTE_ZERO_IN_CELCIUS >= (fahrenheit'  32) * 10 / 18
THEN ABSOLUTE_ZERO_IN_CELCIUS
ELSE (fahrenheit'  32) * 10 / 18
You could notice that we applied beta reduction syntactically from top to
bottom, like peeling an onion. We could do it in another direction: First
starting with the application of Fahrenheit2Celcius
. This actually does not
matter, as long as our goal is to produce a TLA+ expression that is free of
userdefined operators. For instance, Apalache applies Alpha conversion and
Beta reduction to remove userdefined operator and then translates the TLA+
expression to SMT.