Polynomial Size Analysis of First-Order Shapely Functions
Polynomial Size Analysis of First-Order Shapely Functions
复制标题
一阶 Shapely 函数的多项式大小分析
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
R. V. Kesteren
中科院分区：
文献类型：
--
作者：
O. Shkaravska;M. V. Eekelen;R. V. Kesteren
A B s t r a c t .我们提出了一个大小感知型系统的一阶shapely函数定义。这里，当结果的大小由参数大小的多项式精确确定时，函数定义被称为shapely。shapely函数定义的示例可以是矩阵乘法和两个列表的笛卡尔积的实现。该类型系统被证明是健全的w.r.t.语言的操作语义。类型检查问题一般是不可判定的。我们定义了一个自然的语法限制，使类型检查成为可判定的，即使大小多项式不一定是线性或单调的。此外，我们已经证明了类型推理问题至少是半可判定的（在此限制下）。我们已经实现了一个过程，结合运行时测试和类型检查，自动获得大小依赖。它终止于所有类型化的函数定义。
A b s t r a c t . We present a size-aware type system for first-order shapely function defini tions. Here, a function definition is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments. Examples of shapely function defi nitions may be implementations of matrix multiplication and the Cartesian product of two lists. The type system is proved to be sound w.r.t. the operational semantics of the language. The type checking problem is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear or monotonic. Furthermore, we have shown that the type-inference problem is at least semi-decidable (under this restriction). We have implemented a procedure that combines run-time testing and type-checking to automatically obtain size dependencies. It terminates on total typable function definitions.