THE INFORMATION SYSTEM MODEL OF PCF
PCF的信息系统模型

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.