一阶Shapely函数的多项式规模分析
Polynomial Size Analysis of First-Order Shapely Functions
摘要：
我们提出了一个大小感知类型系统的一阶shapely函数定义。这里，当结果的大小由参数大小的多项式精确确定时，函数定义被称为shapely。shapely函数定义的示例可以是矩阵乘法和两个列表的笛卡尔积的实现。该类型系统被证明是健全的w.r.t.语言的操作语义。类型检查问题一般是不可判定的。我们定义了一个自然的语法限制，使类型检查成为可判定的，即使大小多项式不一定是线性或单调的。此外，我们已经证明了类型推理问题至少是半可判定的（在此限制下）。我们已经实现了一个过程，结合运行时测试和类型检查，自动获得大小依赖。它终止于所有类型化的函数定义。
英文摘要：
We present a size-aware type system for first-order shapely function definitions. 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 definitions 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
