Recursive operators and functions
We are going to remove support for recursive operators and functions soon. See Folding sets and sequences.
WARNING: In our experience, it is hard to check recursive operators and functions in Apalache:
 Recursive operators need additional annotations.
 Resursive operators and functions usually apply
CHOOSE
, which is hard to implement faithfully without blowing up the SMT encoding.
Hence, we recommend using the operators FoldSet
and FoldSeq
:
(*****************************************************************************)
(* The folding operator, used to implement computation over a set. *)
(* Apalache implements a more efficient encoding than the one below. *)
(* (from the community modules). *)
(*****************************************************************************)
RECURSIVE FoldSet(_,_,_)
FoldSet( Op(_,_), v, S ) == IF S = {}
THEN v
ELSE LET w == CHOOSE x \in S: TRUE
IN LET T == S \ {w}
IN FoldSet( Op, Op(v,w), T )
(*****************************************************************************)
(* The folding operator, used to implement computation over a sequence. *)
(* Apalache implements a more efficient encoding than the one below. *)
(* (from the community modules). *)
(*****************************************************************************)
RECURSIVE FoldSeq(_,_,_)
FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
THEN v
ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
These operators are treated by Apalache in a more efficient manner than recursive operators. They are always terminating and thus do not require an annotation that specifies an upper bound on the number of operator iterations. We are preparing a tutorial on this topic.
See Folding sets and sequences.
Recursive operators
In the preprocessing phase, Apalache replaces every application of a user operator with its body. We call this process "operator inlining". This cannot be done for recursive operators, for two reasons:

A recursive operator may be nonterminating (although a nonterminating operator is useless in TLA+);

A terminating call to an operator may take an unpredicted number of iterations.
However, in practice, when one fixes specification parameters (that is,
CONSTANTS
), it is usually easy to find a bound on the number of operator
iterations. For instance, consider the following specification:
 MODULE Rec6 
EXTENDS Integers
N == 5
VARIABLES
\* @type: Set(Int);
set,
\* @type: Int;
count
RECURSIVE Sum(_)
Sum(S) ==
IF S = {}
THEN 0
ELSE LET x == CHOOSE y \in S: TRUE IN
x + Sum(S \ {x})
UNROLL_DEFAULT_Sum == 0
UNROLL_TIMES_Sum == N
Init ==
/\ set = {}
/\ count = 0
Next ==
\E x \in (1..N) \ set:
/\ count' = count + x
/\ set' = set \union {x}
Inv == count = Sum(set)
=======================================
It is clear that the expression Sum(S)
requires the number of iterations that
is equal to Cardinality(S) + 1
. Moreover, the expression set \subseteq 1..N
is an invariant, and thus every call Sum(set)
requires up to N+1
iterations.
When we can find an upper bound on the number of iterations, Apalache can unroll the recursive operator up to this bound. To this end, we define two additional operators. For instance:
 MODULE Rec6 
EXTENDS Integers
N == 5
VARIABLES
\* @type: Set(Int);
set,
\* @type: Int;
count
RECURSIVE Sum(_)
Sum(S) ==
IF S = {}
THEN 0
ELSE LET x == CHOOSE y \in S: TRUE IN
x + Sum(S \ {x})
UNROLL_DEFAULT_Sum == 0
UNROLL_TIMES_Sum == N
Init ==
/\ set = {}
/\ count = 0
Next ==
\E x \in (1..N) \ set:
/\ count' = count + x
/\ set' = set \union {x}
Inv == count = Sum(set)
=======================================
In this case, Apalache unrolls every call to Sum
exactly UNROLL_TIMES_Sum
times, that is, four times. On the default branch, Apalache places
UNROLL_DEFAULT_Sum
, that is, 0.
All recursively defined operators should follow this convention where, for every such operator Oper
, the user defines both UNROLL_TIMES_Oper
, which expands to a positive integer value, and UNROLL_DEFAULT_Oper
, which expands to some default value Oper(args*)
should take, if the computation would require more than UNROLL_TIMES_Oper
recursive calls.
At present, we only support literals (e.g. 4
) or primitive arithmetic expressions (e.g. 2 + 2
) in the body of UNROLL_TIMES_Oper
.
Recursive functions
Apalache offers limited support for recursive functions. However, read the warning below on why you should not use recursive functions. The restrictions are as follows:

Apalache supports recursive functions that return an integer or a Boolean.

As Apalache's simple type checker is not able to find the type of a recursive function, all uses of a recursive function should come with a type annotation.

As in TLC, the function domain must be a finite set.
The example below shows a recursive function that computes the factorial of n
.
 MODULE Rec8 
EXTENDS Integers
VARIABLES
\* @type: Int;
n,
\* @type: Int;
factSpec,
\* @type: Int;
factComp
(*
Defining a recursive function on a finite domain. Although it is rather
unnatural to define factorial on a finite set, both Apalache and TLC
require finite domains. As is usual for function application, the result
of the application is not defined on the elements outside of the function
domain.
*)
Fact[k \in 1..20] ==
IF k <= 1
THEN 1
ELSE k * Fact[k  1]
Init ==
/\ n = 1
/\ factSpec = Fact[n]
/\ factComp = 1
Next ==
/\ n' = n + 1
/\ factSpec' = Fact[n']
/\ factComp' = n' * factComp
Inv ==
factComp = factSpec
===============================================================================
Check other examples in
test/tla
that
start with the prefix Rec
.
Why you should avoid recursive functions. Sometimes, recursive functions concisely describe the function that you need. The nice examples are the factorial function (see above) and Fibonacci numbers (see Rec3). However, when you define a recursive function over sets, the complexity gets ugly really fast.
Consider the example Rec9, which computes set cardinality. Here is a fragment of the spec:
The set cardinality function. It needs an upper bound on the set size.
Although this function looks nice, be warned that this definition requires us
to construct the powerset SUBSET NUMS and then write down the constraints
for the function Card. This encoding is (at least) doubleexponential.
*)
Card[S \in SUBSET NUMS] ==
IF S = {}
THEN 0
ELSE LET i == CHOOSE j \in S: TRUE IN
1 + Card[S \ {i}]
Init ==
/\ set = {}
/\ size = 0
Since we cannot fix the order, in which the set elements are evaluated, we
define function Card
over SUBSET NUMS
, that is, all possible subsets of
NUMS
. Apalache translates the function in a quantifierfree theory of SMT.
Hence, in this case, Apalache expands SUBSET NUMS
, so it introduces
2^NUMS
sets! Further, Apalache writes down the SMT constraints for the
domain of Card
. As a result, it produces NUMS * 2^NUMS
constraints.
As you can see, recursive functions over sets explode quite fast.
It is usually a good idea to use recursive operators over sets rather than
recursive functions. The downside is that you have to provide an upper bound on
the number of the operator iterations. The upside is that recursive operators
are usually unrolled more efficiently. (If they contain only constant
expressions, they are even computed by the translator!) For instance, set
cardinality does not require 2^NUMS
constraints, when using a recursive
operator.