本节要点:
- 两个集合运算:
UNION S 和
SUBSET S
- 两种集合构造方式 :
{x∈S:p} 和
{e:x∈S}
- 标准模块
FiniteSets中两个运算符
Cardinality(S) 和
IsFiniteSet(S)
- 罗素悖论(个人觉得可以不看)
我们用来编写规约所需要的数学基础,是建立在一个小而简单的集合概念上的。 您可能已经了解了描述绝大多数数学形式所需的内容,现在需要掌握的只是在下面第6.1节中描述的少数几个集合运算符。 了解它们之后,您将能够定义规约中出现的所有数据结构和操作。
虽然我们用到的数学很简单,但是其基础并不是显而易见的,例如,递归函数定义和CHOOSE运算符的含义很微妙,本节将讨论其中一些基础,了解它们将帮助您更有效地使用TLA +。
6.1 Set(集合)
1.2节中描述的简单的集合操作,对编写大多数系统规范已经足够了, 但是,有时可能需要使用更复杂的运算符,尤其是如果您需要定义除元组,记录和简单函数之外的数据结构。
集合论的两个关键运算符是一元运算符 并集和子集,定义如下:
-
UNION S 集合S中所有元素的并集。换句话说,
e是集合
UNION S 的一个元素 当且仅当 它是
S的一个元素中的一个元素,例如:
UNION {{1,2},{2,3},{3,4}}={1,2,3,4}
-
SUBSET S
S所有子集的集合。换句话说,
T∈SUBSET S当且仅当
T⊆S。例如:
SUBSET {1,2}={{},{1},{2},{1,2}}
数学家们经常采用如下术语描述集合:“…是所有…的集合,使得…”。TLA+有两种结构可以将上述语言形式化:
-
{x∈S:p} 是
S的一个子集,其中的每个元素都满足属性
p。例如,所有奇自然数的集合可以写作:
{n∈Nat:n%2=1}。标识符
x出现在表达式
p中,不会出现在
S中。
-
{e:x∈S} 是由集合
S中每个元素,按照形式
e生成的元素的集合。例如,
{2∗n+1:n∈Nat} 就是所有奇自然数的集合,其中标识符
x出现在
e中,不会在
S中出现。
{e:x∈S}与
∃x∈S:F有相同的构造生成方式。例如
{e:x∈S,y∈T}是所有满足形式
e的集合,其中
x属于集合
S,
y属于集合
T。在集合
{x∈S:P}中,我们可以让
x为一个元组。例如,
{⟨y,z⟩∈S:P} 是
S中满足条件
P的所有元素对
⟨y,z⟩的集合。第15章的TLA+语法会更精确地描述集合表达式的写法。
到目前为止所有这些用到的集合运算符都是TLA+的内置运算符,另外,还有一个名为
FiniteSets的标准模块定义了如下两个集合操作符:
Cardinality(S) 集合
S中元素的个数(
S是一个有限集合)
IsFiniteSet(S)
S是有限集则为TRUE
FiniteSets模块在第341页。
Cardinality(S)定义在第70页。
关于集合的粗心推理可能会出问题, 经典的例子是罗素悖论:
令
R为所有满足
S∈/S的集合
S的集合, 则
R的定义可以推导如下:
R∈R为真当且仅当
R∈/R
两个结论明显相悖,这个悖论产生的原因是
R不是一个集合。如果一个“组合”
C是所有集合的合集,那么它因为太大而不成为一个集合——因为如果它是一个集合,我们可以将
C中的一个不同元素赋值给每一个集合,通俗来说,如果我们定义一个操作
SMap, 使得:
- 对所有集合
S,
SMap(S)是
C的一个元素;
- 如果
S和
T是不同集合,则
SMap(S)=SMap(T)
例如,所有长度为2的序列的组合不是一个集合,因为我们可以定义操作
SMap如下
SMap(S)≜⟨1,S⟩这个操作针对每一个集合
S生成了与之前所有序列都不同的长度为2的序列。