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) \to A = B) .

构造公理：

空集公理 Empty Set Axiom:

\exists A \forall x (x \in / A) .

配对公理 Paring Axiom:

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

并集公理 Union Axiom:

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

幂集公理 Power Set Axiom:

\forall A \exists 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, x R y, y R x \leftrightarrow x = y$
Transitivity 传递性： $\forall x \forall y \forall z \in X, x R y, y R z \to x R z$ .

则 $⟨ X, R ⟩$ 是一个偏序关系。

Chpt 2. Operational Semantics

IMP语言的操作语义

状态（State） ：
- 状态是一个函数 $σ : L oc \to N$
- 状态的集合表示为 $\sum$
- 直观理解：状态指定了各个位置（变量）所持有的值
目标：
- 构建一个关系 $R \subseteq (C o m \times \sum) \times \sum$ ，使得 (c,σ)Rσ′ 表示在初始状态 σ 下执行命令 c，最终得到状态 $σ^{'}$
算术表达式的配置（Configurations for Aexp） ：
- 配置是一个对 $⟨ a, σ ⟩$ ，其中 $a \in A e x p$ 且 $σ \in \sum$
- 目标：定义一个关系 $⟨ a, σ ⟩ \to n$ ，表示在状态 $σ$ 下，算术表达式 $a$ 被求值为整数 $n$ .

IMP的命令语义

赋值

\frac{⟨ a , σ ⟩ \Rightarrow n}{⟨ X := a , σ ⟩ \Rightarrow σ [ X \mapsto n ]}

顺序

\frac{⟨ c _{1} , σ ⟩ \Rightarrow σ ^{''} ⟨ c _{2} , σ ^{''} ⟩ \Rightarrow σ ^{'}}{⟨ c _{1} ; c _{2} , σ ⟩ \Rightarrow σ ^{'}}

条件分支

\frac{⟨ b , σ ⟩ \Rightarrow t r u e ⟨ c _{1} , σ ⟩ \Rightarrow σ ^{'}}{⟨ i f b t h e n c _{1} e l se c _{2} , σ ⟩ \Rightarrow σ ^{'}} \frac{⟨ b , σ ⟩ \Rightarrow f a l se ⟨ c _{2} , σ ⟩ \Rightarrow σ ^{'}}{⟨ i f b t h e n c _{1} e l se c _{2} , σ ⟩ \Rightarrow σ ^{'}}

循环

\frac{⟨ b , σ ⟩ \Rightarrow f a l se}{⟨ w hi l e b d o c , σ ⟩ \Rightarrow σ} \frac{⟨ b , σ ⟩ \Rightarrow t r u e ⟨ c , σ ⟩ \Rightarrow σ ^{''} ⟨ w hi l e b d o c , σ ^{''} ⟩ \Rightarrow σ ^{'}}{⟨ w hi l e b d o c , σ ⟩ \Rightarrow σ ^{'}}

大步语义：如上，描述程序从初始状态到最终状态的转变，不关注中间过程； $⟨ c, σ ⟩ \to σ^{'}$

小步语义：描述one-step的执行变化，比如执行了一次加法或赋值； $⟨ c, σ ⟩ \to_{1} ⟨ c^{'}, σ^{'} ⟩$

Chpt 3. Some Principles of Induction

数学归纳法：

[P (0) &\forall n \in N . (P (n) \to P (n + 1))] \to \forall n \in N . P (n)

良基归纳 Well-Founded Induction:

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

The relation $≺$ is well-founded if:

there is no infinite descending sequence $... ≺ a_{n} ≺ ... ≺ a_{1} ≺ a_{0}$ in $A$ .
well-foundedness implies irreflexibility: $\forall a \in A, a ⊀ a .$

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

结构归纳 Structural Induction:

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

Chpt 4. Inductive Definitions

$前提 / 结论$

Axiom Instances: $\emptyset/ y$

Non-axiom Rule Instances: ${x_{1}, ..., x_{n}} / y$

$d ⊢_{R} y$ ：推导 $d$ 在规则集 $R$ 下可以导出结论 $y$ 。

(\emptyset/ y) ⊢_{R} y if (\emptyset/ y) \in R

({d_{1}, \dots, d_{n}} / y) ⊢ y if ({x_{1}, \dots, x_{n}} / y) \in R and d_{1} ⊢_{R} x_{1}, \dots, d_{n} ⊢_{R} x_{n};

Rule Induction:

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

\forall x \in I_{R} . P (x) iff \forall (X / y) \in R . [(X \subseteq I_{R} & \forall x \in X . P (x)) \to P (y)]

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

Closedness：

\forall (X / y) \in R . (x \subseteq Q \to 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))) \to Q (y)]

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

\forall c, σ, σ^{'} \cdot [(Y \in / loc (c) & ⟨ c, σ ⟩ \to σ^{'}) \Rightarrow σ (Y) = σ^{'} (Y)]

证：

定义集合 $A$ ：

A := {⟨ c, σ ⟩ \to σ^{'} ∣ Y \in / loc (c)}

定义谓词 $Q$ ：

Q (c, σ, σ^{'}) := σ (Y) = σ^{'} (Y)

验证条件：

\forall ⟨ c, σ ⟩ \to σ^{'} \in A . Q (c, σ, σ^{'})

利用闭合性：

\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:

c_{0} \sim c_{1}, iff \forall σ, σ^{'}, (⟨ c_{0}, σ ⟩ \to σ^{'} \leftrightarrow ⟨ c_{1}, σ ⟩ \to σ^{'}) iff {(σ, σ^{'}) ∣ ⟨ c_{0}, σ ⟩ \to σ^{'}} = {(σ, σ^{'}) ∣ ⟨ c_{1}, σ ⟩ \to σ^{'}}

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

完备偏序集 Complete Partial Orders CPOs:

上界
- $(P, ⊑)$ 是一个偏序集，指 $P$ 是一个集合而 $⊑$ 是一个偏序关系；
- $X$ 是P的一个子集；
- 若 $p \in P$ 满足 $\forall q \in X . q ⊑ p .$ ，则 $p$ 是 $X$ 的上界。
- $p_{0}$ 是最小上界： $\forall q \in X_{p}, p_{0} ⊑ q$
$ω$ -链
- 无限序列 $d_{0}, ..., d_{n}, ...$ ，满足 $d_{0} ⊑ d_{1} ⊑ ... ⊑ d_{n} ⊑ ...$
CPOs
- $(P, ⊑)$ 是一个CPO，如果对于 $P$ 上任意的 $ω$ -链，最小的上界都存在于 $P$ 中，记作：

n \in ω ⨆ d_{n} := ⊔ {d_{n} ∣ n \in ω} = ⊔ {d_{0}, d_{1}, ..., d_{n}, ...}

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

单调函数 Monotonic Functions:

With $(D, ⊑_{D}), (E, ⊑_{E})$ ，a function $f : D \to E$ is monotonic if

\forall d, d^{'} \in D . [d ⊑_{D} d^{'} \to f (d) ⊑_{E} f (d^{'})]

连续函数Continous Functions:

A function $f : D \to E$ is continuous if

$f$ is monotonic
for all $ω$ -chains $d_{0} ⊑ d_{1} ⊑ ... ⊑ d_{n} ⊑ ...$ in $D$ , we have

n \in ω ⨆ f (d_{n}) = f (n \in ω ⨆ d_{n})

不动点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) ⊑ d$

Suppose

$(D, ⊑_{D})$ with a bottom $⊥_{D}$
$f : D \to D$ a continuous function
$⊥_{D} ⊑ f (⊥_{D}) ⊑ f^{2} (⊥_{D}) ⊑ ... ⊑ f^{n} (⊥_{D}) ⊑ ...$
$fix (f) = ⨆_{n \in ω} f^{n} (⊥_{D})$

Then

$fix (f)$ is fix point of $f$
$fix (f)$ is the least prefixed point of $f : f (d) ⊑ d \to fix (f) ⊑ d$
$fix (f)$ is the least fixed point of $f : f (d) = d \to fix (f) ⊑ d$

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

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

Chpt 5. The Axiomatic Semantics of IMP

霍尔三元组 Hoare Triples：

{P} c {Q}

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

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

σ ⊨^{'} {A} c {B} iff (σ ⊨^{'} A ⟹ C [x] (σ) ⊨^{'} B)

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

程序语言理论笔记