论文部分内容阅读
带类型的λ－演算是一个逻辑系统，它可以作为程序语言的基础，Ｐｌｏｔｋｉｎ所引进的ＰＣＦ就是这样一类程序语言。Ｐｌｏｔｋｉｎ构造了ＰＣＦ的一个模型，然后讨论与这个模型相关的指称语义和操作语义之间的配合问题－简单配合和完全配合，本文利用Ｓｃｏｔｔ引进的信息系统概念构造ＰＣＦ的另一种模型，并证明与这个模型对应的指称语义与操作语义是完全配合的。