函数式编程的论域论基础

第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的定型规则

第3章 PCF的Scott模型

本章我们引入一种结构, 其中Dana Scott解释了PCF语言 (及其逻辑LCF). (See Scott [1969] for a reprint of a widely circulated underground paper from 1969 where this interpretation was presented for the first time.) 但是在此之前, 我们将会讨论PCF的指称语义的一般形式并试图找出我们所施加的结构要求的动机.

函数式编程的论域论基础

第1章引论

第2章 PCF及其操作语义

第3章 PCF的Scott模型

第3.1节基本的domain论

第3.2节 PCF的domain模型

第3.3节 LCF——可计算函数逻辑

第4章 Computational Adequacy

第5章 Milner的上下文引理

第6章完全抽象问题

第7章逻辑关系 (Logical Relations)

第8章 $D_{σ}$ 的一些结构性质

第9章递归domain方程的解

第10章完全抽象模型的刻画

第11章作为PCF模型的顺序domain

函数式编程的论域论基础

第1章 引论

第2章 PCF及其操作语义

第3章 PCF的Scott模型

第3.1节 基本的domain论

第3.2节 PCF的domain模型

第3.3节 LCF——可计算函数逻辑

第4章 Computational Adequacy

第5章 Milner的上下文引理

第6章 完全抽象问题

第7章 逻辑关系 (Logical Relations)

第8章 Dσ的一些结构性质

第9章 递归domain方程的解

第10章 完全抽象模型的刻画

第11章 作为PCF模型的顺序domain

第1章引论

第3.1节基本的domain论

第6章完全抽象问题

第7章逻辑关系 (Logical Relations)

第8章 $D_{σ}$ 的一些结构性质

第9章递归domain方程的解

第10章完全抽象模型的刻画

第11章作为PCF模型的顺序domain