Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings.
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings.
复制标题
智能计算机数学 - 国际会议，CICM 2015，美国华盛顿特区，2015 年 7 月 13-17 日，会议记录。
DOI：
10.1007/978-3-319-20615-8_6
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Obua S
中科院分区：
文献类型：
--
作者：
Obua S
zfh代表在高阶逻辑中实现的Zermelo-Fraenkel集合理论。它是Agerholm和Gordon的HOL-ST的后代，但不允许使用类型变量，也不允许定义新类型。我们首先要说明为什么我们要使用ZFH的proofpeer，这是我们正在构建的协作定理证明系统。然后我们重点介绍了我们为ZFH开发的类型推断算法。在ZFH的语法中，以并置形式编写的函数应用程序被重载为集合论的或高阶的。我们的算法扩展了Hindley-Milner类型推断来处理这种特殊的函数应用程序过载。我们描述了该算法，证明了其正确性，并讨论了为什么在存在强制或重载的情况下进行类型推断的先前一般方法不能涵盖我们的特殊情况。
ZFHstands for Zermelo-Fraenkel set theory implemented in higher-order logic. It is a descendant of Agerholm’s and Gordon’s HOL-ST but does not allow the use of type variables nor the definition of new types. We first motivate why we are using ZFH forProofPeer, the collaborative theorem proving system we are building. We then focus on the type inference algorithm we have developed for ZFH. In ZFH’s syntax, function application, written as juxtaposition, is overloaded to be either set-theoretic or higher-order. Our algorithm extends Hindley-Milner type inference to cope with this particular overloading of function application. We describe the algorithm, prove its correctness, and discuss why prior general approaches to type inference in the presence of coercions or overloading do not cover our particular case.