构造演算以及它在受囿算子系统中的公理化(英文)

首先简略介绍Ｃｏｑｕａｎｄ和Ｈｕｅｔ的构造演算以及Ｐｌｏｔｋｉｎ和孙踊的受囿算子系统。然后，将构造演算在受囿算子系统中进行公理化。此公理化无需无限级（数据）类型结构。原则上，可以在原构造演算的ｔｙｐｅ空间之上引入ｋｉｎｄ空间。但是，不允许在ｋｉｎｄ上使用量词，也不允许引入ｙ：ｋｉｎｄ．从技术上说，将忠实地把构造演算翻译进受囿算子系统中去。为了能对构造演算中的Π类型受予受囿算子系统中的类型，不得不引入新的算子。举例来说，构造演算中的Πｘ：Ｍ．Ｎ可用受囿算子系统中的Πｙ．ｕ：ｔｖ来表达。其中，ｘ对应于ｙ，Ｍ对应于ｔ，以及Ｎ对应于ｕ。