| 摘要: |
| 带类型的λ－演算是一个逻辑系统，它可以作为程序语言的基础．Ｐｌｏｔｋｉｎ所引进的ＰＣＦ就是这样一类程序语言．Ｐｌｏｔｋｉｎ构造了ＰＣＦ的一个模型，然后讨论与这个模型相关的指称语义和操作语义之间的配合问题──简单配合和完全配合．本文利用Ｓｃｏｔｔ引进的信息系统概念构造ＰＣＦ的另一种模型，并证明与这个模型对应的指称语义与操作语义是完全配合的． |
| 关键词: 操作等价，指称等价，完全配合，信息系统 |
| DOI： |
| 分类号: |
| 基金项目: |
|
| THE INFORMATION SYSTEM MODEL OF PCF |
|
Wang Meiqing
|
| Abstract: |
| Typed lambda-calculus is a logic system, which can be used as a programming language, such as Plotkin's PCF. Plotkin contructed a model for PCF, then he considered the matching problems between the related denotational semanitics and the operational semantics-simple match and complete match. In the present paper the authors construct another model for PCF using the concept of information system which was introduced by Scott in 1982. The authors prove that the denotational semantics are related to the model and the operational semantics are completely matched. |
| Key words: Operational equivalence denotational equivalence complete match information system. |
