函数式编程的论域论基础

第1章引论

第2章 PCF及其操作语义

本章我们引入原型函数式编程语言PCF及其操作语义.

语言PCF是一个类型化的语言, 其类型集合 $Type$ 被归纳定义如下

基本类型 $nat$ 是一个类型, 并且
每当 $σ$ 和 $τ$ 是类型, 那么 $(σ \to τ)$ 也是一个类型.

我们经常将基本类型

nat

记作

ι

, 将

(σ \to τ)

记作

σ \to τ

, 其中

\to

被理解为

Type

上的一个右结合的二元运算, 例如

σ_{1} \to σ_{2} \to σ_{3}

代表

σ_{1} \to (σ_{2} \to σ_{3})

.

\begin{array}{l} \frac{}{Γ, x : σ, Δ ⊢ x : σ} & \frac{Γ, x : σ ⊢ M : τ}{Γ ⊢ (λ x : σ . M) : σ \to τ} \\ \frac{Γ ⊢ M : σ \to τ Γ ⊢ N : σ}{Γ ⊢ M (N) : τ} & \frac{Γ ⊢ M : σ \to σ}{Γ ⊢ Y_{σ} (M) : σ} \\ \frac{}{Γ ⊢ zero : nat} & \frac{Γ ⊢ M : nat}{Γ ⊢ succ (M) : nat} \\ \frac{Γ ⊢ M : nat}{Γ ⊢ pred (M) : nat} & \frac{Γ ⊢ M_{i} : nat, i = 1, 2, 3}{Γ ⊢ ifz (M_{1}, M_{2}, M_{3}) : nat} \end{array}

图2.1 PCF的定型规则

\begin{array}{l} \frac{}{x ⇓ x} & \frac{}{λ x : σ . M ⇓ λ x : σ . M} \end{array}

图2.2 PCF的大步语义

第3章 PCF的Scott模型