specifications - 冒号符号可以与 Z 规范语言中的集合成员符号互换吗？

Question

在 Z 规范语言中，冒号符号“：”仅仅是集合成员符号“∈”的变体吗？它们总是可以互换使用吗？特别是，以下表达式在 Z 中是否合法？

标签： specificationsformal-languages

Answer 1

恕我直言，不。

尽管每个集合都可以用作类型 [来源：第 11 页]，但声明 x类型变量的语法T是明确定义的，并且明确地仅使用冒号符号:[来源：第 15 页]。

Type的概念和membership-of的概念之间的细微区别在于，一个变量x只能属于一个给定的Type，但它可能属于（可能无限）许多Sets。

由于这种类型的写作属于滥用符号，因此您可能需要在您的研究论文/文档中包含免责声明，以阐明您正在使用的符号，以及这样做的好处是什么（我看不到）。在这方面，我会邀请您查看研究文献和同行，并尝试遵守周围环境使用的惯例。

---

这个

{ x ∈ Z | x < 100 }

不尊重集合推导的语法：

{ x : T | pred(x) ● expr(x) }

expr(x)对所有x类型T进行评估而产生的所有元素的集合 pred(x) 。

当expr(x)等于 时x，即当我们返回元素本身时，我们可以省略expr(x)并写成

{ x : T | pred(x) }

[来源：第 7,8 页]

---

这个

λx ∈ Z • x + 1

不尊重lambda 函数的语法[来源：第 24 页]：

 λa : S | p • e