本节列出了函数和运算符的几个区别:
- 最明显的区别是函数可以表示值而运算符不行;
- 函数以某个集合为定义域,而运算符没有;
- 在TLA+中,运算符不能递归定义,而函数可以(需要的话,可以使用LET…IN语句将运算符以函数的方式定义出来);
- 运算符可以以运算符为入参,而函数不行;
- TLA+不允许定义中缀函数,只能以运算符的形式定义如 +,-,*,/。
函数和运算符的区别可以决定你的选择策略,如果使用任一都可以的话,按照你习惯的方式来吧:)
考虑到我们之前遇到的两个定义:
Tail(s)≜[i∈1..(Len(s)−1)↦s[i+1]]
fact[n∈Nat]≜IF n=0 THEN 1 ELSE n∗fact[n−1]
上面定义了两种截然不同的对象:
fact是一个函数,
Tail是一个运算符。函数和运算符在几个基本方面有所不同。它们最明显的区别在于,像
fact这样的函数本身是一个表示值的完整表达式,而像
Tail这样的运算符则不是。表达式
fact[n]∈S和
fact∈S在语法上都是正确的,而
Tail(n)∈S在语法上正确,
Tail∈S则不然。就像
x+>0一样,没有任何意义。
不同于操作符,函数需要有一个定义域,它是一个集合。我们不能定义一个
Tail函数,使得
Tail[s]是所有非空序列的尾;因为这样一个函数的定义域必须包含所有的非空序列,所有这样的非空序列的“组合”因为太大而不能成为一个集合(在之前第6.1章讲集合的时候我们提到过,一个“组合”
C因为太大而不成为一个集合——如果我们可以将
C中的一个不同元素赋给每一个集合,这里,通过定义运算符
SMap(S)≜⟨S⟩, 可以为集合S赋予一个不同的非空序列
⟨S⟩),因此,我们不能将
Tail定义为一个函数。
与函数不同,操作符不能在TLA+中递归定义,不过,我们通常可以定义一个递归函数,将非法的递归运算符转换为非递归运算符定义。例如,我们尝试在有限集上定义
Cardinality运算符(回忆一下,有限集S的
Cardinality是
S中元素的个数),所有有限集的“组合”太大,不是一个集合(运算符
SMap(S)≜{S}为每一个集合赋予一个基数为1的集合)。
Cardinality运算符有一个简单直接的定义:
-
Cardinality({})=0.
- 如果
S是一个非空有限集,
x是
S一个随机元素,则
Cardinality(S)=1+Cardinality(S∖{x})
使用
CHOOSE运算符来指代
S的任一元素,我们可以将上式写得更正式一点,不过仍然是不合规则的:
Cardinality(S)≜IF S={} THEN 0 ELSE 1+Cardinality(S∖{ CHOOSE x:x∈S})
上式仍然不合规是因为里面包含递归——只有在递归函数才可以在表达式的右值中出现待定义的符号。
有鉴于此,为了将上式转换为一个合法的定义,对一个给定的有限集
S,我们定义一个函数
CS, 使得对
S的每个子集
T,
CS[T]等于
T的基数,新定义如下:
CS[T∈SUBSET S]≜IF T={} THEN 0 ELSE 1+CS[T∖{ CHOOSE x:x∈T}]
因为
S是自己的子集,因此如果
S是一个有限集的话,
CS[S]=Cardinality(S),(这里我们不关心如果
S非有限的话,
CS[T]的值是什么). 所以,我们现在可以定义
Cardinality运算符了:
Cardinality(S)≜LET CS[T∈SUBSET S]≜IF T={} THEN 0 ELSE 1+CS[T∖{ CHOOSE x:x∈T}IN CS[S]
还有一个不同的地方是一个运算符可以以运算符为入参,例如,我们定义操作符
IsPartialOrder使得
IsPartialOrder(R,S)等于TRUE当且仅当操作符R对S定义了一个偏序关系:
IsPartialOrder(R(_,_),S)≜∧∀x,y,z∈S:R(x,y)∧R(y,z)⇒R(x,z)∧∀x∈S:¬R(x,x)
我们也可以使用一个类似
≺这样的中缀运算符代替
R作为入参,记作:
IsPartialOrder(_≺_,S)≜∧∀x,y,z∈S:(x≺y)∧(y≺z)⇒(x≺z)∧∀x∈S:¬(x≺x)
IsPartialOrder的第一个入参是一个有两个参数的运算符,第二个入参是一个表达式,因为
>是一个有两个参数的运算符,表达式
IsPartialOrder(>,Nat)在语法上式正确的。事实上,如果
>是定义在自然数上那个通用的大于运算符,则其值为真。表达式
IsPartialOrder(+,Nat)同样在语法上没有问题,不过它是个笨表达式,我们不清楚它是否为真。
函数和运算符还有一点微小的不同,不是很重要,为完整性考虑我还是提一下。举个例子,有个任意值
s的操作符
Tail(s)定义如下:
(6.5)
[i∈1..(Len(1/2)−1)↦(1/2)[i+1]]
我们不知道这个表达式是什么意思,不清楚
(Len(1/2)或(1/2)[i+1]是个什么东西。但是,不管它的含义如何,它等于
Tail(1/2)。函数
fact定义的
fact[n]只对
n∈Nat有效,
fact[1/2]没有任何意义。不过它在语法形式上是没问题的,尽管它也表示某个值,只不过
fact的定义不能确定这是个啥值。
最后一点运算符和函数之间的区别与数学无关,只是TLA+ 的特质:它不允许我们定义中缀函数。 数学家通常将 “/” 定义为两个参数的函数,但是我们在TLA+ 中无法做到这一点。 如果要定义 “/”,别无选择只能将其设为运算符。
可以使用函数或运算符来写同样不知所谓的表达式。 但是,无论您使用的是函数还是运算符,都可以确定所写的废话是非句法的胡言乱语,还是语法上正确但在语义上愚蠢的表达式。字符串2(“a”)在语法上不是正确的公式,因为2不是运算符。 但是,2 ["a“]也可以写为2.a,这在语法上是正确的。不过因为2不是一个函数,这么写也没什么意义。
我们不知道2[“a”]是什么意思。同样,
Tail(s,t)在语法上也是错误的,因为
Tail是一个入参的运算符。但是,如第301页的16.1.7节所述,
fact[m,n]是
fact[⟨m,n⟩]事实的句法糖,因此它也是一个语法正确,语义上愚蠢的公式。错误是语法错误还是语义错误决定了哪种工具可以捕获它。特别是,第12章中描述的解析器捕获语法错误,但不捕获语义上的愚蠢。如第14章所述,TLC模型检查器在评估语义上愚蠢的表达式时会报告错误。
函数和运算符之间的区别似乎使某些人感到困惑。一个原因是,尽管这种区别存在于普通数学中,但数学家通常不会注意到。如果您问数学家,
SUBSET是否是一个函数,她可能会说是。但是,如果您指出她,因为
SUBSET的域不能是集合,那么
SUBSET就不能成为函数,她可能会第一次意识到数学家会使用像
SUBSET和
∈这样的运算符,而不会注意到它们构成了一类与函数不同的对象。逻辑学家将注意到,由于TLA+是一阶逻辑而不是高阶逻辑,因此出现了运算符与值(包括函数)之间的区别。
在定义对象
V时,您可能必须决定是使
V成为接受入参的运算符还是成为一个函数,运算符和函数之间的差异通常会决定决策。例如,如果变量的值可能为
V,则
V必须是一个函数。因此,在第5.3节的内存规约中,我们必须用函数而不是运算符来表示内存的状态,因为变量mem不能等于运算符。如果这些差异不能确定是使用运算符还是使用函数,那么如何选择就取决于你的习惯。我通常更喜欢运算符。