简单类型 λ-演算中的可定义函数
摘要：在简单类型的lambda演算中，可定义的整数函数与扩展的多项式完全一致，这是众所周知的。当我们将整数解释为类型（p->p)->p->p，其中p是一种基本类型，或者等号被视为β-转换时，确实如此。普遍认为，对于β-η等式和任何形式为（t->t)->t->t的固定类型表示的整数，情况也是如此。本文证明了这种观点不完全正确。 我们证明了在简单类型的lambda演算中，可严格定义的函数类要比扩展的多项式类大得多。具体而言，我们将F定义为可严格定义的函数类，将G定义为包含了扩展的多项式和两个额外函数（准确地说，是两个函数模式）的类，并且在组合下封闭。我们证明G是F的一个子集。 我们猜想G精确地描述了可严格定义的函数，即G=F，并且我们收集了一些证据支持这个猜想，例如，证明了每个斜表示有限范围函数都可严格表示为（t->t)->t->t，其中t是某种类型。
作者：Mateusz Zakrzewski
论文ID：cs/0701022
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23