程序语言理论笔记 | 起居室老虎

Chpt 1. Set Theory

幂集, Power Set: 集合 $A$ 的所有子集构成的集合，记作 $P(A)$ 或 $2^A$

外延性公理, Axiom of Extensionality: 两个集合包含相同的元素则它们相等

\forall A\forall B(\forall x(x\in A\leftrightarrow x\in B)\rightarrow A=B).

构造公理：

空集公理 Empty Set Axiom:

\exist A\forall x(x\notin A).

配对公理 Paring Axiom:

\forall u\forall v\exist A\forall x(x\in A \leftrightarrow(x=u\lor x=v)

并集公理 Union Axiom:

\forall A\exist B \forall x(x\in B \leftrightarrow \exist C(C\in A\land x\in C))

幂集公理 Power Set Axiom:

\forall A\exist B\forall x(x\in B\leftrightarrow x\subseteq A)

偏序, Partial Order: 对于一个关系 $R$ 和一个集合 $X$ ，如果满足：

Reflexivity 自反性： $\forall x\in X, x R x$
Anti-symmetry 反对称性： $\forall x\forall y \in X, xRy, yRx\leftrightarrow x=y$
Transitivity 传递性： $\forall x \forall y \forall z\in X, xRy, yRz \rightarrow xRz$ .

则 $\left<X, R\right>$ 是一个偏序关系。

Chpt 2. Operational Semantics

IMP 语言的操作语义

状态（State）：
- 状态是一个函数 $\sigma :Loc\rightarrow N$
- 状态的集合表示为 $\sum$
- 直观理解：状态指定了各个位置（变量）所持有的值
目标：
- 构建一个关系 $R\subseteq(Com \times \sum)\times \sum$ ，使得 (c,σ)Rσ′ 表示在初始状态 σ 下执行命令 c，最终得到状态 $\sigma'$
算术表达式的配置（Configurations for Aexp）：
- 配置是一个对 $\left<a, \sigma\right>$ ，其中 $a\in Aexp$ 且 $\sigma \in \sum$
- 目标：定义一个关系 $\left<a, \sigma\right>\rightarrow n$ ，表示在状态 $\sigma$ 下，算术表达式 $a$ 被求值为整数 $n$ .

IMP 的命令语义

赋值

\frac{\langle a, \sigma \rangle \Rightarrow n}{\langle X := a, \sigma \rangle \Rightarrow \sigma[X \mapsto n]}

顺序

\frac{\langle c_1, \sigma \rangle \Rightarrow \sigma'' \quad \langle c_2, \sigma'' \rangle \Rightarrow \sigma'}{\langle c_1; c_2, \sigma \rangle \Rightarrow \sigma'}

条件分支

\frac{\langle b, \sigma \rangle \Rightarrow true \quad \langle c_1, \sigma \rangle \Rightarrow \sigma'}{\langle if \ b \ then \ c_1 \ else \ c_2, \sigma \rangle \Rightarrow \sigma'}\\ \frac{\langle b, \sigma \rangle \Rightarrow false \quad \langle c_2, \sigma \rangle \Rightarrow \sigma'}{\langle if \ b \ then \ c_1 \ else \ c_2, \sigma \rangle \Rightarrow \sigma'}

循环

\frac{\langle b, \sigma \rangle \Rightarrow false}{\langle while \ b \ do \ c, \sigma \rangle \Rightarrow \sigma}\\ \frac{\langle b, \sigma \rangle \Rightarrow true \quad \langle c, \sigma \rangle \Rightarrow \sigma'' \quad \langle while \ b \ do \ c, \sigma'' \rangle \Rightarrow \sigma'}{\langle while \ b \ do \ c, \sigma \rangle \Rightarrow \sigma'}

大步语义：如上，描述程序从初始状态到最终状态的转变，不关注中间过程； $\left<c, \sigma\right>\rightarrow\sigma'$

小步语义：描述 one-step 的执行变化，比如执行了一次加法或赋值； $\left<c, \sigma\right>\rightarrow_1\left<c', \sigma'\right>$

Chpt 3. Some Principles of Induction

数学归纳法：

\left[ P(0) \& \forall n\in \mathbb{N}. (P(n)\rightarrow P(n+1))\right] \rightarrow \forall n\in \mathbb{N}. P(n)

良基归纳 Well-Founded Induction:

$A$ : a set
$\prec \subseteq A\times A$ : a binary relation on $A$

The relation $\prec$ is well-founded if:

there is no infinite descending sequence $... \prec a_n\prec ... \prec a_1\prec a_0$ in $A$ .
well-foundedness implies irreflexibility: $\forall a\in A, a\nprec a.$

即不允许无限下降链，所以 $\leq$ 不是良基的，因为可以出现无限下降链（全等于）。

结构归纳 Structural Induction:

基始步（Base Case）：证明性质对于基本结构（即最小或最简单的结构）成立。
归纳步（Inductive Step）：假设性质对某些子结构成立，然后证明性质对包含这些子结构的复合结构也成立。

Chpt 4. Inductive Definitions

$前提/结论$

Axiom Instances: $\empty/y$

Non-axiom Rule Instances: $\left\{x_1, ..., x_n\right\}/y$

$d\vdash_Ry$ ：推导 $d$ 在规则集 $R$ 下可以导出结论 $y$ 。

(\emptyset / y) \vdash_R y \text{ if } (\emptyset / y) \in R

(\{d_1, \ldots, d_n\} / y) \vdash y \text{ if } (\{x_1, \ldots, x_n\} / y) \in R ~~\text{and}~~ d_1 \vdash_R x_1, \ldots, d_n \vdash_R x_n;

Rule Induction:

$I_R=\{y\in E|\vdash _R y\}$ ， $I$ 是元素集合 $E$ 中可以通过规则 $R$ 推导得到的元素的集合；
$P$ 是 $I_R$ 上的一个谓词：

\begin{align*}&\forall x\in I_R. P(x) ~~\text{iff}~~~ \forall (X/y)\in R. [(X\subseteq I_R ~~\&~~ \forall x\in X.P(x))\rightarrow P(y)]\end{align*}

就是若 $X$ 则 $y$ ， $X$ 都满足 $P$ 则 $y$ 也满足

Closedness：

\forall (X/y)\in R. (x\subseteq Q\rightarrow y\in Q).

Special Rule Induction: 证明一个谓词 $P$ 在 $I_R$ 的一个子集 $A$ 上成立

\forall (X/y)\in R. [(X\subseteq I_R ~\&~ y\in A~\&~ (\forall x\in X \cap A.~~Q(x)))\rightarrow Q(y)]

证明过程例子： $Y$ : a location (program variable)

\forall c, \sigma, \sigma' \cdot [(Y \notin \text{loc}(c) \ \& \ \langle c, \sigma \rangle \to \sigma') \Rightarrow \sigma(Y) = \sigma'(Y)]

证：

定义集合 $A$ ：

A:= \{ \langle c, \sigma \rangle \to \sigma' \mid Y \notin \text{loc}(c) \}

定义谓词 $Q$ ：

Q(c, \sigma, \sigma') := \sigma(Y) = \sigma'(Y)

验证条件：

\forall \langle c, \sigma \rangle \to \sigma' \in A . Q(c, \sigma, \sigma')

利用闭合性：

\forall (X/y) \in R. [(X \subseteq I_R \ \& \ y \in A \ \& \ (\forall x \in X \cap A \cdot Q(x))) \Rightarrow Q(y)]

Chpt 5. The Denotational Semantics of IMP

Equivalence over Commands:

\begin{align*}c_0\sim c_1,~~~ &\text{iff}~\forall \sigma, \sigma', (\left<c_0, \sigma\right>\rightarrow \sigma'\leftrightarrow \left<c_1, \sigma\right>\rightarrow\sigma')\\&\text{iff}~\{(\sigma, \sigma')|\left<c_0, \sigma\right>\rightarrow \sigma'\}=\{(\sigma, \sigma')|\left<c_1, \sigma\right>\rightarrow \sigma'\}\end{align*}

从这个视角来看，commands 都是一些偏函数，展示了从一些状态转移到另一些状态的过程。Denotational Semantics 指称语义就是研究程序对应的数学对象，通过这些数学对象的性质研究程序的性质。

完备偏序集 Complete Partial Orders CPOs:

上界
- $(P, \sqsubseteq)$ 是一个偏序集，指 $P$ 是一个集合而 $\sqsubseteq$ 是一个偏序关系；
- $X$ 是 P 的一个子集；
- 若 $p\in P$ 满足 $\forall q\in X.~~q\sqsubseteq p.$ ，则 $p$ 是 $X$ 的上界。
- $p_0$ 是最小上界： $\forall q \in X_p, p_0\sqsubseteq q$
$\omega$ - 链
- 无限序列 $d_0, ..., d_n, ...$ ，满足 $d_0\sqsubseteq d_1\sqsubseteq ... \sqsubseteq d_n\sqsubseteq ...$
CPOs
- $(P, \sqsubseteq)$ 是一个 CPO，如果对于 $P$ 上任意的 $\omega$ - 链，最小的上界都存在于 $P$ 中，记作：

\bigsqcup_{n\in\omega}d_n:=\sqcup\{d_n|n\in\omega\}=\sqcup\{d_0, d_1, ..., d_n, ...\}

最小元素： $p\in P$ 是最小元素，如果 $\forall q\in P. p\sqsubseteq q.$
CPOs with bottom: 有最小元素的 CPO

单调函数 Monotonic Functions:

With $(D, \sqsubseteq_D),~(E, \sqsubseteq_E)$ ，a function $f:~D\rightarrow E$ is monotonic if

\forall d, d'\in D.~[d\sqsubseteq_Dd'\rightarrow f(d)\sqsubseteq_E f(d')]

连续函数 Continous Functions:

A function $f:~D\rightarrow E$ is continuous if

$f$ is monotonic
for all $\omega$ -chains $d_0 \sqsubseteq d_1\sqsubseteq ... \sqsubseteq d_n \sqsubseteq ...$ in $D$ , we have

\bigsqcup_{n\in \omega}f(d_n)=f\left(\bigsqcup_{n\in\omega}d_n\right)

不动点 Fixed Points:

An element $d\in D$ is:

a fixed point of $f$ if $f(d)=d$
a prefixed point of $f$ if $f(d) \sqsubseteq d$

Suppose

$(D, \sqsubseteq_D)$ with a bottom $\bot_D$
$f:D\rightarrow D$ a continuous function
$\bot_D \sqsubseteq f(\bot_D)\sqsubseteq f^2(\bot_D)\sqsubseteq ... \sqsubseteq f^n(\bot_D)\sqsubseteq...$
$\text{fix}(f)=\bigsqcup_{n\in \omega}f^n(\bot_D)$

Then

$\text{fix}(f)$ is fix point of $f$
$\text{fix}(f)$ is the least prefixed point of $f:~~f(d)\sqsubseteq d \rightarrow \text{fix}(f)\sqsubseteq d$
$\text{fix}(f)$ is the least fixed point of $f: ~ f(d)=d\rightarrow \text{fix}(f)\sqsubseteq d$

Knaster-Tarski 不动点 Knaster-Tarski Fixed-Point Theorem：

完全格 Complete Lattices： $(D, \sqsubseteq)$ is a complete lattice if greatest lower bound $\sqcap X$ exists for every $X \subseteq D$
$L$ 是一个完全格， $f:L\rightarrow L$ 是一个单调函数，则 $f$ 在 $L$ 上有不动点，有最大最小不动点，且不动点的集合也是一个完全格

Chpt 5. The Axiomatic Semantics of IMP

霍尔三元组 Hoare Triples：

\{P\}c\{Q\}

$P$ 是前条件， $c$ 是命令， $Q$ 是后条件。

Assn 定义一组逻辑断言，描述和验证程序的行为。状态 $\sigma$ 满足一个断言 $A$ 记作 $\sigma\models A$ ，当且仅当 $A$ 中所有的 $X$ 被 $\sigma(X)$ 替代之后 $A$ 仍然为真。 $A[a/i]$ 就是把程序 $A$ 中的 $i$ 全部替换成 $a$ 。

\sigma\models'\{A\}c\{B\}~\text{iff}~(\sigma\models'A\implies C[x](\sigma)\models'B)

如果 $A$ 满足， $c$ 能停止，则停止后 $B$ 一定满足