函数式编程的论域论基础

第1章 引论

第2章 PCF及其操作语义

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

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

我们经常将基本类型nat记作ι, 将(στ)记作στ, 其中被理解为Type上的一个右结合的二元运算, 例如σ1σ2σ3代表σ1(σ2σ3).

Γ,x:σ,Δx:σΓ,x:σM:τΓ(λx:σ.M):στΓM:στΓN:σΓM(N):τΓM:σσΓYσ(M):σΓzero:natΓM:natΓsucc(M):natΓM:natΓpred(M):natΓMi:nat,i=1,2,3Γifz(M1,M2,M3):nat
图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的指称语义的一般形式并试图找出我们所施加的结构要求的动机.

第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