集合论
集合是一个无顺序的结构，包含 $0$ 个或多个对象。
| 常用的集合 | 描述 |
|---|---|
| $\textbf{N}$ | 自然数集：$\textbf{N} = \{ 0, 1, 2, \cdots \}$ |
| $\textbf{Z}$ | 整数集：$\textbf{Z} = \{\cdots, -2, -1, 0, 1, 2, \cdots\}$ |
| $\textbf{R}$ | 实数集 |
| $\oslash$ | 空集：$\oslash = \{\} = \{x \mid \textbf{False}\}$ 也可表示为： $\lnot\ \exist\ x : x \in \oslash$ |
集合间的运算
- $S \subset T$：集合 $S$ 是 $T$ 的真子 $S \subseteq T$ 但是 $T \nsubseteq S$
- $|S|$：集合 $S$ 中元素的个数
- $A \cup B$：集合 $A$ 与 $B$ 的并集 $A \cup B = \{x \mid x \in A \lor x \in B\}$
- $A \cap B$：集合 $A$ 与 $B$ 的交集：$A \cap B = \{x \mid x \in A \land x \in B\}$
- $A - B$：集合 $A$ 与 $B$ 的差，在集合 $A$ 但不在集合 $B$ 中的元素： $$A - B = \{x \mid x \in A \land x \notin B\} = \{x \mid \lnot(x \in A \to x \in B)\}$$
- $\overline{A}$：集合 $A$ 相对于全集 $U$ 的补集
- $A \oplus B$：集合 $A$ 与 $B$ 的对称差：在集合 $A$ 和 $B$ 但不在其交集的元素
备注集合内的元素也可以是集合，例如 $S = \{ x | x \subseteq \{1, 2, 3\} \} = \{\oslash, \{1\}, \{2\}, \{3\}, \{1,2\}, \{1,3\}, \{2,3\}, \{1,2,3\}\}$
注意：$1 \ne \{1\} \ne \{\{1\}\}$
特别地，若 $A \cap B = \oslash$，则称集合 $A$ 和 $B$ 不连接（disjoint）。
幂集
集合 $S$ 的所有子集称作集合 $S$ 的幂集，记作 $P(S) = \{x \mid x \subseteq S\}$。
例如，$P(\{a,b\}) = \{\oslash, \{a\}, \{b\}, \{a,b\}\}$
我们有以下结论：$\mid P(S) \mid = 2^{\mid S \mid}$
笛卡尔积
定义 $A \times B :\equiv \{(a,b) \mid a \in A \land b \in B\}$ 为集合 $A$ 与 $B$ 的笛卡尔积。
例如，$\{a,b\} \times \{1,2\} = \{(a,1), (a,2), (b,1), (b,2)\}$
具有以下结论：
- $|A \times B| = |A| \cdot |B|$。
- $\lnot \forall AB: A \times B = B \times A$，即笛卡尔积不具备交换律。
集合间的关系
集合 $A$ 与 $B$ 之间的关系 $R$ 是 $A \times B$ 的一个子集，记作：$R: A \leftrightarrow B$
通常，我们用 $aRb$ 表示 $(a,b) \in R$，即元素 $a$ 与 $b$ 具备关系 $R$。
| 常见的关系 | 表示 |
|---|---|
| 空关系 | $\oslash$ |
| 恒等关系 | $\mathrm{i}d_A :\equiv \{(a,a) \mid (a \in A)\}$ |
| 逆关系 | $R^{-1} :\equiv \{(b,a) \mid (a,b) \in R\}$ |
关系的性质
| 性质 | 定义 |
|---|---|
| 自反性 | 对于 $A$ 上的关系 $R$，$\forall a \in A$，都有 $aRa$ |
| 对称性 | 当且仅当关系 $R$ 满足 $R = R^{-1}$，即 $(a,b) \in R \leftrightarrow (b,a) \in R$ |
| 反对称性 | 当且仅当关系 $R$ 满足 $(\forall a)(\forall b) ((a \in A \land b \in A) \Rightarrow ((a,b) \in R \land (b,a) \in R) \Rightarrow a = b)$，即仅有 $aRa$ |
| 传递性 | 当且仅当关系 $R$ 满足 $\forall a,b,c$，都有 $(a,b) \in R \land (b,c) \in R \rightarrow (a,c) \in R$ |
当集合上的关系同时满足一些性质时，则称该关系为一种特殊的关系。
| 特殊关系 | 定义 |
|---|---|
| 等价关系 | 同时满足自反性、对称性和传递性 |
| 偏序关系 | 同时满足自反性、反对称性和传递性 |
通过集合论，我们可以形式化地给出自然数的定义：
$$ \begin{array}{c}\begin{align*} 0 &= \oslash \\ 1 &= \{0\} = \{\oslash\} = \oslash \cup \{\oslash\} = 0 \cup \{0\} \\ 2 &= \{0, 1\} = \{\oslash, \{\oslash\}\} = 1 \cup \{1\} = 0 \cup \{0\} \cup \{1\} \\ 3 &= \{0, 1, 2\} = \{\oslash, \{\oslash\}, \{\oslash \cup \{\oslash\}\}\} = 2 \cup \{2\} = 0 \cup \{0\} \cup \{1\} \cup \{2\} \\ & \cdots \\ n+1 &= n \cup \{n\} \end{align*} \end{array}$$
函数
函数定义为从集合 $A$ 到集合 $B$ 的一种对应关系，记作 $f: A \rightarrow B$。
集合的描述
数据类型
某个类型的所有可能成员都具备一些共同特征，这时我们称它们属于同一个类型。Z语言就是在类型的集合论上建立起来的。
BuildIn types
Z语言的内置类型，无需定义即可使用。常见的类型：
- Integer：表示所有整数，记作 $Z$，可使用 $+, -, *, \text{div}, \text{mod}$ 运算
- Natural（Integer类型的子集）：记作 $N$，必须为非负数。$N1$ 则表示正整数
Basic types
在名称周围添加方括号来声明，可附带注释。例如：
$$[\mathrm{PERSON}] \qquad \text{the set of all persons}$$Free types
通过列举其元素来定义的数据类型，例如：
$$\text{freeType} ::= \text{element}_1 \mid \text{element}_2 \mid \cdots \mid \text{element}_n$$变量
Z语言的每个变量名在赋值前必须先声明，格式为
$$v: \text{TYPE}$$示例，$\text{chauffeur}: \text{PERSON}$，表示 $\text{chauffeur}$ 是 $\text{PERSON}$ 类型的变量。
集合
Z语言中的集合可以通过在括号内列举它的所有值来声明。
备注集合中的元素值的类型必须是先前声明过的类型，否则视为非法值。
| 运算 | 表示 |
|---|---|
| 集合的大小（势） | $\# S$ |
| 幂集 | $\mathbb{P} S$ |
| 差 | $S \backslash T$ |
| 并集 | $S \cup T$ |
| 交集 | $S \cap T$ |
| 划分 | $S \cup T = U \land S \cap T = \oslash$ |
用集合描述系统
特点：以状态的转换为核心描述系统行为；系统的操作（函数）通过描述其执行如何改变系统状态来定义。
步骤
- 定义描述目标系统状态的变量以及与这些变量相关的任何不变的性质
- 定义初始操作，将变量的值设置为满足不变性质的某个初始状态
- 定义对状态的操作，满足在改变状态的同时保持不变的性质
- 定义查询操作，使其在不改变系统状态的前提下获取系统信息
案例：乘客登机系统
- 基本数据类型： $$[\text{PERSON}]$$
- 变量： $$\text{capacty}: N \quad \text{飞机的座位容量} \\ \text{onboard}: \mathbb{P}\text{PERSON} \quad \text{已登机的人群集合}$$
- 全局约束： $$\# \text{onboard} \leqslant \text{capacity}$$
- 初始化操作： $$\text{onboard}' = \oslash$$
- 登机操作： $$\begin{align*} & p: \text{PERSON} \\ & p \in \text{onboard} \\ & \# \text{onboard} < \text{capacity} \\ & \text{onboard}' \cup \{p\} \end{align*}$$
- 下机操作： $$\begin{align*} & p: \text{PERSON} \\ & p \in \text{onboard} \\ & \text{onboard}' \backslash \{p\} \end{align*}$$
- 查询登机人数： $$\begin{align*} & \text{numOnboard}: N \\ & \text{numOnboard} = \# \text{onBoard} \\ & \text{onBoard}' = \text{onBoard} \end{align*}$$
- 查询乘客是否登机： $$\begin{align*} & \text{RESPONSE} ::= \text{yes} \mid \text{no} \\ & \text{numOnboard}: N \\ & \text{reply}: \text{RESPONSE} \\ & ((p \in \text{onBoard} \land \text{reply} = \text{yes}) \lor (p \notin \text{onBorad} \land \text{reply} = no)) \\ & \text{onBoard}' = \text{onBoard} \end{align*}$$
更一般的，可以使用集合和逻辑运算符一起描述一个系统：
$$\text{RESPONSE} ::= \text{OK} \mid \text{twoErrors} \mid \text{onBoard} \mid \text{full} \mid \text{notOnboard}$$这样可以方便地给出登机操作：
$$\begin{align*} & p: \text{PERSON} \\ & \text{reply}: \text{RESPONSE} \\ & (p \notin \text{onBoard} \land \# \text{onBoard} < \text{capacity} \land \text{onBoard}' = \text{onBoard} \cup \{p\} \land \text{reply} = \text{OK}) \\ \lor & (p \in \text{onBoard} \land \# \text{onBoard} = \text{capacity} \land \text{onBoard}' = \text{onBoard} \land \text{reply} = \text{twoErrors}) \\ \lor & (p \in \text{onBoard} \land \# \text{onBoard} < \text{capacity} \land \text{onBoard}' = \text{onBoard} \land \text{reply} = \text{onBoard}) \\ \lor & (p \notin \text{onBoard} \land \# \text{onBoard} = \text{capacity} \land \text{onBoard}' = \text{onBoard} \land \text{reply} = \text{full}) \\\end{align*}$$同理可给出下机操作：
$$\begin{align*} & p: \text{PERSON} \\ & \text{reply}: \text{RESPONSE} \\ & (p \in \text{onBoard} \land \text{onBoard}' = \text{onBoard} \backslash \{p\} \land \text{reply} = \text{OK}) \\ \lor & (p \notin \text{onBoard} \land \text{onBoard}' = \text{onBoard} \land \text{reply} = \text{notOnboard})\end{align*}$$
模式
模式是一种结构化的规格说明。
模式表达
图表格式：
$$\begin{array}{l} \text{SchemaName} \\ \left\| \begin{array}{l} \text{Declarations} \\ \hline \text{Predicate} \\ \hline \end{array} \right.\end{array}$$文字格式：
$$\text{SchemaName} == [\ \text{Declarations} \mid \text{Predicate} \ ]$$一个完整的模式应当包含以下内容：
| 内容 | 规范 |
|---|---|
| 声明 | 每行声明均被视为以分号结尾，若干行构成一个序列 |
| 谓词 | 若干行谓词被视为以运算符连接 |
| 不含谓词部分的模式 | 只声明新变量，不施加约束谓词 |
| 局部变量 | 模式里声明的变量，在其他模式里引用时需要明确包含该定义的模式 |
| 全局变量 | 在规格说明始终可以引用，以公理定义声明；值不能被规格说明运算改变 |
模式推演
模式可作为单元，进行类似逻辑运算的操作
修饰
修饰（Decoration）：表示一个模式在执行了某些操作后的值，可表示为
$$\begin{array}{l} \text{S} \\ \left\| \begin{array}{l} a,b:N \\ \hline a < b \\ \hline \end{array} \right. \end{array} \begin{array}{l} \text{S'} \\ \left\| \begin{array}{l} a',b':N \\ \hline a' < b' \\ \hline \end{array} \right. \end{array}$$包含
包含（Inclusion）： 一个模式的声明可以包含另一个模式，会将被包含模式的声明和谓词合并，可表示为
$$\begin{array}{l} \text{IncludeS} \\ \left\| \begin{array}{l} c:N \\ S \\ \hline c<10 \\ \hline \end{array} \right.\end{array}$$合取与析取
合取（Conjunction）：将两个模式取交，得到一个新模式，其声明原来两个模式的合并，谓词是原来两个模式的与。
析取（Disjunction）：将两个模式取并，得到一个新模式，其声明原来两个模式的合并，谓词是原来两个模式的或。
Delta & Xi
Delta convention 表示模式的改变，可以类比为复制一份，可表示为
$$\begin{array}{l} \Delta\text{S} \\ \left\| \begin{array}{l} a,b:N \\ a',b':N \\ \hline a < b \\ a' < b' \\ \hline \end{array} \right.\end{array}$$Xi convention 表示模式的改变，可以类比为复制一份，它的声明比Delta convention更强，可表示为
$$\begin{array}{l} \Xi\text{S} \\ \left\| \begin{array}{l} a,b:N \\ a',b':N \\ \hline a < b \\ a' < b' \\ a=a' \\ b=b' \\ \hline \end{array} \right.\end{array}$$其他
重命名（Renaming）：
$$\text{newSchemaName} == \text{oldSchemaName} [\text{newName1/oldName1}, \text{newName2/oldName2}, \cdots]$$隐藏（Hide）：隐藏声明中的变量，让它只存在于谓词的运算符中，
$$\text{newSchemaName} == \text{oldSchemaName} \backslash (\text{varName1}, \text{ varName2}, \cdots) $$例如：
$$\begin{array}{l} \text{S} \\ \left\| \begin{array}{l} x_1:T_1 \\ \vdots \\ x_n:T_n \\ \text{declaration} \\ \hline \varphi \\\hline \end{array} \right.\end{array} $$执行 $\text{S}_0 = \text{S} \backslash (x_1, x_2, \cdots, x_n)$ 后，可得
$$\begin{array}{l} \text{S}_0 \\ \left\| \begin{array}{l} \text{declaration} \\ \hline \exist x_1:T_1; \cdots; x_n:T_n \cdot \varphi \\ \hline \end{array} \right.\end{array} $$投影（Project）：隐藏除指定变量之外的变量，
$$\text{newSchemaName} == \text{oldSchemaName} \uparrow (\text{varName1}, \text{varName2}, \cdots)$$合成（Composition）：表示执行 $S$ 后执行 $T$，隐藏了中间变量，可表示为
$$S \circ_g T = (S[x_1^+ / x'_1, \cdots, x_n^+ / x'_n] \land T[x_1^+ / x'_1, \cdots, x_n^+ / x'_n]) \backslash (x_1^+, \cdots, x_n^+) $$输入和输出变量
输入变量：变量名 + $?$
输出变量：变量名 + $!$
举例：
$$\begin{array}{l} \text{Add} \\ \left\| \begin{array}{l} a?,b?:N \\ \text{sum}!:N \\ \hline \text{sum}! = a? + b? \\ \hline \end{array} \right.\end{array}$$谓词、量词与关系
谓词
| 谓词 | 定义 |
|---|---|
| 零元谓词 | 事实的陈述，独立于单个变量 |
| 一元谓词 | 反映对象（个体）的特性 |
| 二元谓词 | 一对对象（个体）的关系 |
量词
全称量词
$$\forall \ \text{declaration} \mid \text{constraint} \cdot \text{predicate}$$$\text{declaration}$ 给出一些变量，$\text{contraint}$ 约束为确定的值，$\text{predicate}$ 均为真
存在量词
$$\exist \ \text{declaration} \mid \text{constraint} \cdot \text{predicate}$$$\text{declaration}$ 给出一些变量，$\text{contraint}$ 约束为确定的值，$\text{predicate}$ 对于一些值为真
唯一量词
$$\exist_1 \ \text{declaration} \mid \text{constraint} \cdot \text{predicate}$$只存在一个值使得 $\text{declaration}$ 为真
集合推导
通过给定条件（谓词）来定义集合。表示为
$$\{\text{declaration} \mid \text{constraint} \cdot \text{expression}\}$$例如：$\{x: Z \mid \text{Even}(x) \cdot x^2 \}$ 表示偶数的平方的集合。
Z中的关系
声明关系
$$R: X \leftrightarrow Y \quad (X \leftrightarrow Y == \mathbb{P}(X \times Y))$$举例：
$$\begin{align*} &[\text{COUNTRY}] \quad \text{the set of all countries} \\ &[\text{LANGUANGE}] \quad \text{the set of all languages} \\ &\text{speaks}: \text{COUNTRY} \leftrightarrow \text{LANGUAGE} \end{align*}$$映射与关系
$x \mapsto y == (x,y)$ 表示 $x$ 与 $y$ 有关
有以下等价关系：
$$xRy == x \mapsto y \in R == (x,y) \in R$$
| 概念 | 内容 |
|---|---|
| 定义域（Domain） | $\text{dom} R == \{a \mid (\exist \ b)((a,b) \in R) \}$ |
| 值域（Range） | $\text{ran} R == \{b \mid (\exist \ a)((a,b) \in R)\}$ |
| 像（Image） | 对于 $S \subseteq \text{dom} R$，$R(|S|)$ 是 $S$ 对应值的集合 |
常用关系
| 关系 | 记法 |
|---|---|
| 中缀关系 | $\_\ R\ \_ : X \leftrightarrow Y$ 常用来定义新关系 |
| 反转关系 | $R\sim \ : Y \leftrightarrow X$ |
| 组合关系 | 若 $R: X \leftrightarrow Y$，$Q: Y \leftrightarrow Z$，则 $R;Q: X \leftrightarrow Z$ |
| 恒等关系 | $\text{id} X == \{x:X \cdot x \mapsto x\}$ |
我们有反向组合 $Q \circ R == R;Q$
特别地，若 $R: X \leftrightarrow X$（即 $xRx$ ），则 $R;R: X \leftrightarrow X$（可记作 $x R^2 x$）
| 限制 | 记号 |
|---|---|
| 定义域限制 | $S \triangleleft R$，表示关系 $R$ 的定义域限制在 $S$ 内 |
| 值域限制 | $R \triangleright S$，表示关系 $R$ 的值域限制在 $S$ 内 |
| 定义域去除 | $S \ntriangleleft R$，表示关系 $R$ 的定义域去掉 $S$ |
| 值域去除 | $R \ntriangleright S$，表示关系 $R$ 的值域去掉 $S$ |
| 闭包 | 记号 |
|---|---|
| 传递闭包 | $x R^+ y$ |
| 自反传递闭包 | $R^* = R^+ \cup \text{id} X$ |
案例：使用关系定义家庭成员关系
$$\begin{align*} & \text{[PERSON]} \\ & \text{father, mother}: \text{PERSON} \leftrightarrow \text{PERSON} \\ & \text{parent}: \text{PERSON} \leftrightarrow \text{PERSON} \\ & \text{sibling}: \text{PERSON} \leftrightarrow \text{PERSON} \\ & \text{ancestor}: \text{PERSON} \leftrightarrow \text{PERSON} \\ \\ & \text{parent}: \text{father} \cup \text{mother} \\ & \text{sibling}: (\text{parent}; \text{parent}\sim) \ \backslash \text{id} \ \text{PERSON} \\ & \text{ancestor}: \text{parent}^+ \\ \end{align*}$$
函数
定义
Z语言中的函数是一种特殊的关系，可为一对一或多对一。定义域有限的函数也称作映射。
记法：$f: X + \rightarrow Y$（从 $X$ 到 $Y$ 的函数）
当 $x \in \text{dom}f$ 且最多只对应一个 $y$ 时，等价于关系 $f: X \leftrightarrow Y, x \in \text{dom}f \Rightarrow \exist_1 y:Y \cdot xfy$
- 若 $\text{source}$ 不全在 $\text{domain}$ 中，则称为部分函数；
- 若 $\text{source}$ 全在 $\text{domain}$ 中，则称为全函数。
| 分类 | 定义 |
|---|---|
| 单射 | 一对一的关系，部分函数中记作 $f: X >+ \rightarrow Y$，全函数中记作 $f: X \rightarrowtail Y$ |
| 满射 | 函数的值域是整个 $\text{target}$，部分函数记作 $f: X + \twoheadrightarrow Y$，全函数记作 $f: X \twoheadrightarrow Y$ |
| 双射 | 既是单射又是满射的函数，记作 $f: X \rightarrowtail Y$ |
函数重写
对于一个已知函数，指定其定义域的一个子集，在对应的值域赋予其新的值。
例如，若 $f: X +\rightarrow Y$，$g: X +\rightarrow Y$，其中 $f$ 被 $g$ 重写为新的函数 $f \oplus g$，则有：
- $f \oplus g == (\text{dom} g \ntriangleleft f) \cup g$（即 $f$ 的定义域去掉 $g$ 的定义域，再并上 $g$）
- 当 $x$ 在 $f$ 的定义域而不在 $g$ 的定义域中时，$f \oplus g\ x = f \ x$
- 当 $x$ 在 $g$ 的定义域中时，$f \oplus g\ x = g \ x$
序列
序列可视为元素到自然数的一个函数，该函数的定义域为从1到序列大小的连续自然数。
不含任何元素的序列称为空序列。
序列的声明
$s: \text{seq} X$ 等价于声明函数 $\{f: N + \rightarrow X \mid \text{dom} f = 1,2\cdots\}$
若序列必须非空，则可声明为 $s: \text{seq}_1 X$
若序列为单射（即 $X$ 中的元素在序列中只出现一次），则可声明为 $s: \text{iseq} X$
常量序列：$s = \left<s_1, s_2, \cdots, s_n\right>$
例如：
$$\begin{array}{c} \begin{align*} &[\text{CITY}] \quad \text{the set of cities of the world} \\ &\text{flight}: \text{seq} \quad \text{CITY} \\ & \text{flight} = \left<\text{Geneva}, \text{Paris}, \text{London}, \text{NewYork}\right> \end{align*} \end{array}$$序列的操作
设序列 $s = \left<s_1, s_2, \cdots, s_n\right>$
| 操作 | 语法 | 示例 |
|---|---|---|
| 选择（Selection） | 获取序列中特定的元素 | $s \ 2 = s_2$ |
| 首元素（Head） | 获取序列中第一个元素 | $\text{head } s = s_1$ |
| 首元素序列（Front） | 获取序列中除去最后一个元素的序列 | $\text{front } s = \left<s_1, s_2, \cdots, s_{n-1}\right>$ |
| 尾元素（Last） | 获取序列中最后一个元素 | $\text{last } s = s_n$ |
| 尾元素序列（Tail） | 获取序列中除去第一个元素的序列 | $\text{tail } s = \left<s_2, s_3 \cdots, s_n\right>$ |
| 取值范围（Range） | 获取序列中所有元素 | $\text{ran } s = \{s_1, s_2, \cdots, s_n\}$ |
| 反转（Reversion） | 将序列中的元素逆序排列 | $\text{rev } s = \left<s_n, s_{n-1}, \cdots, s_1\right>$ |
| 连接（Concatenation） | 对于两个类型相同的序列 $s = \left<s_1, s_2, \cdots, s_m\right>$ 和 $t = \left<t_1, t_2, \cdots, t_n\right>$，可连接为一个新序列，它包含两个序列的所有元素。 | $s^{\land} t = \left<s_1, s_2, \cdots, s_m, t_1, t_2, \cdots, t_n\right>$ |
| 过滤（Filtering） | 从一个序列中尝试获取指定的元素，并按照原序列的次序排列 | $s \uparrow t$ |
| 限制（Restriction） | 与函数的限制类似 | $1 \cdots n \triangleleft s$ |
| 压缩（Squash） | 获取特定范围内的序列 | $m \cdots n \triangleleft s$ |