本章我们引入原型函数式编程语言PCF及其操作语义.
语言PCF是一个类型化的语言, 其类型集合被归纳定义如下
图2.1 PCF的定型规则 |
本章我们引入一种结构, 其中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的指称语义的一般形式并试图找出我们所施加的结构要求的动机.