关键词: 受囿算子系统, 等值逻辑, 公理化, 构造演算, 受囿算子

Abstract: This paper briefly introduces Coquand and Huet's Calculus of Constructions (CC) and a Framework for Binding Operators (FBO). It then shows CC's axiomatization in FBO. This axiomatization is without an infinite type hierarchy. Specifically, we introduce an extra universe kind above the original universe type in CC. But we allow neither quantification over kind nor introduction of y: kind. Another operator=> is added for typing II types in FBO, since we are only considering a single-sorted FBO. Technically speaking, we translate CC into FBO; i.e. every CC term is typed in FBO. For example, II,i>x:M.N in CC is translated as IIy.u:t=>v in FBO, where x, M and N correspond to y, t and u respectively under the translation. As a result, we demonstrate that FBO is powerful enough to provide an equational platform for CC.

Key words: binding opera tors, a Framework for Binding Operators (FBO), equational logics, axiomatization, Calculus of Constructions (CC)