6.1 集合

集合有两个更高级的运算符：

交集UNION { {1, 2}, {2, 3} } = {1, 2, 3}

求子集（幂集）SUBSET {1, 2} = { {}, {1}, {2}, {1, 2} }

描述某种类型且元素满足某种公式的集合有两种方法，以奇数为例：{x \in Nat : x % 2 = 1}和{2 * n + 1 : n \in Nat}。

FiniteSets模块定义了两种新的运算符：

Cardinality(S)在S是有限集时返回元素的个数。

IsFiniteSet(S)判断S是有限集。

在 TLA+ 的集合定义下，如何避免罗素悖论？TLA+ 的方式是限制自身的表达能力，不能表达其元素与“所有集合”一一对应的集合。

6.2 无意义的表达式

TLA+ 没有类型系统，因此不能检查3 / "abc"等无意义的表达式。可以认为这些表达式具有一个由表达式唯一复现的、不确定的返回值。

6.3 重温递归

TLA+ 要求递归函数有特殊的定义方法。下面的直观的递归定义阶乘函数是错误的：

fact == [n \in Nat |-> IF n = 0 THEN 1 ELSE n * fact[n - 1]]

原因是在解析右侧的表达式时，fact标识符还没有定义。

第五章中说明递归定义的语法是f[x \in S] == e，这实际上是f == CHOOSE f: f = [x \in S |-> e]。TLA+ 通过对CHOOSE关键字的语法解析完成递归函数定义。同样，如果不存在合法的CHOOSE，例如无意义的表达式或者表达式与要定义的函数有逻辑冲突，递归函数将会定义为某个不确定的值。

有些递归函数表达为同时依赖多个函数，例如 f、g 的计算同时依赖 f、g。这可以通过定义一个记录并通过record.f和record.g访问解决。

虽然 TLA+ 支持递归定义，但是应当注意运用已提供的运算符，这样效率更高。例如不要使用递归重复定义Head(s)。

6.4 函数与运算符

函数和运算符有如下区别：

函数是一个语法完整的公式，运算符不是。具体而言，function \in S、function[x] \in S、operator(x) \in S都是合法的，但operator \in S有语法错误。
函数有定义域，但运算符没有。有的运算符（例如Tail(s)）的定义域太大而不能在 TLA+ 下表达，参见 6.1 节。
运算符不能被递归定义。但在 TLA+ 中，可以通过能递归定义的函数辅助定义运算符。例如Cardinality运算符可以定义为：
```
Cardinality(S) ==
  LET CS[T \in SUBSET S] ==
      IF T = {} THEN 0
                ELSE 1 + CS[T \ {CHOOSE x: x \in T}]
  IN CS[S]
```
运算符可以将另一个运算符作为参数。
中缀关系只能由运算符定义。
错误的运算符写法会产生语法错误，但错误的函数写法不能被检查语法错误，一般只能产生语义错误。这与 TLC 等运行环境实现有关。

6.5 使用函数

按照前文定义的方式正确定义函数，奇怪的定义方法往往有潜在问题。

6.6 `CHOOSE` 运算符

CHOOSE 运算符在无法“选出”一个符合要求的元素时会返回不确定的值，但相同的CHOOSE公式是可复现的。