HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
复制标题
HOL2P - 具有二阶多态性的经典高阶逻辑系统
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Norbert Völker
中科院分区：
文献类型：
--
作者：
Norbert Völker
本文介绍了用类型算子变量和通用类型扩展经典高阶逻辑（HOL）的逻辑系统HOL2P。HOL2P为类型抽象和类型应用提供了显式的术语操作。类型应用项t [t]的形成仅限于不包含任何通用类型的小类型t。这个约束保证了集合论模型的存在性和一致性。
This paper introduces the logical system HOL2P that extends classical higher order logic (HOL) with type operator variables and universal types. HOL2P has explicit term operations for type abstraction and type application. The formation of type application terms t [T] is restricted to small types T that do not contain any universal types. This constraint ensures the existence of a set-theoretic model and thus consistency.
The expressiveness of HOL2P allows category-theoretic concepts such as natural transformations and initial algebras to be applied at the level of polymorphic HOL functions. The parameterisation of terms with type operators adds genericity to theorems. Type variable quantification can also be expressed.
A prototype of HOL2P has been implemented on top of HOL-Light. Type inference is semi-automatic, and some type annotations are necessary. Reasoning is supported by appropriate tactics. The implementation has been used to check some sample derivations.